\documentclass{article}
\input camila.mac
\begin{document}

\INCLUDE{io.cam}
\INCLUDE{seq.cam}
\INCLUDE{str.cam}
\INCLUDE{txt.cam}
\SORTS

$\begin{array}{lcll}
Db & \cong & IdComp \pfunc{MComp}  \\
MComp & \cong & {Comp + RComp}  \\
Comp & \cong & 
\PROD F \TYPE IdCompIfAny \NEXT St \TYPE str \pfunc{Sets} \NEXT A \TYPE Actions \DORP
  \\
IdCompIfAny & \cong & IdComp + 1  \\
RComp & \cong & 
\PROD F \TYPE IdComp \NEXT St \TYPE str \pfunc{str} \NEXT A \TYPE str \pfunc{str} \DORP
  \\
Actions & \cong & IdAccao \pfunc{Func}  \\
Func & \cong & 
\PROD I \TYPE {Sets^{\star}} \NEXT O \TYPE {Sets^{\star}} \DORP
  \\
Sets & \cong & {{{{{{Var + Pow} + List} + Ffun} + Times} + Plus} + Cons}  \\
Cons & \cong & 
\PROD N \TYPE str \DORP
  \\
Var & \cong & 
\PROD V \TYPE str \DORP
  \\
Pow & \cong & 
\PROD E \TYPE Sets \DORP
  \\
List & \cong & 
\PROD A \TYPE Sets \DORP
  \\
Ffun & \cong & 
\PROD D \TYPE Sets \NEXT R \TYPE Sets \DORP
  \\
Times & \cong & 
\PROD A \TYPE Sets \NEXT B \TYPE Sets \DORP
  \\
Plus & \cong & 
\PROD A \TYPE Sets \NEXT B \TYPE Sets \DORP
  \\
IdComp & \cong & str  \\
IdAccao & \cong & str  \\
\end{array}$

\OPERS

$\begin{array}{l}
TAXDUMP:NAT \tfunc{VOID} \\ TAXDUMP(i) \deff \\ \rule{3ex}{0pt}  
\LET 
a = \{k \asor k \in 
dom(db) \wedge 
\neg \is{nil}(
F( db(k))) \}\\
b =  
\star\hookrightarrow F (
db \mapdr a) 
\IN 
ioTxt2File(\!\!\mattt{
\mbox{\texttt{"\_tmp0"}}},
tax2txt(
llg2tax(b),0,i)) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
flat(p) \deff \\ \rule{3ex}{0pt} \enlist{
\pi_1(p),
\pi_1(
\pi_2(p)),
\pi_2(
\pi_2(p))}
\end{array}$

\traco

$\begin{array}{l}
listByIndex:A \pfunc{B} \times {A^{\star}} \tfunc{ABlist} \\ listByIndex(f,l) \deff \\ \rule{3ex}{0pt}  \enlist{\enlist{a, f(a)} \asor a \in l \wedge 
a \in 
dom(f)}
\end{array}$

\traco

$\begin{array}{l}
STRsetSort:{\set{str}} \tfunc{{str^{\star}}} \\ STRsetSort(s) \deff \\ \rule{3ex}{0pt}  
\COND{
s = \emptyset}{\emptylist}{
\LET 
a = 
strMIN(s) 
\IN \enlist{a} \conc 
STRsetSort(s - \{a\}) 
\TEL}
\end{array}$

\traco

$\begin{array}{l}
addSep2StrList(l,s) \deff \\ \rule{3ex}{0pt} 
\COND{
l = \emptylist}{\emptylist}{\enlist{
head(l)} \conc 
\conc (\enlist{\enlist{s,x} \asor x \in 
tail(l)})}
\end{array}$

\traco

$\begin{array}{l}
llg2tax:LLGraph \tfunc{Tax} \\ llg2tax(g) \deff \\ \rule{3ex}{0pt}  
llg2taxAux(g,\{a \asor a \in 
ran(g) - 
dom(g)\})
\end{array}$

\traco

$\begin{array}{l}
llg2taxAux:LLGraph \times Classes \tfunc{Tax} \\ llg2taxAux(g,S) \deff \\ \rule{3ex}{0pt}  \left( \begin{array}{c}
 a \\ 
llg2taxAux(g,\{b \asor b \in 
dom(g) \wedge 
 g(b) = a\}) 
\end{array} \right)_{a \in S}
\end{array}$

\traco

