
\clearpage{}
\begin{theorem}[Preservation]

Suppose we have a state $H ; t$ with store $H$ and term $t$.
	Let $\Sigma$ be a store typing which models $H$. 
	If $H$ and $t$ are well typed, 
		and $H ; t$ can transition to a new state $H' ; t'$
		then for some $\Sigma'$ which models $H'$, 
		$H'$ is well typed, 
		$t'$ has the same type as $t$,
		and $t'$ has an effect that is no greater than for $t$.

\medskip
\statement{
	If	&~ $\tyJudgeGS{t}{\tau}{\sigma}$ ~and~ $\Sigma \models H$ ~and~ $\Sigma \vdash H$ \\
	\ and	&~ $\evJudge{H}{t}{H'}{t'}$ \\
	\multicolumn{2}{l}{then for some $\Sigma'$, $\sigma'$ we have} \\
		&~ $\tyJudge{\Gamma}{\Sigma'}{t'}{\tau}{\sigma'}$ \\
		&~ and~ $\Sigma' \supseteq \Sigma$
			~and~ $\Sigma' \models H'$
			~and~ $\Sigma' \vdash  H'$
			~and~ $\suJudge{\Gamma}{\Sigma'}{\sigma'}{\sigma}$ 
}
\end{theorem}

\begin{proof}
By induction over the derivation of $\tyJudgeGS{t}{\tau}{\sigma}$.

\tabbedstmts{
	(IH) 
		\> Preservation holds for all subterms of $t$.
		\> (assume) 
}

\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = x$}

Can't happen. Type environment is empty.


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t$ is one of~
	$l$,~
	$()$,~
	$\Lambda(a :: \kappa). \ t'$,~
	$\lambda (x :: \tau). \ t'$ }

Can't happen. There is no transition rule for $H ; t$

\bigskip


% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ \varphi_2$ / TyAppT / EvContext}
$$ 
	\frac
	{ (5)~
	  \tyJudgeGS
		{t_1}
		{\tyForall{a}{\kappa_{11}}{\varphi_{12}}}
		{\sigma}
	  \qq
	  (6) \ \kiJudgeGS {\varphi_2} {\kappa_{11}} 
	}
	{ (\un{1})~
	  \tyJudgeGS
		{t_1 \ \varphi_2} 
		{\varphi_{12}	[\varphi_2/a]} 
		{\sigma}
	}
$$
$$
\qq \qq
	\frac
	{ (7) \ \evJudge {H} {t_1} {H'} {t_1'} }
	{ (\un{2}) \ \evJudge {H} {t_1 \ \varphi_2} {H'} {t_1' \ \varphi_2} }
$$

