

\clearpage{}
% -----------------------------------------------------------------------------
\begin{lemma}[Visible Actions]
If the reduction of an expression reads, writes or allocates mutable data in a pre-existing region then it has the corresponding effect.

\medskip
\begin{tabular}{llll}
	If~	& $\tyJudgeES{t}{\tau}{\sigma}$ & ~~and~~	& $\eiJudge{H}{t}{H'}{t'}{B}$ \\
	~and~~ 	& \mc{3}{$\Sigma \models H$ ~~and~~ $\Sigma \in H$ ~~and~~ $\un{\rho} \in \Sigma$} \\
	then~~  & \mc{3}{(If $\rmread~   l^\rho \in B$ for some $l$ then $\suJudgeGS{\iRead~  \un{\rho}}{\sigma}$)} \\
	~and~~	& \mc{3}{(If $\rwrite~~~ l^\rho \in B$ for some $l$ then $\suJudgeGS{\iWrite~ \un{\rho}}{\sigma}$)} \\
	~and~~	& \mc{3}{(If $\rmalloc~ l^\rho \in B$ for some $l$  then $\suJudgeGS{\iAlloc~ \un{\rho}}{\sigma}$)}
\end{tabular}
\end{lemma}

\begin{proof}
By induction over the derivation of $\eiJudge{H}{t}{H'}{t'}{B}$.

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


\medskip
\pCase $t = x$ \\
Can't happen as there is no corresponding evaluation rule for free vars.

\medskip
\pCase $t$ one of~ $l,~ (),~ \teLAM{a}{\kappa}{t},~ \teLam{x}{\tau}{t}$ \\
Can't happen as the corresponding evaluation rules yield no actions.

\medskip
% -------------------------------------
\pCase $t = t_1~ \varphi_2$ / TyAppT / EiAppT \\

\[	\infer	{ (\un{1})~
		  \tyJudgeGS
			{t_1~ \varphi_2}
			{\varphi_{12}[\varphi_2/a]}
			{\sigma_1}
		}
		{ (6)~
		  \tyJudgeGS
			{t_1}
			{\tyForall{a}{k_{11}}{\varphi_{12}}}
			{\sigma_1}
		 \quad
		 (7)~
		 \kiJudgeGS
			{\varphi_2}
			{\kappa_{11}}
		}
\]

\[	\infer	{ (\un{2})~
		  \eiJudge
		  	{H_0}	{t_1~ \varphi_2}
			{H_2}	{v^\circ}
			{B_1 \cup B_2}
		}
		{ (8)~
		  \eiJudge
			{H_0}	{t_1}
			{H_1}	{\teLAM{a}{\kappa_{11}}{t_{12}}}
			{B_1}
		  \quad
		  (9)~
		  \eiJudge
			{H_1}	{t_{12}[\varphi_2/a]}
			{H_2}	{v^\circ}
			{B_2}
		}
\]

