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

$\begin{array}{l}
seqCata:B \times AxB \pfunc{B} \times {A^{\star}} \tfunc{B} \\ seqCata(c,f,l) \deff \\ \rule{3ex}{0pt}  
\COND{
l = \emptylist}{c}{
f(
hd(l),
seqCata(c,f,
tl(l)))}
\end{array}$

\traco

$\begin{array}{l}
seqInseg:NAT \tfunc{{NAT^{\star}}} \\ seqInseg(n) \deff \\ \rule{3ex}{0pt}  
\COND{
n = 0}{\emptylist}{
seqInseg(
n - 1) \conc \enlist{n}}
\end{array}$

\traco

$\begin{array}{l}
seqSubl:{A^{\star}} \times NAT \times NAT0 \tfunc{{A^{\star}}} \\ seqSubl(l,i,n) \deff \\ \rule{3ex}{0pt}  
\COND{
n = 0}{\emptylist}{
\COND{
l = \emptylist}{\emptylist}{
\LET 
h = 
hd(l)\\
t = 
tl(l) 
\IN 
\COND{
i = 1}{\enlist{h} \conc 
seqSubl(t,i,
n - 1)}{
seqSubl(t,
i - 1,n)} 
\TEL}}
\end{array}$

\traco

$\begin{array}{l}
seqAddSep:{A^{\star}} \times A \tfunc{{A^{\star}}} \\ seqAddSep(l,a) \deff \\ \rule{3ex}{0pt}  
\COND{
l = \emptylist}{\emptylist}{\enlist{
hd(l)} \conc 
\conc (\enlist{\enlist{a,x} \asor x \in 
tl(l)})}
\end{array}$

\traco

$\begin{array}{l}
seq2mset:{A^{\star}} \tfunc{A \pfunc{NAT}} \\ seq2mset(l) \deff \\ \rule{3ex}{0pt}  \left( \begin{array}{c}
 x \\ 
length(\enlist{y \asor y \in l \wedge 
y = x}) 
\end{array} \right)_{x \in 
elems(l)}
\end{array}$

\traco

$\begin{array}{l}
seqInv:{A^{\star}} \tfunc{{A^{\star}}} \\ seqInv(l) \deff \\ \rule{3ex}{0pt}  
\COND{
l = \emptylist}{\emptylist}{
seqInv(
tl(l)) \conc \enlist{
hd(l)}}
\end{array}$

\traco

$\begin{array}{l}
seqBlast:{A^{\star}} \tfunc{{A^{\star}}} \\ seqBlast(l) \deff \\ \rule{3ex}{0pt}  
seqInv(
tl(
seqInv(l)))
\end{array}$

\traco

$\begin{array}{l}
seq2mseSeq:{A^{\star}} \tfunc{{A \pfunc{NAT}^{\star}}} \\ seq2mseSeq(l) \deff \\ \rule{3ex}{0pt}  \enlist{\left( \left(\!\! \begin{array}{c}
 x \\ 1 
\end{array}\!\! \right) \right) \asor x \in l}
\end{array}$

\traco

$\begin{array}{l}
set2seq:{\set{A}} \tfunc{{A^{\star}}} \\ set2seq(s) \deff \\ \rule{3ex}{0pt}  \enlist{a \asor a \in s}
\end{array}$

\traco

$\begin{array}{l}
seq2ff:{A^{\star}} \tfunc{NAT \pfunc{A}} \\ seq2ff(l) \deff \\ \rule{3ex}{0pt}  \left( \begin{array}{c}
 x \\ 
nth(x,l) 
\end{array} \right)_{x \in 
\inseg{
length(l)}}
\end{array}$

\traco

$\begin{array}{l}
seqSplit:{A^{\star}} \times NAT \tfunc{{{A^{\star}}^{\star}}} \\ seqSplit(l,n) \deff \\ \rule{3ex}{0pt}  
\LET 
c = 
length(l)\\
i = 
c / n\\
m = 
\COND{

rem(c,n) = 0}{i}{
i + 1} 
\IN \enlist{
seqSubl(l,


j - 1 \times n + 1,n) \asor j \in 
seqInseg(m)} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
seqDiff:{A^{\star}} \times {A^{\star}} \tfunc{{A^{\star}}} \\ seqDiff(s,r) \deff \\ \rule{3ex}{0pt}  \enlist{a \asor a \in s \wedge 
\neg 
a \in 
elems(r) }
\end{array}$

\traco

$\begin{array}{l}
seqUpdate:A \times B \times {A^{\star}} \tfunc{{A^{\star}}} \\ seqUpdate(x,d,l) \deff \\ \rule{3ex}{0pt}  \enlist{
\COND{
a = x}{d}{a} \asor a \in l}
\end{array}$

\traco
\end{document}
