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

Suppose we have a state $H ; t$ with store $H$ and term $t$. 
Let $\Sigma$ be a store typing which models $H$. 
If $H$ is well typed, and $t$ is closed and well typed, and $t$ contains no fabricated region witnesses,
then either $t$ is a value or $H ; t$ can transition to the next state.

\medskip
\begin{tabular}{ll}
	If 	&~ $\tyJudge {\emptyset} {\Sigma} {t} {\tau} {\sigma}$  
			~and~ $\Sigma \models H$
			~and~ $\Sigma \vdash  H$
			~and~ $\pnofab{t}$  
	\\
	then	&~ $t$ $\in$ $Value$ \\
	\ or 	&~ {for some $H'$, $t'$ we have} \\
		&~ ~~ (~~~~$\evJudge {H} {t} {H'} {t'}$ \ and \ $\pnofab{t'}$ \\
		&~ ~~~ or $\evJudge {H} {t} {H'} {\trm{fail}}$)
\end{tabular}	
\end{theorem}

\begin{proof}
By induction over the derivation of \ \ $\tyJudge {\emptyset} {\Sigma} {t} {\tau} {\sigma}$

\begin{center}
Let $(\pstep{H}{t}) \equiv$ 
	(for some $H$, $t$ we have $\evJudge {H} {t} {H'} {t'}$ and $\pnofab{t'}$)
\end{center}

We will not formally prove $\pnofab{t'}$ in the conclusion of each case. This property
can be verified by inspecting (EvLetRegion) and noting that unevaluated applications
of witness constructors are not substitued into the body of the term.

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

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

Can't happen. Type environment is empty.

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

$t \in Value$	

\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = (t_1 \ \varphi_2)$ / TyAppT}

$$
	\frac	
	{ (5) \ 
	  \tyJudgeES
		{t_1}
		{\tyForall {a} {\kappa_{11}} {\varphi_{12}}}
		{\sigma} 
	  \quad
	  (6) \ 
	  \kiJudgeES
		{\varphi_2}
		{\kappa_{11}}
	}
	{ (\un{1}) \
	  \tyJudgeES
	  	{t_1 \ \varphi_2}
		{\varphi_{12}[\varphi_2/a]}
		{\sigma}
	} 
$$
\smallskip

\tabbedstmts{
	(\un{2..4}) 
	  	 	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
	 		\> (assume)
			\\
	(7)		\> $t_1 \in~ Value~ \por~ \pstep{H}{t_1}$
			\> (IH 5 2..4)
\\[1ex]
	(8)		\> $\emph{Case:} \ \ t_1 \in Value$
\\
	(9)		\> $t_1 = \teLAM{a}{\kappa_{11}}{t_{12}}$
			\> (Forms of Terms 8 5)
\\
	(10)		\> $\pstep{H}{t}$
			\> (EvTAppAbs 9)
\\[1ex]
	(11)		\> $\emph{Case:} \ \ \pstep{H}{t_1}$
\\
	(12)		\> $\pstep{H}{t}$
			\> (EvContext 11)
}


\clearpage{}
% -------------------------------------------------------------------------------------------------
\pCase{$t = t_1 \ t_2$ / TyApp}
$$
	\frac	
	{ (5) \ \tyJudgeES {t_1} {\tau_{11} \toa{\sigma} \tau_{12}} {\sigma_1} 
	  \qq
	  (6) \ \tyJudgeES {t_2} {\tau_{11}} {\sigma_2} 
	}
	{ (\un{1}) 
	  \ \tyJudgeES {t_1 \ t_2} {\tau_{12}} {\sigma_1 \lor \sigma_2 \lor \sigma} }
$$	  
\tabbedstmts{
	(\un{2..4}) 
			\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume)
\\
	(7)		\> $t_1 \in Value \por \pstep{H}{t_1}$
			\> (IH 5 2..4)
\\
	(8)		\> $t_2 \in Value \por \pstep{H}{t_2}$
			\> (IH 6 2..4)
\\[1ex]
	(9)		\> $\pcase {\pstep{H}{t_1}}$
\\
	(10)		\> $\pstep{H}{t}$
			\> (EvContext 9)
\\[1ex]
	(11, 12)	\> $\pcase {t_1 \in Value, \ \pstep{H}{t_2}}$
\\
	(13)		\> $\pstep{H}{t}$
			\> (EvContext 11 12)
\\[1ex]
	(14, 15)	\> $\pcase {t_1 \in Value, \ t_2 \in Value}$
\\
	(16)		\> $t_1 = \teLam{x}{\tau_{11}}{t_{12}}$
			\> (Forms of Terms 14 5)
\\
	(17)		\> $\pstep{H}{t}$
			\> (EvAppAbs 16 15)
}

\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = K~ \varphi~ \ov{\varphi'}~ \ov{t'}$ / TyData}
$$
	\frac
	{ \begin{array}{ll}
  	  & 
	  (7)~
	  \ov{\tyJudgeES
		{t'_i}
		{\tau_i[\varphi/r][\ov{\varphi'/a}]}
		{\sigma_i}}^{\: i \gets 0..n} 
	  \\
          (5)~ \kiJudgeES{\varphi}{\%} 
	  &
	  (6)~
	  K :: \forall(r : \%). \forall(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)
	  \end{array}
	}
	{ (\un{1})~
	  \tyJudgeES
		{K~ \varphi~ \ov{\varphi'}~ \ov{t'}}
		{T~ \varphi~ \ov{\varphi'}}
		{\sigma_0 \lor \sigma_1 ... \lor \sigma_n}
	}
$$

\tabbedstmts{
\\[0.5ex]
	(\un{2..4})	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume) 
\\[1ex]
	(8)		\> $\pcase{\pstep{H}{t_i'}~~~ \trm{for some}~ i}$
\\
	(9)		\> $\pstep{H}{t}$
			\> (EvContext 8)
\\[1ex]
	(10)		\> $\pcase{\trm{forall}~ i~ \trm{we have}~ t_i' \in Value}$
\\
	(11)		\> $\varphi = \un{\rho}$,~ for some $\rho$
			\> (Forms of Types 5)
\\
	(12)		\> $\un{\rho} \in \Sigma$
			\> (KiHandle 5 11)
\\
	(13)		\> $\rho \in H$
			\> (Def. Store Model 2 12)
\\	
	(14)		\> $\pstep{H}{t}$
			\> (EvAlloc 10 11 13)
}


\medskip
% -------------------------------------------------------------------------------------------------
\pCase{$t = (\kcase~ t_1~ \kof~ \ov{p \to t'})$ / TyCase}
$$
	\frac
	{ (5)~
	  \tyJudge
		{\emptyset}
		{\Sigma}
		{t_1}
		{T~ \varphi~ \ov{\varphi'}}
		{\sigma}
	  \quad
	  (6)~
	  \ov{\tyJudge
		{\emptyset}
		{\Sigma}
		{p_i 				\to t_i'}
		{T~ \varphi~ \ov{\varphi'}	\to \tau}
		{\sigma_i'}}^{~ i \gets 0..n}
	}
	{ (\un{1})~
	  \tyJudge
		{\emptyset}
		{\Sigma}
		{\kcase~ t_1~ \kof~ \ov{p \to t'}}
		{\tau}
		{\sigma \lor Read~ \varphi \lor \sigma_0' \lor \sigma_1' ... \lor \sigma_n'}}
$$	

\tabbedstmts{
	(\un{2..4})	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume)
\\
	(7)		\> $t_1 \in Value \por \pstep{H}{t_1}$
			\> (IH 5 2..4)
\\
	(8)		\> $\pcase {\pstep{H}{t_1}}$
\\
	(9)		\> $\pstep{H}{t}$
			\> (EvContext 8)
\\
	(10)		\> $\pcase {t_1 \in Value}$
\\
	(11)		\> $t_1 = l$
			\> (Forms of Terms 10 5)
\\
	(12)		\> $\tyJudge
				{\emptyset}
				{\Sigma',~ l : T~ \rho~ \ov{\varphi'}}
				{l}
				{T~ \rho~ \ov{\varphi'}}
				{\bot}$
			\> (5, 11)
\\
	(13)		\> $l \mtoa{\rho} C_K~ \ov{v^\circ} \in H$
			\> (Def. Store Model 2 12)
\\
	(14)		\> $\pstep{H}{t}$
			\> (EvCase 13)
				
}


\bigskip
% -------------------------------------------------------------------------------------------------
\pCase{$t_1 = (update_{K,i}~ \varphi~ \ov{\varphi'}~ \delta~ t_2~ t_3)$ / TyUpdate}
$$
	\frac	
	{ \begin{array}{ll}
	  (6)~
	  \kiJudgeES
		{\delta}
		{Mutable~ \varphi}
	  \\
	  (5)~ 
	  \tyJudgeES
		{t_2}
		{T~ \varphi~ \ov{\varphi'}}
		{\delta}
	  \end{array}
	  \quad
	  \begin{array}{ll}
	  (8)~
	  \tyJudgeES
		{t_3}
		{\tau_i[\varphi/r][\ov{\varphi'/a}]}
		{\sigma'} 
	  \\
	  (7)~
	  K :: \forall(r : \%). \forall(\ov{a : \kappa}). \ov{\tau} \to T~ r~ \ov{a} \in \trm{ctorTypes}(T)
	  \\
	  \end{array}
	}
	{ (\un{1}) 
	   \ \tyJudgeES
		{(update_{K,i}~ \varphi~ \ov{\varphi'}~ \delta~ t_2~ t_3)}
		{()}
		{(\sigma \lor \sigma' \lor Write \ \varphi)} 
	}
$$

\medskip
\tabbedstmts{
	(\un{2..4})	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume)
\\
	(9)		\> $\delta = \un{\rmutable~ \rho}$~ for some $\rho$
			\> (Forms of Types 6 4)
\\
	(10,~11)	\> $\kiJudgeES
				{\un{\rmutable~ \rho}}
				{Mutable~ \un{\rho}}$,~~
			   $\varphi = \un{\rho}$
			\> (KiMutable 9 6)
\\
	(12)		\> $\un{\rmutable~ \rho} \in \Sigma$
			\> (KiMutable 10)
\\[1ex]
	(13)		\> $\pcase{\pstep{H}{t_2}}$
\\
	(14)		\> $\pstep{H}{t_1}$
			\> (EvContext 13)
\\
\\
	(15,~16)	\> $\pcase{t_2 \in Value,~ \pstep{H}{t_3}}$
\\
	(17)		\> $t_2 = l$
			\> (Forms of Terms 15 5)
\\
	(18)		\> $\pstep{H}{t_1}$
			\> (EvContext 17 16)
\\[1ex]
	(19,~20)	\> $\pcase{t_1 \in Value,~ t_2 \in Value}$
\\
	(21)		\> $t_2 = l$
			\> (Forms of Terms 19 5)
\\
	(22)		\> $\tyJudgeES
				{l}
				{T~ \un{\rho}~ \ov{\varphi'}}
				{\bot}$
			\> (TyLoc 5 11)
\\
	(23)		\> $l :: T~ \un{\rho}~ \ov{\varphi'} \in \Sigma$
			\> (TyLoc 22)
\\
	(24)		\> $l \mtoa{\rho} C_{K'}~ \ov{v^\circ} \in H$~ for some $K', \ov{v^\circ}$
			\> (Def. Store Model 2 23)
\\
	(25)		\> $\un{\rmutable~ \rho} \in H$
			\> (Def. Store Model 2 12)
\\[1ex]
	(26)		\> \quad $\pcase{K = K'}$
\\
	(27)		\> \quad $\pstep{H}{t}$
			\> \hspace{-3em} (EvUpdateBind 25 24 9 21 20)
\\[1ex]
	(28)		\> \quad $\pcase{K \ne K'}$
\\
	(29)		\> \quad $H;t \eto H';\trm{fail}$
			\> \hspace{-3em} (EvUpdateFail 25 24 9 21 20)
}


% -------------------------------------------------------------------------------------------------
\pCase{$t = (suspend \ \delta \ t_1 \ t_2)$ / TySuspend}
$$
	\frac	
	{ (5)~
	  \kiJudgeES
		{\delta}
		{Pure \ \sigma}
          \quad
	  (6)~
	  \tyJudge
		{\emptyset}
		{\Sigma}
		{t_1}{\tau_{11} \toa{\sigma} \tau_{12}}
		{\sigma_1} 
	  \quad
	  (7)~
	  \tyJudge
		{\emptyset}
		{\Sigma}
		{t_2}
		{\tau_{11}}
		{\sigma_2} 
	}
	{ (\un{1})~
	  \tyJudge
		{\emptyset}
		{\Sigma}
		{(suspend~ \tau_{11}~ \tau_{12}~ \sigma~ \delta~ t_1~ t_2)}
		{\tau_{12}}
		{\sigma_1 \lor \sigma_2} 
	}
$$
\tabbedstmts{
	(\un{2..4}) 	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume)
\\
	(8) 		\> $\delta \in \{ 
				MkPurify \ \delta_2,~
				MkPureJoin \ \delta_3 \ \delta_4,~
				MkPureBot,$
\\
			\> \qq \quad \ $\un{\rpure \ \sigma} \}$
			\> (Forms of Types 5)
\\[1ex]
	(9)		\> $\pcase{\delta \in \{ 
				MkPurify \ \delta_2,~
				MkPureJoin \ \delta_3 \ \delta_4,~
				MkPureBot \} }$
\\
	(10)		\> $H \ ; \ \delta \leadsto \delta'$
	 		\> (Progress of Purity 5 9 4)
\\
	(11)		\> $\pstep{H}{t}$
			\> (EvSuspendWit 10)
\\[1ex]
	(12..14) 	\> $\pcase{\delta = \un{\rpure \ \sigma}, \ t_1 \in Value, \ t_2 \in Value}$
\\
	(15) 		\> $t_1 = \teLam{x}{\tau}{t_3}$
			\> (Forms of Terms 6 13)
\\
	(16) 		\> $\pstep{H}{t}$
			\> (EvSuspendApp 12 15 14)
}



\pagebreak{}
% -------------------------------------------------------------------------------------------------
\pCase{$t = \kmask~ \delta~ \kin~ t_1$}

$$
	\infer
	{ (\un{1})~
	  \tyJudgeES
		{\kmask~ \delta~ \kin~ t}
		{\tau}
		{\sigma \setminus \sigma'}
	}
	{ (5)~
	  \tyJudgeES
		{t}
		{\tau}
		{\sigma}
	  \quad
	   (6)~
	   \kiJudgeES
		{\delta}
		{Pure~ \sigma'}
	}
$$


\tabbedstmts{
	(\un{2..4}) 	\> $\Sigma \models H, \ \Sigma \vdash H, \ \pnofab{t}$
			\> (assume)
\\
	(7) 		\> $\delta \in \{ 
				MkPurify \ \delta_2,~
				MkPureJoin \ \delta_3 \ \delta_4,~
				MkPureBot,$
\\
			\> \qq \quad \ $\un{\rpure \ \sigma} \}$
			\> (Forms of Types 6)
\\[1ex]
	(8)		\> $\pcase{\delta \in \{ 
				MkPurify \ \delta_2,~
				MkPureJoin \ \delta_3 \ \delta_4,~
				MkPureBot \} }$
\\
	(9)		\> $H \ ; \ \delta \leadsto \delta'$
	 		\> (Progress of Purity 5 8 4)
\\
	(10)		\> $\pstep{H}{t}$
			\> (EvMaskWit 10)
\\[1ex]
	(11)		\> $\pcase{\delta = \un{\rpure~ \sigma}}$
\\
	(12)		\> $\pstep{H}{t}$
			\> (EvMaskApp 11)
}


The remaining cases are similar to the TyApp case.

\end{proof}