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

\INCLUDE{mon.cam}
\INCLUDE{int.cam}
\INCLUDE{ff.cam}
\INCLUDE{tex.cam}
$\begin{array}{l}
mseMax:A \pfunc{NAT} \times A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ mseMax(m,n) \deff \\ \rule{3ex}{0pt}  
monff(m,n,max)
\end{array}$

\traco

$\begin{array}{l}
mseCup:A \pfunc{NAT} \times A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ mseCup(m,n) \deff \\ \rule{3ex}{0pt}  
monff(m,n,add)
\end{array}$

\traco

$\begin{array}{l}
mseDiff:A \pfunc{NAT} \times A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ mseDiff(m,n) \deff \\ \rule{3ex}{0pt}  
m \mapds 
dom(n) \plus \left( \begin{array}{c}
 a \\ 
 m(a) -  n(a) 
\end{array} \right)_{a \in 
dom(m) \cap 
dom(n) \wedge 
 m(a) >  n(a)}
\end{array}$

\traco

$\begin{array}{l}
mseExMul:NAT \times A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ mseExMul(n,m) \deff \\ \rule{3ex}{0pt}  
\LET 
f = 
\LAMBDA{x}
x \times n 
\IN  
\star\hookrightarrow f (m) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
mseCUP:{A \pfunc{NAT}^{\star}} \tfunc{A \pfunc{NAT}} \\ mseCUP(l) \deff \\ \rule{3ex}{0pt}  mseCup-red(\left(  \right),l)
\end{array}$

\traco

$\begin{array}{l}
mseMul:A \pfunc{NAT} \times A \pfunc{NAT} \tfunc{A \pfunc{Nat}} \\ mseMul(m,n) \deff \\ \rule{3ex}{0pt}  
monff(m,n,mul)
\end{array}$

\traco

$\begin{array}{l}
mseSumRan:A \pfunc{NAT} \tfunc{NAT} \\ mseSumRan(f) \deff \\ \rule{3ex}{0pt}  
intSUM(\enlist{ f(x) \asor x \in 
dom(f)})
\end{array}$

\traco

$\begin{array}{l}
mseWam:NAT \pfunc{NAT} \times NAT \tfunc{NAT} \\ mseWam(ms,p) \deff \\ \rule{3ex}{0pt}  

intSUM(\enlist{

 ms(n) \times n \times 
intPot(10,p) \asor n \in 
dom(ms)}) / 
mseSumRan(ms)
\end{array}$

\traco

$\begin{array}{l}
msePerc:A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ msePerc(ms) \deff \\ \rule{3ex}{0pt}  
\LET 
t = 
mseSumRan(ms) 
\IN \left( \begin{array}{c}
 x \\ 
intPerc( ms(x),t,0) 
\end{array} \right)_{x \in 
dom(ms)} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
mseUnif:A \pfunc{A} \times A \pfunc{NAT} \tfunc{A \pfunc{NAT}} \\ mseUnif(ff,ms) \deff \\ \rule{3ex}{0pt}  
\LET 
f = 
ffinv(ff) 
\IN \left( \begin{array}{c}
 x \\ 
mseSumRan(
ms \mapdr  f(x)) 
\end{array} \right)_{x \in 
dom(f)} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
mseCupSeq:{A \pfunc{NAT}^{\star}} \times {A \pfunc{NAT}^{\star}} \tfunc{{A \pfunc{NAT}^{\star}}} \\ mseCupSeq(l,n) \deff \\ \rule{3ex}{0pt}  
monseq(l,n,mseCup)
\end{array}$

\traco

$\begin{array}{l}
mseCUPSEQ:{{A \pfunc{NAT}^{\star}}^{\star}} \tfunc{{A \pfunc{NAT}^{\star}}} \\ mseCUPSEQ(l) \deff \\ \rule{3ex}{0pt}  mseCupSeq-red(\emptylist,l)
\end{array}$

\traco

$\begin{array}{l}
mse2TeXbarenv:A \pfunc{NAT} \tfunc{TeX} \\ mse2TeXbarenv(ms) \deff \\ \rule{3ex}{0pt}  
\LET 
m = 
intMAX(
ran(ms))\\
a = 
m / 10\\
b = 
\COND{
a = 0}{1}{a}\\
c = 
1800 / m\\
d = 
\COND{
c = 0}{1}{
\COND{
c \geq 250}{250}{c}}\\
x = 
div(d,10)\\
y = 
rem(d,10)\\
e = 
\COND{
m > 999}{28}{
\COND{
m > 99}{23}{
\COND{
m > 9}{18}{13}}} 
\IN \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"setlength"}}},\enlist{
texCons(\!\!\mattt{
\mbox{\texttt{"unitlength"}}}),\!\!\mattt{
\mbox{\texttt{".2mm"}}}}),
TeXCmd(\!\!\mattt{
\mbox{\texttt{"begin"}}},\enlist{\!\!\mattt{
\mbox{\texttt{"barenv"}}}})} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"setdepth"}}},\enlist{11})} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"setwidth"}}},\enlist{e})} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"setstretch"}}},\enlist{
itoa(x) \conc \!\!\mattt{
\mbox{\texttt{"."}}} \conc 
itoa(y)})} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"setyaxis"}}},\enlist{0,

a + 1 \times 10,b})} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"bar"}}},\enlist{ ms(x),1,
Opt(x)}) \asor x \in 
dom(ms)} \conc \enlist{
TeXCmd(\!\!\mattt{
\mbox{\texttt{"end"}}},\enlist{\!\!\mattt{
\mbox{\texttt{"barenv"}}}})} 
\TEL
\end{array}$

\traco
\end{document}
