
\begin{figure}

\boxfig{
\begin{center}
\fbox{$\evJudgeHH{t}{t'}$}
\end{center}
\begin{tabbing}
MMMMMMMMMM \= MM  	\= MM		\= MMMMMMMMM \= MMMMMMM \= MMMMM \kill
\> $E_v$ \> ::=		\> $[~ ]
				~|~ E_v~ \varphi
				~|~ E_v~ t_2
				~|~ v~ E_v$
\\[0.5ex]
\>	\> \ $|$	\> $\teWithR{\un{\rho}}{\ov{\Delta_i}}{E_v}$
\\[0.5ex]
\>	\> \ $|$	\> $\kcase \ E_v \ \kof \ \ov{\ialt}$ 
\\[0.5ex]
\>	\> \ $|$	\> $K~ \ov{\varphi}~ E_v~ t_1~ ...$ 
			\> $|~~ K \ \ov{\varphi}~ v^\circ~ E_v~ ...$
			\> $|~ ...$
\\[0.5ex]
\>	\> \ $|$	\> $\iupdate_{K,i}~ \ov{\varphi}~ E_v~ t_2$
			\> $|~~ \iupdate_{K,i}~ \ov{\varphi}~ l~ E_v$ 
\\[0.5ex]
\>	\> \ $|$	\> $\isuspend~ \ov{\varphi}~ E_v~ t_2$
			\> $|~~ \isuspend~ \ov{\varphi}~ v~ E_v$
\end{tabbing}
\[	\frac	{\evJudge{H}{t}{H'}{t'}}
		{\evJudge{H}{E_v[t]}{H'}{E_v[t']}}
		~~ \trm{(EvContext)}
\]
\[	\begin{array}{cr}
		\evJudgeHH
			{(\Lambda (a :: \kappa). \ t) \ \varphi}
			{t[\varphi/a]}
		& (\trm{EvTAppAbs})
	\\[1ex]
		\evJudgeHH
			{(\lambda (x :: \tau). \ t) \ v^\circ}
			{t[v^\circ/x]}
		& (\trm{EvAppAbs})
	\end{array}
\]

\[	\ruleIL	{EvCreateR}
		{ \rho~ \trm{fresh}
		  \quad
		  \ov{\Delta_i = \rwitOf(\delta_i[\un{\rho}/r])}^{~ i}
		  \quad
		  \ov{\pi_i    = \rpropOf(\delta_i[\un{\rho}/r])}^{~ i}
		  \quad
		  H' = H,~ \rho,~ \ov{\pi_i}
		}
		{ \evJudge
			{H}
			{\kletregion \ r \ \kwith \ \{ \ov{w_i = \delta_i} \} \ \kin \ t}
			{H'}
			{ \teWithR
				{\un{\rho}}
				{\ov{\Delta_i}}
				{t[\un{\rho}/r~ \ov{\Delta_i/w_i}]}
			}
		}
\]
\[	\ruleAL	{EvEjectR}
		{ \evJudge
		  	{H}	{\teWithR
					{\un{\rho}}
					{\ov{\Delta_i}}
					{v^\circ}}
		  	{H}	{v^\circ}
		}
\]
\[	\begin{array}{cr}
		\evJudge
			{H[\rho]}
			{K \ \un{\rho} \ \ov{\varphi} \ \ov{v^\circ}}
			{H, \ l \mtoa{\rho} C_K \ \ov{v^\circ}}
			{l \qq l \ \trm{fresh}}
		& (\trm{EvAlloc})
	\\[1ex]
		\evJudge
			{H[l \mtoa{\rho} C_K \ \ov{v^\circ}]}
			{\kcase \ l \ \kof \ ... K \ \ov{x} \to t ...}
			{H}
			{t[\ov{v^\circ / x}]}
		& (\trm{EvCase})
	\end{array}
\]
\[	\begin{array}{lrr}
		\mc{2}{H[\ \rmutable \ \rho, \ l \mtoa{\rho} C_K \ \ov{v^\circ}]
		~~;~~ {\iupdate_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~~ l~ u^\circ}}
	\\ & 
		\longrightarrow H, \ l \mtoa{\rho} C_K \ v^\circ_0 .. u_i^\circ.. v^\circ_n
		~~;~~ ()
	& (\trm{EvUpdateBind})
	\end{array}
\]
\[	\begin{array}{lrr}
		\mc{2}{H[\ \rmutable \ \rho, \ l \mtoa{\rho} C_K \ \ov{v^\circ} ]
		~~;~~ {\iupdate_{K',i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~~ l~ u^\circ}}
	\\ & 
		\longrightarrow H ~;~ \trm{fail} \qq \qq K \ne K'
	& (\trm{EvUpdateFail})
	\end{array}
\]

\[	\ruleIL	{EvSuspendWit}
		{\wcJudge
			{H}
			{\delta}
			{\delta'}
		}
		{\evJudgeHH
			{\isuspend \ \ov{\varphi} \ \delta \ t \ t'}
			{\isuspend \ \ov{\varphi} \ \delta' \ t \ t'}
		}
\]
\[	\ruleAL	{EvSuspendApp}
		{\evJudgeHH
			{\isuspend \ \tau \ \tau' \ \sigma \ \un{\rpure \ \sigma} \ (\lambda (x : \tau). \ t) \ v^\circ}
			{t [v^\circ / x]}
		}
\]
\[	\ruleIL	{EvMaskWit}
		{\wcJudge
			{H}
			{\delta}
			{\delta'}
		}
		{\evJudge
			{H}
			{\kmask~ \delta~ \kin~ t}
		 	{H}
			{\kmask~ \delta'~ \kin~ t}
		}
\]
\[	\ruleAL	{EvMaskApp}
		{\evJudgeHH
			{\kmask~ \un{\rpure~ \sigma}~ \kin~ t}
			{t}
		}
\]
} % boxfig
\smallskip
\caption{Term Evaluation}
\label{fig:TermEvaluation}
\end{figure}