\tabbedstmts{
	(\un{3..5})~
		\> $\Sigma \models H$,~ $\Sigma \vdash H$,~ $\un{\rho} \in \Sigma$
		\> (assume)
\\
	(11..15)
		\> $\tyJudge
			{\Gamma}
			{\Sigma'}
			{\teLAM{a}{\kappa_{11}}{t_{12}}}
			{\tyForall{a}{\kappa_{11}}{\varphi_{12}}}
			{\bot}$ \\
		\> ~~ 	$\Sigma' \supseteq \Sigma$,~ 
			$\Sigma' \models H_1$,~ 
			$\Sigma' \vdash H_1$,~ 
			$\suJudge{\Gamma}{\Sigma'}{\bot}{\sigma_1}$
		\> (Preservation 1 8 3 4)
\\
	(16)	\> $\tyJudge
			{\Gamma,~ a : \kappa_{11}}
			{\Sigma'}
			{t_{12}}
			{\varphi_{12}}
			{\bot}$ 
		\> (Inv. TyAbsT 11)
\\
	(17)	\> $\kiJudge
			{\Gamma}
			{\Sigma'}
			{\varphi_2}
			{\kappa_{11}}$
		\> (Weak. Store Typing 7 12)
\\
	(18)	\> $\tyJudge
			{\Gamma}
			{\Sigma'}
			{t_{12}[\varphi_2/a]}
			{\varphi_{12}[\varphi_2/a]}
			{\bot}$
		\> (Sub Type/Value 16 17)
\\
	(19)	\> If $(\rmread~ l^\rho \in B_1$ ... 
			$\suJudge
				{\Gamma}
				{\Sigma'}
				{\iAlloc~ \un{\rho}}
				{\sigma_1})$
		\> (IH 6 8 3 4 5)
\\	
	(20)	\> $\un{\rho} \in \Sigma'$
		\> (Def. $\supseteq$ 5 12)
\\
	(21)	\> If $(\rmread~ l^\rho \in B_2$ ...
			$\suJudge
				{\Gamma}
				{\Sigma'}
				{\iAlloc~ \un{\rho}}
				{\bot})$
		\> (IH 18 9 13 14 20)
}
\medskip
% -------------------------------------
\pCase $t = t_1~ t_2$  \\
Similarly to previous case.


\clearpage{}
% -------------------------------------
\pCase $t = \kletregion...$ / TyLetR / EiLetR

\[	\ruleIL	{TyLetR}
		{ \begin{array}{l}
			(6)~ \ov{\delta_i} \ \trm{well formed}
		  	\qq
			(7)~ \ov{\kiJudgeGS
				{\delta_i}
				{\kappa_i}}^{\ i}
		  \\
			(8)~ {r \notin \ifv(\tau)}
			\qq\qq
		        (9)~ \tyJudge	
				{\Gamma,~ r : \%, \ \ov{w_i : \kappa_i}}
				{\Sigma}
				{t}
				{\tau}
				{\sigma} 
		  \end{array}
		}
		{ (\un{1})~ 
		  \tyJudgeGS
			{\teLetR{r}{\ov{w_i = \delta_i}}{t}} 
			{\tau} 
			{\sigma \setminus {(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}}
		}
\]
\[	\ruleIL	{EiLetR}
		{ \begin{array}{ll}
		  (10)~ \rho'~ \trm{fresh} 
		  \quad
		  (11)~ \ov{\Delta_i = \trm{witOf} (\delta_i[\un{\rho'}/x])}^{~i}
		  \quad
		  (12)~ \ov{\pi_i    = \trm{propOf}(\delta_i[\un{\rho'}/x])}^{~i}
		  \\
		  (13)~ \eiJudge
		 	{H_0}	{\teWithR{\rho'}{\ov{\Delta_i}}{t[\un{\rho'}/x~~ \ov{\Delta_i/w_i}]}}
			{H_1}	{v^\circ}
			{B_1}
		  \end{array}
		}
		{ (\un{2})~ 
			\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}}
		}
\]

\tabbedstmts{
	(\un{3..5})~
		\> 	$\Sigma \models H_0$,~ 
			$\Sigma \vdash H_0$,~ 
			$\un{\rho} \in \Sigma$ 
		\> \hspace{-3em}(assume)
\\
	(14)~	\> let $\Sigma' = \Sigma,~ \un{\rho'},~ \ov{\Delta_i}$
		\> 
\\
	(15)~	\> $\kiJudge{\Gamma}{\Sigma'}{\un{\rho'}}{\%}$
		\> \hspace{-3em}(TyHandle 14)
\\
	(16)~	\> $\ov{
			\kiJudge
				{\Gamma}
				{\Sigma'}
				{\Delta_i}
				{\kappa_i}}^{~ i}$
		\> \hspace{-3em}(7 12 14)
\\	
	(17)~	\> $\tyJudge	
			{\Gamma,~ r : \%, \ \ov{w_i : \kappa_i}}
			{\Sigma'}
			{t}
			{\tau}
			{\sigma}$
		\> \hspace{-3em}(Weak. Store Typing 10 14)
\\
	(18)~	\> $\tyJudge
			{\Gamma}
			{\Sigma'}
			{t      [\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 17 15 16)
\\
	(19)~	\> $\tyJudge
			{\Gamma}
			{\Sigma'}
			{t      [\un{\rho'}/r~ \ov{\Delta_i/w_i}]}
			{\tau   [\un{\rho'}/r]}
			{\sigma [\un{\rho'}/r]}$
		\> \hspace{-3em}(No Wit. Vars in Types or effects 18)
\\[1ex]
	(20)~	\> $\Gamma
			~|~ \Sigma'
			\vdash	{\teWithR
					{\un{\rho'}}
					{\ov{\Delta_i}}
					{t      [\un{\rho'}/r~ \ov{\Delta_i/w_i}]}
				}$
		\> \hspace{-3em}(TyWithR 14 19 11)
\\
		\> \hspace{1.5em}
		   $ ~::~ {\tau   [\un{\rho'}/r]}
		     ~;~  {\sigma [\un{\rho'}/r] \setminus 
				(\iRead~ \un{\rho} \lor \iWrite~ \un{\rho} \lor \iAlloc~ \un{\rho})}$
\\[1ex]
	(21)~	\> $\Gamma
			~|~ \Sigma'
			\vdash	{\teWithR
					{\un{\rho'}}
					{\ov{\Delta_i}}
					{t      [\un{\rho'}/r~ \ov{\Delta_i/w_i}]}
				}$
		\> \hspace{-3em}(9. Def. Subst 20)
\\
		\> \hspace{1.5em}
		   $ ~::~ {\tau}
		     ~;~  {\sigma \setminus 
				(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r) [\un{\rho'}/r]}$
\\[1ex]
	(22)~	\> $\Gamma
			~|~ \Sigma'
			\vdash	{\teWithR
					{\un{\rho'}}
					{\ov{\Delta_i}}
					{t      [\un{\rho'}/r~ \ov{\Delta_i/w_i}]}
				}$
		\> \hspace{-3em}(Prop of Subst. 21)
\\
		\> \hspace{1.5em}
		   $ ~::~ {\tau}
		     ~;~  {\sigma \setminus 
				(\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}$
		\> \hspace{-3em}(we only have R/W/A Effs.)
\\
	(23)~	\> If $\rwrite~ l^\rho \in B_1 ~...~ 
			\suJudge
				{\Gamma}
				{\Sigma'}
				{\iAlloc~ \un{\rho}}
				{\sigma \setminus (\iRead~ r \lor \iWrite~ r \lor \iAlloc~ r)}$
\\
		\>\> \hspace{-3em}(IH 22 13 3 4 5)
}


\medskip
% -------------------------------------
\pCase $t = \kwithregion...$ / TyWithR / EiWithR

\[	\ruleIL	{TyWithR}
		{ (6)~ 
			\tyJudge
			{\Gamma}
			{\Sigma,~ \un{\rho},~ \ov{\Delta_i}}
			{t}
			{\tau}
			{\sigma}
		}
		{ (\un{1})~ 
			\tyJudgeGS
			{\teWithR{\un{\rho}}{\ov{\Delta_i}}{t}}
			{\tau}
			{\sigma \setminus {(\iRead~ \un{\rho} \lor \iWrite~ \un{\rho} \lor \iAlloc~ \un{\rho})}}
		}
\]

\[	\ruleIL	{EiWithR}
		{ (8)~
		  \eiJudge
			{H_0,~ \un{\rho},~ \ov{\rpropOf(\Delta_i)}^{~ i}}	
				{t}
			{H_1}	{v^\circ}
			{B_1}
		}
		{ (\un{2})~ 
			\eiJudge
			{H_0}	{\teWithR{\rho}{\ov{\Delta_i}}{t}}
			{H_1}	{v^\circ}
			{B_1}
		}
\]

\tabbedstmts{
	(\un{3..5})~
		\> $\Sigma \models H_0$,~ $\Sigma \vdash H_0$,~ $\un{\rho'} \in \Sigma$ 
		\> (assume)
\\
	(9)	\> let $\Sigma' = \Sigma,~ \un{\rho},~ \ov{\Delta_i}$
\\
	(10)	\> let $H' = H_0,~ \rho,~ \ov{\rpropOf(\Delta_i)}^{~ i}$ 
\\
	(11)	\> $\Sigma' \vdash H'$
		\> (Well Typed Store 3 9 10)
\\
	(12)	\> $\Sigma' \models H'$
		\> (Store Model 4 9 10)
\\
	(13)	\> If $\rmread~ l^{\rho '} \in B_1 ~...~ 
			\suJudgeGS{\iAlloc~ \un{\rho '}}{\sigma}$
		\> (IH 6 8 9..12)
\\
	(14)	\> $\rho' \ne \rho$
		\> (6)
\\
	(15)	\> If $\rmread~ l^{\rho '} \in B_1 ~...~ 
			\suJudgeGS
				{\iAlloc~ \un{\rho '}}
				{\sigma \setminus (\iRead~ \rho \lor \iWrite~ \rho \lor \iAlloc~ \rho)}$
\\
		\> \> (13 14)
}


\clearpage{}
% -----------------
\pCase $t = K~ \ov{\varphi}~ \ov{t}$ / TyAlloc / EiAlloc

\[	\ruleIL	{TyAlloc}
		{ \begin{array}{ll}
  	  		& 
	  		(6)~ \ov{\tyJudgeGS
				{t}
				{\tau_i	[\un{\rho}/r~ \ov{\varphi'/a}]}
				{\sigma_i}}^{\: i \gets 0..n} 
	  	  \\
         		(7)~ \kiJudgeGS
				{\un{\rho}}
				{\%} 
	  	  &
	  		(8)~ 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{t}}
			{T~ \un{\rho}~ \ov{\varphi'}}
			{\sigma_0 \lor \sigma_1 ... \lor \sigma_n \lor \iAlloc~ \un{\rho}}
		}
\]
\[	\ruleIL	{EiAlloc}
		{ (9)~ \ov{ \eiJudge
			{H_j}		{t_j}
			{H_{j+1}}	{v_j^\circ}
			{B_j}
		     }^{~ j \;\gets\; 0..n}
		  \quad
		  (10)~ \rho \in H_{n+1}
		  \quad
		  (11)~ l~ \trm{fresh}
		}
		{ (\un{2})~
			\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}
\[	(12)~ B' = \left\{
	\begin{array}{cll}
	\setof{\rmalloc~ l^\rho} & \rif~~ \rmutable~ \rho \in H_{n+1}, \\
	\setof{\rpalloc~ l^\rho} & \rif~~ \rconst~ \rho \in H_{n+1}.
	\end{array}\right.
\]

\tabbedstmts{
	(\un{3..5})~
		\> $\Sigma \models H_0$,~ $\Sigma \vdash H_0$,~ $\un{\rho'} \in \Sigma$ 
		\> \hspace{-2em}(assume)
\\
	(13)	\> If $\rmread~ l^{\rho '} \in B_j$ ... 
			$\suJudge
				{\Gamma}
				{\Sigma'}
				{\iAlloc~ \un{\rho '}}
				{\sigma_j}$
		\> \hspace{-2em}(Via IH, sim. to TyAppT case)
\\
	(\un{14})
		\> $\rmalloc~ l^{\rho'} \in B'$
		\> \hspace{-2em}(assume)
\\
	(15)	\> ~~ Case $\un{\rho'} \ne \un{\rho}:$
\\
	(16)	\> ~~~~ Case $(\rmutable~ \rho) \in H_{n+1}$
\\
	(17)	\> ~~~~~~~ $B' = \setof{\rmalloc~ l^\rho}$
		\> \hspace{-2em}(12 16)
\\
	(18)	\> ~~~~~~ Suppose $\neg(\suJudge
					{\Gamma}
					{\Sigma'}
					{\iAlloc~ \un{\rho'}}
					{\iAlloc~ \un{\rho}})$
\\
	(19)	\> ~~~~~~ Contradiction
		\> \hspace{-2em}(14 15 17)
\\
	(20)	\> ~~~~ Cases for $(\rconst~ \rho) \in H_{n+1}$ and $B' = \emptyset$ similarly.
\\
	(21)	\> ~~ Case $\un{\rho'} = \un{\rho}:$
\\
	(22)	\> ~~~~ Case $(\rmutable~ \rho) \in H_{n+1}$
\\
	(23)	\> ~~~~~~ $B' = \setof{\rmalloc~ l^\rho}$
		\> \hspace{-2em}(12 22)
\\
	(24)	\> ~~~~~~ $\suJudge{\Gamma}{\Sigma'}{\iAlloc~ \un{\rho}}{\iAlloc~ \un{\rho}}$
		\> \hspace{-2em}(immediate)
\\
	(25)	\> If $\rmalloc~ l^{\rho '} \in B^{'}$ then 
			$\suJudge
				{\Gamma}
				{\Sigma'}
				{\iAlloc~ \un{\rho}}
				{\iAlloc~ \un{\rho'}}$
		\> \hspace{-2em}(Imp. Intro 14 - 24)
}


% -------------------------------------
\pCase $t$ = $\iupdate...$ / TyUpdate / EiUpdate

\[	\infer	{ (\un{1})~
			\tyJudgeGS
			{\iupdate_{K,i} \ \un{\rho} \ \ov{\varphi} \ \un{\rmutable~ \rho} \ t_1 \ t_2}
			{()}
			{\sigma \lor \sigma' \lor \iWrite \ \un{\rho}}
		}
		{ \begin{array}{ll}
		  	(6)~ \kiJudgeGS
				{\delta}
				{\iMutable \ \varphi}
		  &	(8)~ \tyJudgeGS
				{t_2}
				{\tau_i[\un{\rho}/r~ \ov{\varphi/a}]}{\sigma'} 
		  \\	(7)~ \tyJudgeGS
				{t_1}
				{T \ \un{\rho} \ \ov{\varphi}}
				{\sigma}
		  &	(9)~ K :: \forall(r : \%)(\ov{a : \kappa}). \ov{\tau} \to T \ r \ \ov{a} 
			 	\in \trm{ctorTypes}(T)
		  \end{array}
		}
\]
\[	\infer	{ (\un{2})~
			\eiJudge
			{H_0}	{\rupdate_{K,i}~ \un{\rho}~ \ov{\varphi}~ \un{\rmutable~ \rho}~ t_1~ t_2~}
			{H_2'}	{()}
			{B_3}
		}
		{ \begin{array}{ll}
		  (10)~ \eiJudge
			{H_0}	{t_1}
			{H_1}	{l}
			{B_1}
		  \qq \qq\qq 	(12)~ B_3  = B_1 \cup B_2 \cup \setof{\rtest~ (\rmutable~ \rho),~ \rwrite~ l^\rho}
		  \\
		  (11)~ \eiJudge
			{H_1}	{t_2}
			{H_2[~\rmutable~ \rho,~ l \mtoa{\rho} C_k~ \ov{v^\circ}~]}
				{u^\circ}
			{B_2~}
		  \quad
			(13)~ H_2' = H_2,~ l \mtoa{\rho} C_K~ v_0^\circ ... u_i^\circ ... v_n^\circ
		  \end{array}
		}
\]

\tabbedstmts{
	(\un{3..5})~
		\> $\Sigma \models H_0$,~ $\Sigma \vdash H_0$,~ $\un{\rho'} \in \Sigma$
		\> \hspace{-2em}(assume)
\\
	(6)	\> If $\rmread~ l^\rho \in B_1$ ... 
			$\suJudge
				{\Gamma}{\Sigma'}
				{\iAlloc~ \un{\rho}}{\sigma}$
		\> \hspace{-2em}(Via IH, sim. to TyAppT case)
\\
	(7)	\> If $\rmread~ l^\rho \in B_2$ ... 
			$\suJudge
				{\Gamma}{\Sigma''}
				{\iAlloc~ \un{\rho}}{\sigma'}$
		\> \hspace{-2em}(Via IH, sim. to TyAppT case)
\\	
	(8)	\> Case: $\rho' \ne \rho$ 
\\
	(9)	\> ~~ $\rwrite~ l^{\rho '} \in \setof{\rtest~ (\un{\rmutable~ \rho}),~ \rwrite~ l^\rho}$
		\> \hspace{-2em}(assume)
\\
	(10)	\> ~~ Suppose $\neg(\suJudge
					{\Gamma}
					{\Sigma''}
					{\iWrite~ \un{\rho'}}
					{\iWrite~ \un{\rho}})$
\\
	(11)	\> ~~ Contradiction
		\> \hspace{-2em}(8 9)
\\
	(12)	\> Case: $\rho' = \rho$
\\
	(13)	\> ~~ $\rwrite~ l^\rho \in \setof{\rtest~ (\un{\rmutable~ \rho}),~ \rwrite~ l^\rho}$
		\> \hspace{-2em}(assume)
\\	
	(14)	\> ~~ $\suJudge
			{\Gamma}
			{\Sigma''}
			{\iWrite~ \un{\rho'}}
			{\iWrite~ \un{\rho'}}$
		\> \hspace{-2em}(immediate)
}

\medskip
% -------------------------------------
\pCase $t = \isuspend...$ \\
Similarly to TyAppT case.


\medskip
% -------------------------------------
\pCase $t$ = $\kcase...$ \\
Similarly to TyAlloc case.


\medskip
% -------------------------------------
\pCase $t = \kmask...$ / TyMask / EiMask\\
\[	\infer	{ (\un{1})~
		  \tyJudgeGS
			{\teMask{\delta}{t}}
			{\tau}
			{\sigma \setminus \sigma'}
		}
		{ (6)~
		  \tyJudgeGS{t}{\tau}{\sigma}
	  	  \quad
	  	  (7)~
		  \kiJudgeGS{\delta}{\iPure~ \sigma'}
		}
\]
\[	\infer	{ (\un{2})~
		  \eiJudge
			{H_0}{\teMask{\delta}{t}}
			{H_1}{v^\circ}
			{B_1 \cup B_2}
		}
		{ (8)~
		  \wiJudge{H_0}{\delta}{\un{\rpure~ \sigma'}}{B_1}
		  \quad
		  (9)~
		  \eiJudge
			{H_0}{t}
			{H_1}{v^\circ}
			{B_2}	
		}
\]

\tabbedstmts{
	(\un{3..5})~
		\> $\Sigma \models H_0$,~ $\Sigma \vdash H_0$,~ $\un{\rho} \in \Sigma$
		\> \hspace{-5em}(assume)
\\
	(10)~ 	\> $\rmread~ l^\rho \notin B_1$,~ $\rwrite~ l^\rho \notin B_1$~ $\rmalloc~ l^\rho \notin B_1$
		\> \hspace{-5em}(Only tests in Wit. Eval. 8)
\\
	(11)~	\> If~ $\rmread~ l^\rho \in B_2$ then $\suJudgeES{\iRead~ \un{\rho}}{\sigma}$
		\> \hspace{-5em}(IH 6 9 3 4 5)
\\[0.5ex]
	(12)~	\> $\rmread~ l^\rho \in B_2$
		\> \hspace{-5em}(assume)
\\
	(13)~	\> ~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma}$
		\> \hspace{-5em}(Imp. Elim. 11 12)
\\
	(14)~	\> ~~~ $\rho \in H_0$
		\> \hspace{-5em}(Store Model 3 5)
\\
	(15)~	\> ~~~ $\rmutable~ \rho \in H_1$
		\> \hspace{-5em}(Actions on Mut. Regions 9 12)
\\
	(16)~	\> ~~~ $\rmutable~ \rho \in H_0$
		\> \hspace{-5em}(Sim. Creat. 9 14 15)
\\
	(17)~	\> ~~~ $\un{\rmutable~ \rho} \in \Sigma$
		\> \hspace{-5em}(Store Model 3 16)
\\[0.5ex]
	(\un{18})~	
		\> ~~ Suppose we had a derivation of~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma'}$
\\
	(19)~	\> ~~~~~~~~ $\kiJudgeGS{\un{\rpure~ \sigma'}}{\iPure~ \sigma'}$
		\> \hspace{-5em}(Prog. Purity 8 7)
\\
	(20)~	\> ~~~~~~~~ $\suJudgeGS{\sigma'}{\bot}$
		\> \hspace{-5em}(SubPure 19)
\\
	(21)~	\> ~~~~~~~ $\neg(\suJudgeGS{\sigma'}{\bot})$
		\> \hspace{-5em}(No Purif. of Impurity 18 17)
\\
	(22)	\> ~~~~~~~ Contradiction
		\> \hspace{-5em}(20 21)
\\
	(23)	\> ~~~ $\neg(\suJudgeGS{\iRead~ \un{\rho}}{\sigma'})$
		\> \hspace{-5em}(Neg. Intro. 18-22)
\\
	(24)~	\> ~~~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma \setminus \sigma'}$
		\> (Prop. of $\setminus$ 13 23)
\\
	(25)~	\> If $\rmread~ l^\rho \in B_1 \cup B_2$ ~then~ $\suJudgeGS{\iRead~ \un{\rho}}{\sigma \setminus \sigma'}$
		\> (Imp. Intro. 12-23 10)
\\[0.5ex]
		\> Cases for $\rwrite~ l^\rho \in B_2$ and $\rmalloc~ l^\rho \in B_2$ similarly.
}

\end{proof}

