\documentstyle[12pt]{article}
\input mssymb                                 
\input /jj/kt/tex/fixqmsfonts
\input /jj/kt/tex/laktex
\input /jj/kt/tex/illustrations
\input /var/arvind/idcompiler/macros/prelude

\begin{document}

\pagestyle{empty}

{\large
${\tt S}[\![ {\sf \lambda_{n,m}} \; (\mv{X_n}). \{_{\sf m}\; \begin{array}[t]{lll} 
Y_1 & = &  Se_1\\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_n & = &  Se_n \\
Y_{n+1} & = &  Nse_1 \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_{n+m} & = &  Nse_m \\
\multicolumn{3}{c}{C_1} \\
\multicolumn{3}{c}{ \vdots }\\
\multicolumn{3}{c}{C_k}\\
\multicolumn{3}{l}{ \;\;  \; {\sf In} \; \mv{R_m} \} ]\!]}
\end{array} =
\begin{array}[t]{l}
{\sf \lambda_{n,m+1}}\; (\mv{X_n})\;. \\
\hspace{0.2cm}{
( \{_{\sf m+1}\; \begin{array}[t]{lll}
Y_1 & = &  Se_1\\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_n & = &  Se_n \\
Y_{n+1}, \; S_1 & = &  {\tt SE}[\![Nse_1]\!] \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_{n+m},\;S_m & = &  {\tt SE}[\![ Nse_m]\!] \\
S_{m+1} & = & {\tt SC}[\![ C_1]\!];  \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
S_{m+k} & = & {\tt SC}[\![ C_k]\!]; \\
S' & = & {\sf Sync_{m+k+i}} \; (Deadvariables, \; \mv{S_{m+k}} )    \\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; \mv{R_m} ,\; S' \} ) }  
\end{array} }
\end{array}$\\
}



\blank
\noindent
{\large
${\tt SE}[\![ {\sf WLoop_{n}} \; (P,B,\mv{Y_n}, Y) ]\!] = 
{\sf WLoop_{n}'} \; (P,B,\mv{Y_n}, S_p, Y) $\\
}


 
\blank
\noindent
{\large
${\tt SE}[\![ {\sf Ap_{n,m}} \; (F,\;\mv{X_n}) ]\!] = 
{\sf Ap_{n,m+1}} \; (F,\;\mv{X_n}) $
}

\blank
\noindent
{\large
${\tt SC}[\![ {\sf P\_store} \; (X,\;I\;Z) ]\!] = 
 {\sf Ack\_store} \; (X,\;I\;Z) $\\
}


\newpage


\blank 
\noindent
{\large
$\begin{array}{lll}
\\
\hspace{0.5cm}{\sf WLoop_n'} \; (P, \; B, \; \mv{X_n}, S, \; {\sf True}) & \reduce{}{} &
\{_{\sf n+1} \begin{array}[t]{lll}
 \mv{t_n}, S_b & = & {\sf Ap_{n,{n+1}}} \; (B, \;  \mv{X_n}) ;\\
  t_{p}, S_p & = & {\sf Ap_{n,2}} \; (P, \; \mv{t_n});\\
 S'         & = & {\sf Sync_3} \; (S, \; S_b, \; S_p) ; \\
\mv{t_n'}, S_l & = & {\sf WLoop_n'} \;(P,  \; B,   \; \mv{t_n}, \;S',\; t_{p})  \\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_n'} , \; S_l \} }
\end{array}
\\
\\
\hspace{0.5cm}{\sf WLoop_n'} \; (P, \; B, \;  \mv{X_n}, \; S, \; {\sf False}) & \reduce{}{} &
\mv{X_n}, \; S  
\end{array}$ \\
}


\blank
\noindent
{\small
$ \hspace{0.5cm}{\begin{array}{lll}
{\sf Ack\_store} \;( L ,\; \underline{i}, \; V) & \reduce{}{} &
\begin{array}[t]{l}
\{ t = {\sf Signal};\\
\; {\sf P\_store} \;( L, \; \underline{i}, \; V); \\
\;\;\; {\sf In} \; t \}
\end{array}
\end{array}}$ }

\blank
\noindent
{\small
$ \hspace{0.5cm}{\begin{array}{lll}
{\sf Sync_n} \;( \mv{V_n}) & \reduce{}{} & ()
\end{array}}
$} \\

\end{document} 