\tabbedstmts{
	(\un{3..4}) 	
			\> $\Sigma \models H, \ \Sigma \vdash H$
			\> (assume)
\\[1ex]
	(8..12) 	\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1'}
				{ \tyForall{a} {\kappa_{11}} {\varphi_{12}}} {\sigma'}$, \\
			\> \qq $\Sigma' \supseteq \Sigma,~~
				\Sigma' \models H',~~
				\Sigma' \vdash H',~~
				\suJudge{\Gamma}{\Sigma'}{\sigma'}{\sigma}$
			\> (IH 5 7 3 4)
\\[1ex]
	(13)		\> $\kiJudge
				{\Gamma}
				{\Sigma'}
				{\varphi_2}
				{\kappa_{11}}$
			\> (Weak. Store Typing 6 9)
\\
	(14)		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1' \ \varphi_2} 
				{\varphi_{12}	[\varphi_2/a]} 
				{\sigma'}$
			\> (TyAppT 8 13)
}

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ \varphi_2$ / TyAppT / EvTAppAbs}
$$
	\infer
	{ (\un{1})~
	  \tyJudgeGS
		{ (\teLAM{a}{\kappa_{11}}{t_{12}}) \ \varphi_2}
		{ \varphi_{12}[\varphi_2/a] }
		{ \bot }
	}
	{ 	\infer 
		{ (5) \ \tyJudgeGS
			{ \teLAM   {a}{\kappa_{11}}{t_{12}} }
			{ \tyForall{a}{\kappa_{11}}{\varphi_{12}}}
			{ \bot}
		}
		{ (7) \ \tyJudge
			{\Gamma,~ a : \kappa_{11}}{\Sigma}
			{t_{12}}
			{\varphi_{12}}
			{\bot} 
		}
	  \qq
	  (6)~
	  \kiJudgeGS
		{\varphi_2}
		{\kappa_{11}}
	}
$$
$$ (\un{2}) \
	 H ; (\Lambda (a :: \kappa_{11}). \ t_{12}) \ \varphi_2 \eto 
	 H ; t_{12}[\varphi_2/a] 
$$
\tabbedstmts{
	(\un{3..4}) 	
			\> $\Sigma \models H, \ \Sigma \vdash H $
			\> (assume)
\\ 
	(9) 		\> $\tyJudgeGS
				{t_{12} [\varphi_2/a]}
				{\varphi_{12} [\varphi_2/a] }
				{\bot}$
			\> (Sub. Type/Value 7 6)
}


\clearpage{}
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ t_2$ / TyApp / EvContext ($E_v~ t_2$)}
$$
	\frac	
	{ (5)~
	  \tyJudgeGS
		{t_1}
		{\tau_{11} \toa{\sigma} \tau_{12}}
		{\sigma_1}
	  \qq
	  (6)~
	  \tyJudgeGS
		{t_2}
		{\tau_{11}}
		{\sigma_2}
	}
	{ (\un{1})~
		\tyJudgeGS
		{t_1 \ t_2}
		{\tau_{12}}
		{\sigma_1 \lor \sigma_2 \lor \sigma}
	}
$$
$$
	\frac
	{ (7) \ \evJudge{H}{t_1}
			{H'}{t_1'}
	}
	{ (\un{2})
		 \ \evJudge	
		 	{H}{t_1 \ t_2}
			{H'}{t_1' \ t_2}
	}
$$
\tabbedstmts{
	(\un{3..4})
			\> $\Sigma \models H, \ \Sigma \vdash H$
			\> (assume)
\\
	(8..12) 	\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1'}
				{\tau_{11} \toa{\sigma} \tau_{12}}
				{\sigma_1'}$ 
\\
			\> \qq $\Sigma' \supseteq \Sigma,~~
					\Sigma'    \models H',~~
					\Sigma'    \vdash  H',~~
					\suJudge{\Gamma}{\Sigma'}{\sigma_1'}{\sigma_1}$ 
			\> (IH 5 7 3 4)
\\
	(13) 		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_2}
				{\tau_{11}}
				{\sigma_2}$
			\> (Weak. Store Typing 6 9)
\\
	(14) 		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1' \ t_2}
				{\tau_{12}}
				{\sigma_1' \lor \sigma_2 \lor \sigma}$
			\> (TyApp 8 13)
\\
	(15) 		\> $\suJudge{\Gamma}{\Sigma'}
				{\sigma_1' \lor \sigma_2 \lor \sigma}
				{\sigma_1 \lor \sigma_2 \lor \sigma}$
			\> (Def. $\tle$ 12)
}



\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ t_2$ / TyApp / EvAppAbs}
$$
 	\infer	
	{ (\un{1}) \ 
	   \tyJudgeGS
		{(\teLam{x}{\tau_{11}}
		{t_{12}}) \ v^\circ}
		{\tau_{12}}
		{\sigma_1 \lor \sigma}
	}
	{ 	\infer 
	  	{ (5) \ 
		  \tyJudgeGS
			{\teLam{x}{\tau_{11}}{t_{12}}}
			{\tau_{11} \toa{\sigma} \tau_{12}}
			{\sigma_1}
		}
		{ 	(7) \ 
			\tyJudge
				{\Gamma,~ x : \tau_{11}}
				{\Sigma}
				{t_{12}}
				{\tau_{12}}
				{\sigma}
		}
		& \quad
		(6) \
		\tyJudgeGS
			{v^\circ}
			{\tau_{11}}
			{\bot}
	}
$$	
$$
	(\un{2}) \
	\evJudge	
		{H}
		{(\teLam{x}{\tau_{11}}{t_{12}}) \ v^\circ}
		{H'}
		{t_{12}[v^\circ/x]}
$$
\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H, \ \Sigma \vdash H$
			\> (assume)
\\
	(8)		\> $\tyJudgeGS
				{t_{12}[v^\circ/x]}
				{\tau_{12}}
				{\sigma}$ 
			\> (Sub. Value/Value 7 6)
\\
	(9)		\> $\suJudge{\Gamma}{\Sigma'}{\sigma}{\sigma_1 \lor \sigma}$
			\> (Def. $\tle$)
}

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = K~ \un{\rho}~ \ov{\varphi}~ \ov{v^\circ}$ / TyData / EvAlloc}
$$
	\frac
	{ \begin{array}{ll}
  	  & 
	  (7)~
	  \ov{\tyJudgeGS
		{v^\circ_i}
		{\tau_i	[\un{\rho}/r][\ov{\varphi/a}]}
		{\bot}}^{\: i \gets 0..n} 
	  \\
          (5)~
          \kiJudgeGS
		{\un{\rho}}
		{\%} 
	  &
	  (6)~
	  K :: \forall(r : \%). \forall(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)
	  \end{array}
	}
	{ (\un{1})~
	  \tyJudgeGS
		{K~ \un{\rho}~ \ov{\varphi}~ \ov{v^\circ}}
		{T~ \un{\rho}~ \ov{\varphi}}
		{\iAlloc~ \un{\rho}}
	}
$$
$$	(\un{2})~ 
	\evJudge
		{H[\rho]}
		{K~ \un{\rho}~ \ov{\varphi}~ \ov{v^\circ}}
		{H,~ l \mtoa{\rho} C_K~ \ov{v^\circ}}
		{l}
	~~~~~~~~~ l~~ \trm{fresh}
$$
\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H, \ \Sigma \vdash H$
			\> (assume)
\\	
	(8)		\> \trm{let}~ $\Sigma' ~= \Sigma,~ l :: T~ \un{\rho}~ \ov{\varphi}$
\\
	(9)		\> \trm{let}~ $H' = H,~ l \mtoa{\rho} C_K~ \ov{v^\circ}$
\\
	(10)		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{l}
				{T~ \un{\rho}~ \ov{\varphi}}
				{\bot}$
			\> (TyLoc 8)
\\
	(11)		\> $\Sigma' \supseteq \Sigma$
			\> (Def. $\supseteq$ 8)
\\
	(12)		\> $\Sigma' \models H'$
			\> (Store Model 3 8 9)
\\
	(13)		\> $\Sigma' \: \vdash H'$
			\> (Well Typed Store 4 9 8 6 7)
\\
	(14)		\> $\suJudge{\Gamma}{\Sigma'}{\bot}{\iAlloc~ \un{\rho}}$
			\> (Def. $\tle$)
}

\clearpage{}
% -------------------------------------------------------------------------------------------------
\pCase{$t = (\teLetR{r}{\ov{w_i = \delta_i}}{t_1})$ / TyLetR / EvLetR}

$$	\infer
	{ (\un{1}) \
	  \tyJudgeGS
	  	{(\teLetR{r}{\ov{w_i = \delta_i}}{t_1})}
		{\tau}
		{\sigma \setminus (\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}
	}
	{ \begin{array}{lll}
	  	(5)~	
		\ov{\delta_i} \ \trm{well formed} 
		&
		(6)~
		\ov{\kiJudgeGS
			{\delta_i}
			{\kappa_i}}^{\: i}
		&
		\\
		(7)~
			r \notin fv(\tau) 
		&
		\mc{2}{
		(8)~
		\tyJudge
			{\Gamma,~ r : \%,~ \ov{w_i : \kappa_i}} 
			{\Sigma} 
			{t_1} 
			{\tau} 
			{\sigma}}
	  \end{array}
	}
$$
$$	\infer
	{ (\un{2})~
	  \evJudge
		{H}
		{\teLetR{r}{\ov{w_i = \delta_i}}{t_1}}
		{H}
		{\teWithR
			{\un{\rho}}
			{\ov{\Delta_i}}
			{t_1[\un{\rho}/r~~ \ov{\Delta_i/w_i}]}}
	}
	{ (9)~
	  	\un{\rho} \ \textrm{fresh}
 	  \quad
	  (10)~
		\ov{\Delta_i	= \rwitOf(\delta_i[\un{\rho}/r])}^{~ i}
	}
$$

\tabbedstmts{
	(\un{3..4})
			\> $\Sigma \models H,~ \Sigma \vdash H$
			\> (assume)
\\
	(11)		\> let~ $H' = H,~ \rho,~ \ov{\pi_i}$
			\> (let)
\\
	(12)		\> let~ $\Sigma' ~ = \Sigma,~ \un{\rho},~ \ov{\Delta_i}$
			\> (let)
\\
	(13)		\> $\Sigma' \models H'$
			\> (Store Model 3 11 12)
\\
	(14)		\> $\Sigma' \vdash H'$
			\> (Well Typed Store 4 11 12)
\\
	(15)		\> $\tyJudge
				{\Gamma,~ r : \%, \ \ov{w_i : \kappa_i}} 
				{\Sigma'} 
				{t_1} 
				{\tau} 
				{\sigma}$
			\> (Weak. Store Typing 9 14)
\\
	(16)		\> $\kiJudge
				{\Gamma}
				{\Sigma'}
				{\un{\rho}}
				{\%}$
			\> (KiHandle 12)
\\
	(17)		\> $\ov{\kiJudge
				{\Gamma}
				{\Sigma'}
				{\Delta_i}
				{\kappa_i}}^{\: i}$
			\> (KiConst, KiMutable, 12, 5)
\\
	(18)		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}
				{\tau   [\un{\rho}/r~ \ov{\Delta_i/w_i}]}
				{\sigma [\un{\rho}/r~ \ov{\Delta_i/w_i}]}$
			\> (Subst. Type/Value 5 17 18)
\\[1ex]
	(19)		\> $\tau[\un{\rho}/r~ \ov{\Delta_i/w_i}] \equiv 
			    \tau[\un{\rho}/r]$
			\> (No Wit. Vars in Value Types)
\\[1ex]
	(20)		\> $\sigma[\un{\rho}/r~ \ov{\Delta_i/w_i}] \equiv 
			    \sigma[\un{\rho}/r]$
			\> (No Wit. Vars in Effects)

\\[0.5ex]
	(21)		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}
				{\tau   [\un{\rho}/r]}
				{\sigma [\un{\rho}/r]}$
			\> (Equiv. 18..20)
\\
	(22)		\> $\tyJudge
				{\Gamma}
				{\Sigma'}
				{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}
				{\tau}
				{\sigma [\un{\rho}/r]}$
			\> (Def. Sub. 21 7)
\\[0.5ex]
	(23)		\> $\Gamma ~|~ \Sigma' \vdash \teWithR{\un{\rho}}{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}$
\\
			\> $\hspace{2.2em}:: \tau 
				~;~ \sigma[\un{\rho}/r]\setminus 
						(\iRead~ \un{\rho} \lor \iWrite~ \un{\rho} \lor \iAlloc~ \un{\rho})$
			\> (TyWithR 12 22)
\\[0.5ex]
	(24)		\> $\Gamma ~|~ \Sigma' \vdash \teWithR{\un{\rho}}{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}$
\\
			\> $\hspace{2.2em}:: \tau 
				~;~ \sigma[\un{\rho}/r]\setminus 
						(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)[\un{\rho}/r]$
			\> (Def. Subst 23)
\\[0.5ex]
	(25)		\> $\Gamma ~|~ \Sigma' \vdash \teWithR{\un{\rho}}{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}$
\\
			\> $\hspace{2.2em}:: \tau 
				~;~ (\sigma\setminus 
						(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r))[\un{\rho}/r]$
			\> (Def. Subst 24)
\\[0.5ex]
	(26)		\> $r \notin  \ifv(\sigma\setminus (\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r))$
			\> (Only have R/W/A Effs.)
\\[0.5ex]
	(27)		\> $\Gamma ~|~ \Sigma' \vdash \teWithR{\un{\rho}}{t_1    [\un{\rho}/r~ \ov{\Delta_i/w_i}]}$
\\
			\> $\hspace{2.2em}:: \tau 
				~;~ \sigma \setminus 
						(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)$
			\> (Def. Subst 25 26)
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \teWithR{\un{\rho}}{t}$} / TyWithR / EvEjectR

\[	\infer
	{ (\un{1})~
	  \tyJudgeGS
		{\teWithR{\un{\rho}}{v^\circ}}
		{\tau}
		{\bot}
	}
	{ (5)~
	  \tyJudgeGS
		{v^\circ}{\tau}{\bot}
	}
\]	
\[
	(\un{2})~
	\evJudge{H}{\teWithR{\un{\rho}}{v^\circ}}{H}{v^\circ}
\]

\tabbedstmts{
	(\un{3..4})
		\> $\Sigma \models H,~ \Sigma \vdash H$
		\> (assume)
\\
	(6)~	\> $\tyJudgeGS{v^\circ}{\tau}{\bot}$
		\> (Restate 5)
}


\clearpage{}
% -------------------------------------------------------------------------------------------------
\pCase{$t = \kcase~ l~ \kof~ ...~ K~ \ov{x} ~...$ / TyCase / EvCase}

$$	\infer
	{ (1)~
	  \tyJudgeGS
		{\kcase~ l ~\kof~ ...~ K_j~ \ov{x} \to t_j~...}
		{\tau}
		{\sigma \lor Read~ \un{\rho} \lor \sigma'_0 \lor \sigma'_1 ... \lor \sigma'_n}
	}
	{ (5)~
	  \tyJudgeGS
		{l}
		{T~ \un{\rho}~ \ov{\varphi'}}
		{\sigma}
	  \quad
	  (6)~
	  \ov{\tyJudgeGS
		{K_i~ \ov{x} \to t_i}
		{T~ \un{\rho}~ \ov{\varphi'} \to \tau}
		{\sigma'_i}}^{~ i \gets 0..n}
	}
$$

$$
	(2)~ \evJudge
		{H[l \mtoa{\rho} C_K~ \ov{v^\circ}]}
		{\kcase~ l ~\kof~ ...~ K_j~ \ov{x} \to t_j~...}
		{H}
		{t_j[\ov{v^\circ/x}]}
$$

\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H$,~ $\Sigma \vdash H$
			\> (assume)
\\
	(7 8)		\> $\tyJudgeGS
				{K_j~ \ov{x_k}^{\: k} \to t_j}
				{T~ \un{\rho}~ \ov{\varphi} \to \tau}
				{\sigma'_j}$,~~
			   $j \in 0..n$
			\> (Exhaustive Cases 6)
\\[0.5ex]
	(9)		\> $K :: \forall(r : \%)(\ov{a : \kappa}). \ov{\tau'} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)$
			\> (Inv. TyAlt 7)
\\[0.5ex]
	(10)		\> $\tyJudge
				{\ov{x_k:\tau_k'[\un{\rho}/r~ \ov{\varphi/a}]}^{\: k}}
				{\Sigma}
				{t_j}
				{\tau}
				{\sigma'_j}$
			\> (Inv. TyAlt 7)
\\[0.5ex]
	(11)		\> $l :: T~ \un{\rho}~ \ov{\varphi} \in \Sigma$
			\> (Well Typed Store, TyLoc 4 2 5)
\\
	(12)		\> $\ov{\tyJudgeGS
				{v_k^\circ}
				{\tau_k' [\un{\rho}/r~ \ov{\varphi/a}]}
				{\bot}}^{\: k}$
			\> (Well Typed Store 4 12)
\\[0.5ex]
	(13)		\> $\tyJudgeGS
				{t_j[\ov{v_k^\circ/x}^{\: k}]}
				{\tau}
				{\sigma'_j}$
			\> (Sub. Value/Value 10 12)
\\[0.5ex]
	(14)		\> $\suJudgeGS
				{\sigma'_j}
				{\sigma \lor Read~ \un{\rho} \lor \sigma'_0 \lor \sigma'_1 ... \lor \sigma'_n}$
			\> (Def. $\tle$ 8)
}		


\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = update_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~ l~ u^\circ$ / TyUpdate / EvUpdateBind}
$$
	\infer
	{ (\un{1})~
	  \tyJudgeGS
		{update_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~ l~ u^\circ}
		{()}
		{Write~ \un{\rho}}
	}
	{ \begin{array}{ll}
	  (5)~ 
	  \kiJudgeGS
		{\un{\rmutable~ \rho}}
		{Mutable~ \un{\rho}}
	  &
	  (6)~
	  \tyJudgeGS
		{u^\circ}
		{\tau_i	[\un{\rho}/r~ \ov{\varphi}/a]}
		{\bot}
	  \\
	  (7)~
	  \tyJudgeGS
		{l}
		{T~ \un{\rho}~ \ov{\varphi}}
		{\bot}
	  &
	  (8)~
	  K :: \forall(r : \%)(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)
	 \end{array}
	}
$$

$$
(\un{2})\begin{array}{lll}
	
		& H[\rmutable~ \un{\rho},~ l \mtoa{\rho} C_K~ \ov{v^\circ}] 
		& ;~~ update_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~ l~ u^\circ
\\ 	 \eto	& H,~ l \mtoa{\rho} C_K~ v^\circ_0 .. u^\circ_i... v^\circ_n
		& ;~~  	()
	\end{array}
$$

\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H,~ \Sigma \vdash H$
			\> (assume)
\\
	(9)		\> $\tyJudgeGS{()}{()}{\bot}$
			\> (TyUnit)
\\
	(10)		\> let $H' = H,~ l \mtoa{\rho} C_K~ v^\circ_0 .. u^\circ_i... v^\circ_n$
			\> (let)
\\[0.5ex]
	(11)		\> $\ov{\tyJudgeGS
				{v^\circ_j}
				{\tau_j	[\un{\rho}/r~ \ov{\varphi/a}]}
				{\bot}}^{\: j \gets 0..n}$
			\> (Well Typed Store 4 8)
\\
	(12)		\> $\Sigma \vdash H'$
			\> (Well Typed Store 11 6 7 4 10)
\\
	(13)		\> $\Sigma \models H'$
			\> (Store Model 4 10)
\\
	(14)		\> $\suJudgeGS{\bot}{Write~ \un{\rho}}$
			\> (Def. $\tle$)
}

\clearpage{}

% -------------------------------------------------------------------------------------------------
\pCase{$t = suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta~ t_1~ t_2$ / TySuspend / EvSuspendWit}

$$
	\infer
	{ (\un{1})~
	  \tyJudgeGS
		{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta~ t_1~ t_2}
		{\tau_{12}}
		{\sigma_1 \lor \sigma_2}
	}
	{ \begin{array}{ll}
	  &
	  (5)~
	  \kiJudgeGS
		{\delta}
		{Pure~ \sigma}
	  \\
	  (3)~
	  \tyJudgeGS
		{t_1}
		{\tau_{11} \toa{\sigma} \tau_{12}}
		{\sigma_1}
	  &
	  (4)~
	  \tyJudgeGS
		{t_2}
		{\tau_{11}}
		{\sigma_2}
	 \end{array}
	}
$$

$$
	\infer
	{ (2)~
	  \evJudge
		{H}
		{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta~ t_1~ t_2}
		{H}
		{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta'~ t_1~ t_2}
	}
	{ (6)~ 
	  \wcJudge
		{H}
		{\delta}
		{\delta'}
	}
$$

\tabbedstmts{
	(\un{3..4})	\> $\Sigma \models H$, $\Sigma \vdash H$
			\> (assume)
\\
	(7)		\> $\tyJudgeGS
				{\delta'}
				{Pure~ \sigma}$
			\> (Pres. Purity 5 6)
\\
	(8)		\> $\tyJudgeGS
				{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta'~ t_1~ t_2}
				{\tau_{12}}
				{\sigma_1 \lor \sigma_2}$
			\> (TySuspend 3 7 4)
}

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = suspend~ \tau_{11}~ \tau_{12}~ \sigma~ 
		\un{\rpure~ \sigma}~ 
		(\teLam{x}{\tau_{11}}{t_{12}})~ 
		v^\circ_2$ / TySuspend / EvSuspendApp}
$$
	\infer
	{ (\un{1}) \
	  \tyJudgeGS
		{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ 
			\un{\rpure~ \sigma}~ 
			(\teLam{x}{\tau_{11}}{t_{12})}~ 
			v^\circ_2}
		{\tau_{12}}
		{\bot}
	}
	{	
		\begin{array}{ll}
			\infer
			{ (5)~
			  \tyJudgeGS
			  	{\teLam{x}{\tau_{11}}{t_{12}}}
				{\tau_{11} \toa{\sigma} \tau_{12}}
				{\bot }
		   	}
			{ (6)~
			  \tyJudge
			  	{\Gamma,~ x : \tau_{11}}
				{\Sigma}
				{t_{12}}
				{\tau_{12}}
				{\sigma}
			}
		\end{array}
		\qq
		\begin{array}{ll}
			(7)~
			\kiJudgeGS
			  	{\un{\rpure~ \sigma}}
				{Pure~ \sigma}
			\\
			(8)~
			\tyJudgeGS
			  	{v_2^\circ}
				{\tau_{11}}
				{\bot}
		\end{array}
	}
$$
$$
	(\un{2})~
	\evJudge
		{H}
		{suspend~ \tau_{11}~ \tau_{12}~ \sigma~ 
			\un{\rpure~ \sigma}~ 
			(\teLam{x}{\tau_{11}}{t_{12})}~ 
			v^\circ_2}
		{H}
		{t_{12}[v_2^\circ/x]}
$$
\tabbedstmts{
	(\un{3..4})
			\> $\Sigma \models H, \ \Sigma \vdash H$
			\> (assume)
\\
	(9)		\> $\tyJudgeGS
				{t_{12}[v^\circ_2/x]}
				{\tau_{12}}
				{\sigma}$
			\> (Sub. Value/Value 6 8)
\\
	(10)		\> $\suJudgeGS{\sigma}{\bot}$
			\> (SuMaskPure 7)
}	

\bigskip


% -------------------------------------------------------------------------------------------------
\pCase{$t = \kmask~ \delta~ \kin~ t_1$ / TyMask / EvMaskWit}

Similarly to TySuspend / EvSuspendWit case.

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = \kmask~ \un{\rpure~ \sigma'}~ \kin~ t_1$ / TyMask / EvMaskApp}
$$
	\infer
	{ (\un{1})~ 
	  \tyJudgeGS
		{\kmask~ \un{\rpure~ \sigma'}~ \kin~ t_1}
		{\tau}
		{\sigma \setminus \sigma'}
	}
	{ (5)~
	  \tyJudgeGS
		{t_1}
		{\tau}
		{\sigma}
	  \quad
	  (6)~
	  \kiJudgeGS
		{\un{\rpure~ \sigma'}}
		{Pure~ \sigma'}
	}
$$
$$
	(\un{2})~ 
		\evJudge
		{H}
		{\kmask~ \un{\rpure~ \sigma'}~ \kin~ t_1}
		{H}
		{t}
$$

\tabbedstmts{
	(\un{3..4})
		\> $\Sigma \models H, \ \Sigma \vdash H$
		\> (assume)
\\
	(7)	\> $\suJudgeGS{\sigma'}{\bot}$ 
		\> (SuMaskPure 6)
\\
	(8)	\> $\suJudgeGS{\sigma}{\sigma \setminus \sigma'}$
		\> (Prop. of $\tle$ 7)
}

\bigskip
% -------------------------------------------------------------------------------------------------
The remaining cases are similar to the TyApp / EvContext ($E_v~ t_2$) case.

\end{proof}