$\begin{array}{l}
tax2txt:Tax \times NAT \times NAT \tfunc{txt} \\ tax2txt(t,a,b) \deff \\ \rule{3ex}{0pt}  
\LET 
c = 
\conc (\enlist{\enlist{\enlist{
strFill(\!\!\mattt{
\mbox{\texttt{" "}}},
a \times b),k}} \conc 
tax2txt( t(k),
a + 1,b) \asor k \in 
dom(t)}) 
\IN 
txtFlat(
txtAddNL(c)) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
SetsSubst:Sets \times str \pfunc{Sets} \tfunc{Sets} \\ SetsSubst(e,s) \deff \\ \rule{3ex}{0pt}  
\COND{\is{Cons}(e)}{e}{
\COND{\is{Var}(e)}{
\LET 
v = 
V(e) 
\IN 
\COND{
v \in 
dom(s)}{ s(v)}{e} 
\TEL}{
\COND{\is{Pow}(e)}{
Pow(
SetsSubst(
E(e),s))}{
\COND{\is{List}(e)}{
List(
SetsSubst(
A(e),s))}{
\COND{\is{Ffun}(e)}{
Ffun(
SetsSubst(
D(e),s),
SetsSubst(
R(e),s))}{
\COND{\is{Times}(e)}{
Times(
SetsSubst(
A(e),s),
SetsSubst(
B(e),s))}{
Plus(
SetsSubst(
A(e),s),
SetsSubst(
B(e),s))}}}}}}
\end{array}$

\traco

$\begin{array}{l}
Sets2STR:Sets \tfunc{str} \\ Sets2STR(e) \deff \\ \rule{3ex}{0pt}  
\COND{\is{Cons}(e)}{
N(e)}{
\COND{\is{Var}(e)}{
V(e)}{
\COND{\is{Pow}(e)}{
strcat(
Sets2STRaux(
E(e)),\!\!\mattt{
\mbox{\texttt{"-set"}}})}{
\COND{\is{List}(e)}{
strcat(
Sets2STRaux(
A(e)),\!\!\mattt{
\mbox{\texttt{"-seq"}}})}{
\COND{\is{Ffun}(e)}{
strcat(
Sets2STRaux(
D(e)),\!\!\mattt{
\mbox{\texttt{"->"}}},
Sets2STR(
R(e)))}{
\COND{\is{Times}(e)}{
strcat(
Sets2STRaux(
A(e)),\!\!\mattt{
\mbox{\texttt{"*"}}},
Sets2STRaux(
B(e)))}{
strcat(
Sets2STRaux(
A(e)),\!\!\mattt{
\mbox{\texttt{"+"}}},
Sets2STRaux(
B(e)))}}}}}}
\end{array}$

\traco

$\begin{array}{l}
Sets2STRaux:Sets \tfunc{str} \\ Sets2STRaux(e) \deff \\ \rule{3ex}{0pt}  
\COND{\is{Cons}(e)}{
N(e)}{
\COND{\is{Var}(e)}{
V(e)}{
strcat(\!\!\mattt{
\mbox{\texttt{"("}}},
Sets2STR(e),\!\!\mattt{
\mbox{\texttt{")"}}})}}
\end{array}$

\traco

$\begin{array}{l}
ActionsSubst:Actions \times str \pfunc{Sets} \tfunc{Actions} \\ ActionsSubst(f,s) \deff \\ \rule{3ex}{0pt}  \left( \begin{array}{c}
 k \\ 
\LET 
x =  f(k)\\
i = 
I(x)\\
o = 
O(x)\\
ii = \enlist{
SetsSubst(e,s) \asor e \in i}\\
oo = \enlist{
SetsSubst(e,s) \asor e \in o} 
\IN 
Func(ii,oo) 
\TEL 
\end{array} \right)_{k \in 
dom(f)}
\end{array}$

\traco

