
\begin{figure}

\boxfig{
\begin{center}
\fbox{$\eiJudge{H}{t}{H}{t'}{\setof{\alpha}}$}
\end{center}

\[	\begin{array}{ll}
	\alpha	& 	::= \rcreate~ o
			~|~ \rtest~ o
			~|~ \ralloc~ l^\rho
			~|~ \rread~ l^\rho
			~|~ \rwrite~ l^\rho
	\end{array}
\]


\[	\ruleAL	{EiVal}
		{\eiJudge
			{H}{v^\circ}
			{H}{v^\circ}
			{\emptyset}}
\]

\[	\ruleIL	{EiAppT}
		{ \eiJudge
			{H_0}	{t_1}
			{H_1}	{\teLAM{a}{\kappa}{t_{12}}}
			{B_1}
		  \quad
		  \eiJudge
			{H_1}	{t_{12}[\varphi_2/a]}
			{H_2}	{v^\circ}
			{B_2}
		}
		{ \eiJudge
			{H_0}	{t_1~ \varphi_2}
			{H_2}	{v^\circ}
			{B_1 \cup B_2}
		}
\]

\[	\ruleIL	{EiApp}
		{ \begin{array}{cc}
		  &
		  \hspace{2.8em}
		  \eiJudge
			{H_1}	{t_2}
			{H_2}	{v_2^\circ}
			{B_2}
		  \\
		  \eiJudge
			{H_0}	{t_1}
			{H_1}	{\teLam{x}{\tau}{t_{12}}}
			{B_1} 
		  &
		  \eiJudge
			{H_2}	{t_{12}[v_2^\circ/x]}
			{H_3}	{v_3^\circ}
			{B_3}
		  \end{array}
		}
		{ \eiJudge
			{H_0}	{t_1~ t_2}
			{H_3}	{v_3^\circ}
			{B_1 \cup B_2 \cup B_3}
		}
\]

\[	\ruleIL	{EiLetR}
		{ \begin{array}{ll}
		  \rho~ \trm{fresh} 
		  \quad
		  \ov{\Delta_i = \trm{witOf} (\delta_i[\un{\rho}/x])}^{~i}
		  \quad
		  \ov{\pi_i = \trm{propOf} (\delta_i[\un{\rho}/x])}^{~i}
		  \\
		  \eiJudge
		 	{H_0,~ \rho,~ \ov{\pi_i}}
				{\teWithR
					{\un{\rho}}
					{\ov{\Delta_i}}
					{t[\un{\rho}/x~~ \ov{\Delta_i/w_i}]}}
			{H_1}	{v^\circ}
			{B_1}
		  \end{array}
		}
		{ \eiJudge
			{H_0}	{\teLetR{r}{\ov{w_i = \delta_i}}{t}}
			{H_1}	{v_\circ}
			{B_1 \cup \setof{\rcreate~ \rho} \cup \ov{\rcreate~ \pi_i}}
		}
\]

\[	\ruleIL	{EiWithR}
		{ \eiJudge
			{H_0}	{t}
			{H_1}	{v^\circ}
			{B_1}
		}
		{ \eiJudge
			{H_0}	{\teWithR{\un{\rho}}{\ov{\Delta_i}}{t}}
			{H_1}	{v^\circ}
			{B_1}
		}
\]

\[	\ruleIL	{EiAlloc}
		{ \ov{ \eiJudge
			{H_j}		{t_j}
			{H_{j+1}}	{v_j^\circ}
			{B_j}
		     }^{~ j \;\gets\; 0..n}
		  \quad
		  \rho \in H_{n+1}
		  \quad
		  l~ \trm{fresh}
		}
		{ \eiJudge
			{H_0}		{K~ \un{\rho}~ \ov{\varphi_i'}~ \ov{t_j}}
			{H_{n+1},~ l \mtoa{\rho} C_k~ \ov{v_j^\circ}}
					{l}
			{\bigcup \ov{B_j}~ \cup B' \cup \setof{\rtest~ \rho} }
		}
\]\vspace{-1em}
\[	B' = \left\{
	\begin{array}{cll}
	\setof{\ralloc~ l^\rho} & \rif~~ \rmutable~ \rho \in H_{n+1}, \\
	\emptyset 		& \trm{otherwise}.
	\end{array}\right.
\]

\[	\ruleIL	{EiCase}
		{ \eiJudge
			{H_0}	{t}
			{H_1[l \mtoa{\rho} C_k~ \ov{u^\circ}]}	{l}
			{B_1}
		  \quad
		  \eiJudge
			{H_1}	{t'[\ov{u^\circ/x}]}
			{H_2}	{v^\circ}
			{B_2}
		}
		{ \eiJudge
			{H_0}	{\kcase~ t~ \kof~ ... K~ \ov{x} \to t' ...}
			{H_1}	{v^\circ}
			{B_1 \cup B_2 \cup B_3}
		}
\]\vspace{-1em}
\[	B_3 = \left\{
	\begin{array}{cll}
	\setof{\rread~ l^\rho} 	& \rif~~ \rmutable~ \rho \in H_2, \\
	\emptyset 		& \trm{otherwise}.
	\end{array}\right.
\]

\[	\ruleIL	{EiUpdate}
		{ \begin{array}{ll}
		  \eiJudge
			{H_0}	{t_1}
			{H_1}	{l}
			{B_1}
		  \qq \qq\qq 	B_3  = B_1 \cup B_2 \cup \setof{\rtest~ (\rmutable~ \rho),~ \rwrite~ l^\rho}
		  \\
		  \eiJudge
			{H_1}	{t_2}
			{H_2[~\rmutable~ \rho,~ l \mtoa{\rho} C_k~ \ov{v^\circ}~]}
				{u^\circ}
			{B_2~}
		  \quad
			H_2' = H_2,~ l \mtoa{\rho} C_K~ v_0^\circ ... u_i^\circ ... v_n^\circ
		  \end{array}
		}
		{ \eiJudge
			{H_0}	{\rupdate_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~ t_1~ t_2~}
			{H_2'}	{()}
			{B_3}
		}
\]


\[	\ruleIL	{EiSuspend}
		{ \begin{array}{ll}
		  \hspace{0.1em}
		  \wiJudge{H_0}{\delta}{\rpure~ \sigma}{B_4}
		  & 
		  \hspace{2.75em}
		  \eiJudge
			{H_1}	{t_2}
			{H_2}	{v_2^\circ}
			{B_2}
		  \\
		  \eiJudge
			{H_0}	{t_1}
			{H_1}	{\teLam{x}{\tau_{11}}{t_{12}}}
			{B_1}
		  &
		  \eiJudge
			{H_2}	{t_{12}[v_2^\circ/x]}
			{H_3}	{v_3^\circ}
			{B_3}
		  \end{array}
		} 
		{ \eiJudge
		 	{H_0}	{\rsuspend~ \tau_1~ \tau_2~ \delta~ \sigma~ t_1~ t_2}
			{H_3}	{v_3^\circ}
			{B_1 \cup B_2 \cup B_3 \cup B_4}
		}
\]	

\[	\ruleIL	{EiMask}
		{ \wiJudge{H_0}{\delta}{\rpure~ \sigma}{B_1}
		  \quad
		  \eiJudge
			{H_0}	{t}
			{H_1}	{v^\circ}
			{B_2}
		}
		{ \eiJudge
			{H_0}	{\kmask~ \delta~ \kin~ t}
			{H_1}	{v^\circ}
			{B_1 \cup B_2}	
		}
\]
} % boxfig
\smallskip
\caption{Natural Semantics}
\label{fig:NaturalSemantics}

\end{figure}











