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

\INCLUDE{io.cam}
\INCLUDE{mse.cam}
\INCLUDE{sets.cam}
\INCLUDE{ffs.cam}
\INCLUDE{txt.cam}
\INCLUDE{sql.cam}
\SORTS

$\begin{array}{lcll}
PPD & \cong & 
\PROD S \TYPE Stock \NEXT P \TYPE Pricelist \NEXT E \TYPE EquipDb \DORP
  \\
Stock & \cong & Unid \pfunc{NAT}  \\
Pricelist & \cong & Comp \pfunc{Currency}  \\
EquipDb & \cong & Equip \pfunc{(Unid \pfunc{NAT})}  \\
Unid & \cong & {Equip + Comp}  \\
Comp & \cong & 
\PROD K \TYPE NAT \DORP
  \\
Equip & \cong & 
\PROD K \TYPE NAT \DORP
  \\
Currency & \cong & NAT  \\
NAT & \cong & int  \\
\end{array}$

\OPERS

\STATE{ppd}{PPD}
$\begin{array}{l}
Explode:Equip \tfunc{Comp \pfunc{NAT}} \\ Explode(k) \deff \\ \rule{3ex}{0pt}  
explode(k,
E(ppd))
\end{array}$

\traco

$\begin{array}{l}
CompCost:Equip \times NAT \tfunc{Comp \pfunc{NAT}} \\ CompCost(k,n) \deff \\ \rule{3ex}{0pt}  
\LET 
ms = 
mseExMul(
explode(k,
E(ppd)),n) 
\IN 
mseDiff(ms,
S(ppd)) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
explode:Equip \times EquipDb \tfunc{Comp \pfunc{NAT}} \\ explode(k,db) \deff \\ \rule{3ex}{0pt}  
\LET 
ms = 
\COND{
k \in 
dom(db)}{ db(k)}{\left(  \right)} 
\IN 
mseCUP(\enlist{
\COND{\is{Comp}(x)}{
ms \mapdr \{x\}}{
mseExMul(
explode(x,
db \mapds \{k\}), ms(x))} \asor x \in 
dom(ms)}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
Init: \tfunc{SYM} \\ Init() \deff \\ \rule{3ex}{0pt}  ppd' = 
PPD(\left( \left(\!\! \begin{array}{c}
 
Comp(11) \\ 10 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(12) \\ 5 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(13) \\ 1 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(14) \\ 20 
\end{array}\!\! \right) \right),\left(  \right),\left( \left(\!\! \begin{array}{c}
 
Equip(11) \\ \left( \left(\!\! \begin{array}{c}
 
Comp(11) \\ 1 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(12) \\ 3 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(12) \\ \left( \left(\!\! \begin{array}{c}
 
Comp(13) \\ 4 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(11) \\ 3 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(10) \\ \left( \left(\!\! \begin{array}{c}
 
Equip(11) \\ 3 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(12) \\ 2 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \right))
\end{array}$

\traco

$\begin{array}{l}
abs\_Unid(x) \deff \\ \rule{3ex}{0pt} 
\LET 
i = 
\pi_1(x)\\
y = 
\pi_2(x) 
\IN 
\COND{
i = 2}{
Comp(y)}{
Equip(y)} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
rep\_Unid(x) \deff \\ \rule{3ex}{0pt} \enlist{
\COND{\is{Comp}(x)}{2}{1},
K(x)}
\end{array}$

\traco

$\begin{array}{l}
rep0' = 
\LAMBDA{x}\enlist{\enlist{ 
rep\_Unid \hookrightarrow\star (
S(x)), 
K \hookrightarrow\star (
P(x))}, 
\star\hookrightarrow 
rep\_Unid \hookrightarrow\star  ( 
K \hookrightarrow\star (
E(x)))}
\end{array}$\\


$\begin{array}{l}
rep1' = 
prod(id,uncurry)
\end{array}$\\


$\begin{array}{l}
rep2' = 
prod(id,
j606o \hookrightarrow\star )
\end{array}$\\


$\begin{array}{l}
rep3' = 
prod(id,pJoinInv)
\end{array}$\\


$\begin{array}{l}
rep4' = 
prod(id,
prod(mkr,mkr))
\end{array}$\\


$\begin{array}{l}
rep5' = 
prod(id,
prod(
flat\hbox{-set} ,
flat\hbox{-set} ))
\end{array}$\\


$\begin{array}{l}
rep6' = 
prod(id,
prod(
seq2ff\hbox{-set} ,
seq2ff\hbox{-set} ))
\end{array}$\\


$\begin{array}{l}
rep7(t) \deff \\ \rule{3ex}{0pt} 
do(\_ppdSP' = 
\pi_1(t),
ioObjSave('\_ppdSP,
\pi_1(t)),
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_ppdEETable"}}},
\pi_1(
\pi_2(t)),\!\!\mattt{
\mbox{\texttt{"\%"}}}),
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_ppdECTable"}}},
\pi_2(
\pi_2(t)),\!\!\mattt{
\mbox{\texttt{"\%"}}}))
\end{array}$

\traco

$\begin{array}{l}
abs6to0(r) \deff \\ \rule{3ex}{0pt} 
abs0(
abs1(
abs2(
abs3(
abs4(
abs5(
abs6(r)))))))
\end{array}$

\traco

$\begin{array}{l}
rep0to6(a) \deff \\ \rule{3ex}{0pt} 
rep6(
rep5(
rep4(
rep3(
rep2(
rep1(
rep0(a)))))))
\end{array}$

\traco

$\begin{array}{l}
Explode7:Equip \tfunc{Comp \pfunc{NAT}} \\ Explode7(k) \deff \\ \rule{3ex}{0pt}  
do(
sh(\!\!\mattt{
\mbox{\texttt{"perl ppdExplode.pl "}}} \conc 
itoa(
K(k))),
ioAfsPrint(
ffsRename(\left( \left(\!\! \begin{array}{c}
 1 \\ \!\!\mattt{
\mbox{\texttt{"Comp"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ \!\!\mattt{
\mbox{\texttt{"Qty"}}} 
\end{array}\!\! \right) \right),
ioAwk2afs(\!\!\mattt{
\mbox{\texttt{"\_r"}}},\!\!\mattt{
\mbox{\texttt{"\%"}}}))))
\end{array}$

\traco

$\begin{array}{l}
Init7: \tfunc{SYM} \\ Init7() \deff \\ \rule{3ex}{0pt}  
rep7(
rep0to6(
PPD(\left( \left(\!\! \begin{array}{c}
 
Comp(11) \\ 10 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(12) \\ 5 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(13) \\ 1 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(14) \\ 20 
\end{array}\!\! \right) \right),\left(  \right),\left( \left(\!\! \begin{array}{c}
 
Equip(11) \\ \left( \left(\!\! \begin{array}{c}
 
Comp(11) \\ 1 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Comp(12) \\ 3 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(12) \\ \left( \left(\!\! \begin{array}{c}
 
Comp(13) \\ 4 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(11) \\ 3 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(10) \\ \left( \left(\!\! \begin{array}{c}
 
Equip(11) \\ 3 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 
Equip(12) \\ 2 
\end{array}\!\! \right) \right) 
\end{array}\!\! \right) \right))))
\end{array}$

\traco

$\begin{array}{l}
CompCost7:Equip \times NAT \tfunc{Comp \pfunc{NAT}} \\ CompCost7(k,n) \deff \\ \rule{3ex}{0pt}  
do(
sh(\!\!\mattt{
\mbox{\texttt{"perl ppdExplode.pl "}}} \conc 
itoa(
K(k))),
sh(\!\!\mattt{
\mbox{\texttt{"awk -f otimes.awk m="}}} \conc 
itoa(n) \conc \!\!\mattt{
\mbox{\texttt{" \_r > \_tmp0 "}}}),
princ(\!\!\mattt{
\mbox{\texttt{"(cr)[ mseExMul successfully performed at UNIX level ](cr)"}}}),
ioObjLoad('\_ppdSP),
\LET 
a =  
abs\_Unid \hookrightarrow\star (
\pi_1(\_ppdSP))\\
b = 
ioAwk2afs(\!\!\mattt{
\mbox{\texttt{"\_tmp0"}}},\!\!\mattt{
\mbox{\texttt{"\%"}}})\\
c = \left( \begin{array}{c}
 
Comp(
atoi( t(1))) \\ 
atoi( t(2)) 
\end{array} \right)_{t \in b} 
\IN 
princ(\!\!\mattt{
\mbox{\texttt{"(cr)[ Refinement memo: mseDiff still at abstract level ](cr)"}}},\!\!\mattt{
\mbox{\texttt{"(cr)Result is:(cr)"}}},
pp(
mseDiff(c,a))) 
\TEL,\!\!\mattt{
""})
\end{array}$

\traco
\end{document}