$\begin{array}{l}
Comp2SEXP:Comp \times Db \tfunc{SEXP} \\ Comp2SEXP(i,db) \deff \\ \rule{3ex}{0pt}  
\COND{
i \in 
dom(db)}{
\LET 
x =  db(i)\\
a = 
\COND{\is{Comp}(x)}{
AcInherit(i,\left(  \right),db)}{
\LET 
y = 
AcInherit(
F(x),
A(x),db)\\
f = 
\LAMBDA{d}
SetsSubst(d, 
\star\hookrightarrow Var (
St(x))) 
\IN \left( \begin{array}{c}
 a \\ 
\LET 
i = 
I( y(a))\\
o = 
O( y(a)) 
\IN 
Func( 
f^* (i), 
f^* (o)) 
\TEL 
\end{array} \right)_{a \in 
dom(y)} 
\TEL}\\
b = \left( \begin{array}{c}
 n \\ 
\LET 
x =  a(n)\\
i = \enlist{
Sets2STR(s) \asor s \in 
I(x)}\\
o = \enlist{
Sets2STR(s) \asor s \in 
O(x)}\\
ii = 
strCAT(
addSep2StrList(i,\!\!\mattt{
\mbox{\texttt{" , "}}}))\\
oo = 
strCAT(
addSep2StrList(o,\!\!\mattt{
\mbox{\texttt{" , "}}}))\\
s = \enlist{ii,oo} 
\IN s 
\TEL 
\end{array} \right)_{n \in 
dom(a)}\\
c = 
STRsetSort(
dom(b))\\
d = 
length(c)\\
e = 
seqSubl(c,1,
d / 2)\\
f = 
seqSubl(c,

d / 2 + 1,

d / 2 + 1)\\
g = 
listByIndex(b,e)\\
h = 
listByIndex(b,f)\\
j = \enlist{
flat(x) \asor x \in g}\\
k = \enlist{
flat(x) \asor x \in h} 
\IN \left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"@Name"}}} \\ i 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"@State"}}} \\ 
Sets2STR(
StInherit(i,db)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"@LActions"}}} \\ j 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"@RActions"}}} \\ k 
\end{array}\!\! \right) \right) 
\TEL}{\left(  \right)}
\end{array}$

\traco

$\begin{array}{l}
INIT: \tfunc{SYM} \\ INIT() \deff \\ \rule{3ex}{0pt}  db' = \left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"RSC"}}} \\ 
Comp(Comp,\left(  \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"RD"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"WR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"NOP"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"EQL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FSET"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"RSC"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INIT"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"REM"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"GET"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"EMPTY"}}} \\ 
Func(\emptylist,\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"TEST"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FFUN"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"RSC"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INIT"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"REM"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"EMPTY"}}} \\ 
Func(\emptylist,\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FIND"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"MSET"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FFUN"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"MUL"}}} \\ 
Func(\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"DIF"}}} \\ 
Func(\enlist{
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}))},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ADD"}}} \\ 
Func(\enlist{
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}))},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"BREL"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FSET"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Times(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"REMR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"REML"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}))}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\enlist{
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}))}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FFSET"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FSET"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"HIST"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\enlist{
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}))}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"REN"}}} \\ 
Func(\enlist{
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}))},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"JOIN"}}} \\ 
Func(\enlist{
Pow(
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})))},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ORDER"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"BREL"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"RCLOSE"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SCLOSE"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"TCLOSE"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"QSET"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FSET"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INIT"}}} \\ 
Func(\enlist{
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}))},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"EQU"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ETEST"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"CLASS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}))}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SEQ"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"RSC"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
List(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INIT"}}} \\ 
Func(\emptylist,\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"EMPTY"}}} \\ 
Func(\emptylist,\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"BOOL"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FLIST"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"SEQ"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
List(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"CONS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"HEAD"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"TAIL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"GET"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"STACK"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"SEQ"}}},\left(  \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"PUSH"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"TOP"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"POP"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"QUEUE"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"SEQ"}}},\left(  \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ENQ"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FRONT"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"DEQ"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"TEXT"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FLIST"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
List(
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"DEL"}}} \\ 
Func(\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"READ"}}} \\ 
Func(\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FAMILY"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FFUN"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"JOIN"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"LEAVE"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"PQUEUE"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FFUN"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
List(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ENQ"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FRONT"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"DEQ"}}} \\ 
Func(\emptylist,\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"PQUEUEMK"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"PQUEUE"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ 
Times(
Var(\!\!\mattt{
\mbox{\texttt{"A1"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"A2"}}})) 
\end{array}\!\! \right) \right),\left(  \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"QFUN"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FFUN"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Ffun(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"DEL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FIND"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FDEP"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FFUN"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Times(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})},\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})}) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"INS"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}),
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FDMO"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FDEP"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ 
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ADDONL"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}))},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"NEW"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}})),
Var(\!\!\mattt{
\mbox{\texttt{"C"}}})},\emptylist) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"FDMONAT"}}} \\ 
Comp(\!\!\mattt{
\mbox{\texttt{"FDMO"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"C"}}} \\ 
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}}) 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ADDONR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SUBONR"}}} \\ 
Func(\enlist{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}}),
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\emptylist) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELONR"}}} \\ 
Func(\enlist{
Cons(\!\!\mattt{
\mbox{\texttt{"NAT"}}})},\enlist{
Pow(
Var(\!\!\mattt{
\mbox{\texttt{"B"}}}))}) 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"BAMS"}}} \\ 
RComp(\!\!\mattt{
\mbox{\texttt{"FDMONAT"}}},\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"A"}}} \\ \!\!\mattt{
\mbox{\texttt{"AccId"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"B"}}} \\ \!\!\mattt{
\mbox{\texttt{"AccHolder"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"C"}}} \\ \!\!\mattt{
\mbox{\texttt{"Amount"}}} 
\end{array}\!\! \right) \right),\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"NEW"}}} \\ \!\!\mattt{
\mbox{\texttt{"OpenAccount"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ADDONL"}}} \\ \!\!\mattt{
\mbox{\texttt{"AddAccHolders"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"ADDONR"}}} \\ \!\!\mattt{
\mbox{\texttt{"Credit"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SUBONR"}}} \\ \!\!\mattt{
\mbox{\texttt{"Withdraw"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"SELONR"}}} \\ \!\!\mattt{
\mbox{\texttt{"GoodCostumers"}}} 
\end{array}\!\! \right) \right)) 
\end{array}\!\! \right) \right)
\end{array}$

