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

$\begin{array}{l}
\_fn' = \!\!\mattt{
\mbox{\texttt{"sets.cam"}}}
\end{array}$\\


$\begin{array}{l}
flat(l) \deff \\ \rule{3ex}{0pt} 
\conc (\enlist{
\COND{

\is{str}(x) \vee \is{int}(x) \vee \is{SYM}(x)}{\enlist{x}}{
flat(x)} \asor x \in l})
\end{array}$

\traco

$\begin{array}{l}
i1(x) \deff \\ \rule{3ex}{0pt} \enlist{1,x}
\end{array}$

\traco

$\begin{array}{l}
i2(x) \deff \\ \rule{3ex}{0pt} \enlist{2,x}
\end{array}$

\traco

$\begin{array}{l}
j606o(y) \deff \\ \rule{3ex}{0pt} 
\LET 
a = 
\pi_1(y)\\
b = 
\pi_2(y)\\
k = 
\pi_1(b)\\
x = 
\pi_2(b) 
\IN \enlist{k,\enlist{a,x}} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
nilit(x) \deff \\ \rule{3ex}{0pt} \enlist{x,nil}
\end{array}$

\traco

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

\traco

$\begin{array}{l}
PLUS(s) \deff \\ \rule{3ex}{0pt} plus-red(\left(  \right),s)
\end{array}$

\traco

$\begin{array}{l}
prod(f,g) \deff \\ \rule{3ex}{0pt} 
\LAMBDA{t}\enlist{
f(
\pi_1(t)),
g(
\pi_2(t))}
\end{array}$

\traco

$\begin{array}{l}
const(f,g) \deff \\ \rule{3ex}{0pt} 
\LAMBDA{x}\enlist{
f(x),
g(x)}
\end{array}$

\traco

$\begin{array}{l}
comp(f,g) \deff \\ \rule{3ex}{0pt} 
\LAMBDA{x}
f(
g(x))
\end{array}$

\traco

$\begin{array}{l}
Kons(c) \deff \\ \rule{3ex}{0pt} 
\LAMBDA{x}c
\end{array}$

\traco

$\begin{array}{l}
id(x) \deff \\ \rule{3ex}{0pt} x
\end{array}$

\traco

$\begin{array}{l}
curry:AxB \pfunc{C} \tfunc{A \pfunc{(B \pfunc{C})}} \\ curry(f) \deff \\ \rule{3ex}{0pt}  
\LET 
X = 
dom(f)\\
Y =  
p1\hbox{-set} (X) 
\IN \left( \begin{array}{c}
 a \\ \left( \begin{array}{c}
 
\pi_2(p) \\  f(p) 
\end{array} \right)_{p \in X \wedge 

\pi_1(p) = a} 
\end{array} \right)_{a \in Y} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
uncurry:A \pfunc{(B \pfunc{C})} \tfunc{AxB \pfunc{C}} \\ uncurry(f) \deff \\ \rule{3ex}{0pt}  
PLUS(\{
\LET 
g =  f(a) 
\IN \left( \begin{array}{c}
 \enlist{a,b} \\  g(b) 
\end{array} \right)_{b \in 
dom(g)} 
\TEL \asor a \in 
dom(f)\})
\end{array}$

\traco

$\begin{array}{l}
ffAset(s) \deff \\ \rule{3ex}{0pt} \left( \begin{array}{c}
 a \\ nil 
\end{array} \right)_{a \in s}
\end{array}$

\traco

$\begin{array}{l}
join(f1,f2) \deff \\ \rule{3ex}{0pt} \left( \begin{array}{c}
 a \\ \enlist{ f1(a), f2(a)} 
\end{array} \right)_{a \in 
dom(f1) \cap 
dom(f2)}
\end{array}$

\traco

$\begin{array}{l}
joinInv' = 
const(
\star\hookrightarrow p1 ,
\star\hookrightarrow p2 )
\end{array}$\\


$\begin{array}{l}
uplus(p) \deff \\ \rule{3ex}{0pt} 
\pi_1(p) \plus 
\pi_2(p)
\end{array}$

\traco

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

\traco

$\begin{array}{l}
nJoin' = 
comp(ujoin,
const(p1,
comp(uplus,
prod(
\star\hookrightarrow 
Kons(nil) ,curry))))
\end{array}$\\


$\begin{array}{l}
nJoinInv' = 
const(
\star\hookrightarrow p1 ,
comp(uncurry,
\star\hookrightarrow p2 ))
\end{array}$\\


$\begin{array}{l}
pJoinInv(f) \deff \\ \rule{3ex}{0pt} 
\LET 
a = \left( \begin{array}{c}
 
\pi_2(x) \\  f(x) 
\end{array} \right)_{x \in 
dom(f) \wedge 

\pi_1(x) = 1}\\
b = \left( \begin{array}{c}
 
\pi_2(x) \\  f(x) 
\end{array} \right)_{x \in 
dom(f) \wedge 

\pi_1(x) = 2} 
\IN \enlist{a,b} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
discollect(f) \deff \\ \rule{3ex}{0pt} 
\bigcup (\{\{\enlist{a,b} \asor b \in  f(a)\} \asor a \in 
dom(f)\})
\end{array}$

\traco

$\begin{array}{l}
collect(r) \deff \\ \rule{3ex}{0pt} \left( \begin{array}{c}
 a \\ \{
\pi_2(q) \asor q \in r \wedge 
a = 
\pi_1(q)\} 
\end{array} \right)_{a \in \{
\pi_1(p) \asor p \in r\}}
\end{array}$

\traco

$\begin{array}{l}
pair2ff(p) \deff \\ \rule{3ex}{0pt} \left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"Att1"}}} \\ 
\pi_1(p) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"Att2"}}} \\ 
\pi_2(p) 
\end{array}\!\! \right) \right)
\end{array}$

\traco

$\begin{array}{l}
ff2pair(f) \deff \\ \rule{3ex}{0pt} 
ff2seq(f,\!\!\mattt{
""})
\end{array}$

\traco

$\begin{array}{l}
mkr(f) \deff \\ \rule{3ex}{0pt} \{\enlist{a, f(a)} \asor a \in 
dom(f)\}
\end{array}$

\traco

$\begin{array}{l}
mkf(r) \deff \\ \rule{3ex}{0pt} \left( \begin{array}{c}
 
\pi_1(t) \\ 
\pi_2(t) 
\end{array} \right)_{t \in r}
\end{array}$

\traco

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

\traco

$\begin{array}{l}
f822:AxB \tfunc{BxA} \\ f822(p) \deff \\ \rule{3ex}{0pt}  \enlist{
\pi_2(p),
\pi_1(p)}
\end{array}$

\traco

$\begin{array}{l}
f870' = uncurry
\end{array}$\\


$\begin{array}{l}
f87x' = curry
\end{array}$\\


$\begin{array}{l}
flatten(r) \deff \\ \rule{3ex}{0pt} 
\bigcup (\{\{\enlist{
\pi_1(p),b} \asor b \in 
\pi_2(p)\} \asor p \in r\})
\end{array}$

\traco

$\begin{array}{l}
rcircle(r,s) \deff \\ \rule{3ex}{0pt} \{\enlist{
\pi_1(p),
\pi_2(q)} \asor p \in r, q \in s \wedge 

\pi_2(p) = 
\pi_1(q)\}
\end{array}$

\traco
\end{document}