\traco

$\begin{array}{l}
StInherit:IdComp \times Db \tfunc{Sets} \\ StInherit(i,db) \deff \\ \rule{3ex}{0pt}  
\COND{
i \in 
dom(db)}{
\LET 
c =  db(i)\\
a = 
F(c)\\
s = 
\COND{\is{Comp}(c)}{
St(c)}{ 
\star\hookrightarrow Var (
St(c))} 
\IN 
\COND{\is{nil}(a)}{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}{
SetsSubst(
StInherit(a,db),s)} 
\TEL}{
Var(\!\!\mattt{
\mbox{\texttt{"A"}}})}
\end{array}$

\traco

$\begin{array}{l}
AcInherit:IdComp \times IdAccao \pfunc{IdAccao} \times Db \tfunc{Actions} \\ AcInherit(i,r,db) \deff \\ \rule{3ex}{0pt}  
\LET 
x = 
\COND{
i \in 
dom(db)}{
\LET 
c =  db(i)\\
a = 
F(c)\\
s = 
St(c) 
\IN 
A(c) \plus 
\COND{\is{nil}(a)}{\left(  \right)}{
\LET 
f = 
AcInherit(a,\left(  \right),db) 
\IN 
ActionsSubst(f,s) 
\TEL} 
\TEL}{\left(  \right)} 
\IN 
Rename(r,x) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
Comp2TeX:IdCom \times Db \tfunc{TeX} \\ Comp2TeX(i,db) \deff \\ \rule{3ex}{0pt}  
\COND{
i \in 
dom(db)}{
\LET 
m = 

strlen(i) + 2\\
a = 
AcInherit(i,\left(  \right),db)\\
b = 
dom(a)\\
c = 
card(b)\\
d = 
div(c,2)\\
e = 
index(\left( \begin{array}{c}
 x \\ x 
\end{array} \right)_{x \in b})\\
f = 
seqSubl(e,1,d)\\
g = 
seqSubl(e,
d + 1,
c - d)\\
h = 

d \times 2 + 10\\
k = \enlist{
\LET 
x = 
nth(i,f)\\
\_ = 
princ(i,x) 
\IN 
TeXCmd(
\COND{

O( a(x)) = \emptylist}{\!\!\mattt{
\mbox{\texttt{"newrpin"}}}}{\!\!\mattt{
\mbox{\texttt{"newrpout"}}}},\enlist{0,
i \times 2,x}) 
\TEL \asor i \in 
inseq(
length(f))}\\
l = \enlist{
\LET 
x = 
nth(i,g) 
\IN 
TeXCmd(
\COND{

O( a(x)) = \emptylist}{\!\!\mattt{
\mbox{\texttt{"newrpin"}}}}{\!\!\mattt{
\mbox{\texttt{"newrpout"}}}},\enlist{m,
i \times 2,x}) 
\TEL \asor i \in 
inseq(
length(g))} 
\IN \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"begin"}}},\enlist{\!\!\mattt{
\mbox{\texttt{"interface"}}},i,m,h})} \conc k \conc l \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"end"}}},\enlist{\!\!\mattt{
\mbox{\texttt{"interface"}}}})} 
\TEL}{\emptylist}
\end{array}$

\traco

$\begin{array}{l}
DUMP: \tfunc{VOID} \\ DUMP() \deff \\ \rule{3ex}{0pt}  
\LET 
f = 
\LAMBDA{k,db}
\LET 
x =  db(k)\\
p = 
F(x)\\
s = 
StInherit(k,db)\\
a = 
A(x)\\
l = \enlist{
\COND{\is{nil}(p)}{\!\!\mattt{
\mbox{\texttt{""\}\}\{$\backslash$enlist\{$\backslash$!$\backslash$!$\backslash$mattt\{
"}}#include \mbox{\texttt{"\},p $\backslash$conc $\backslash$!$\backslash$!$\backslash$mattt\{
"}}.cam\mbox{\texttt{"\}\}\},$\backslash$emptylist,$\backslash$enlist\{$\backslash$!$\backslash$!$\backslash$mattt\{
"}}; Creation date: "}} \conc 
ioReadPipe(\!\!\mattt{
\mbox{\texttt{"date"}}},\!\!\mattt{
\mbox{\texttt{""\}),$\backslash$emptylist,$\backslash$enlist\{$\backslash$!$\backslash$!$\backslash$mattt\{
"}}STATE st: "},
Sets2STR(s)},\enlist{\!\!\mattt{
\mbox{\texttt{"  INV i(st);"}}}},\emptylist} \conc \enlist{
\LET 
g = 
\LAMBDA{i}
chr(
96 + i)\\
i = 
I( a(k))\\
o = 
O( a(k))\\
j =  
g \hookrightarrow\star (
seq2ff(i))\\
m = 
seqAddSep(\enlist{\!\!\mattt{
\mbox{\texttt{"st"}}}} \conc \enlist{k \asor k \in 
dom(j)},\!\!\mattt{
\mbox{\texttt{","}}})\\
p = 
seq2ff(o) 
\IN 
txtAddNL(\enlist{\enlist{\!\!\mattt{
\mbox{\texttt{"FUNC "}}},k,\!\!\mattt{
\mbox{\texttt{"("}}},
seqAddSep(\enlist{\enlist{s,\!\!\mattt{
\mbox{\texttt{": "}}},
Sets2STR( j(s))} \asor s \in 
dom(j)},\!\!\mattt{
\mbox{\texttt{", "}}}),\!\!\mattt{
\mbox{\texttt{"): "}}},
\COND{
o = \emptylist}{\!\!\mattt{
\mbox{\texttt{"VOID"}}}}{
Sets2STR(
hd(o))}},\enlist{\!\!\mattt{
\mbox{\texttt{"PRE    p("}}},m,\!\!\mattt{
\mbox{\texttt{")"}}}},\enlist{\!\!\mattt{
\mbox{\texttt{"STATE  st <- f("}}},m,\!\!\mattt{
\mbox{\texttt{")"}}}},\enlist{\!\!\mattt{
\mbox{\texttt{"RETURN g("}}},m,\!\!\mattt{
\mbox{\texttt{");"}}}}}) 
\TEL \asor k \in 
dom(a)} 
\IN 
txtFlat(
txtAddNL(l)) 
\TEL 
\IN 
foreach(k,\enlist{x \asor x \in 
dom(db) \wedge \is{Comp}( db(x))},
ioTxt2File(\!\!\mattt{
\mbox{\texttt{"/tmp/"}}} \conc k \conc \!\!\mattt{
\mbox{\texttt{".cam"}}},
f(k,db))) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
MComp2Comp:MComp \tfunc{Comp} \\ MComp2Comp(x) \deff \\ \rule{3ex}{0pt}  
\COND{\is{Comp}(x)}{x}{
\LET 
c = 
C(x)\\
s = 
St(x)\\
a = 
A(x) 
\IN 
\COND{
c \in 
dom(db)}{
\LET 
d = 
MComp2Comp( db(c)) 
\IN 
Comp(
F(d), 
\star\hookrightarrow Var (s),
\LET 
b = 
A(d) 
\IN \left(  \right) 
\TEL) 
\TEL}{ db(\!\!\mattt{
\mbox{\texttt{"RSC"}}})} 
\TEL}
\end{array}$

\traco

$\begin{array}{l}
Rename(r,t) \deff \\ \rule{3ex}{0pt} 
t \mapds 
dom(r) \plus \left( \begin{array}{c}
  r(a) \\  t(a) 
\end{array} \right)_{a \in 
dom(r) \cap 
dom(t)}
\end{array}$

\traco
\end{document}
