
\clearpage{}
% -----------------------------------------------------------------------------
\begin{lemma}[Non-Interfering Effects Yield Commutable Actions]

\begin{tabular}{llll}
	If~~		&~ (1)~ $\tyJudge{\Gamma}{\Sigma_1}{t_1}{\tau_1}{\sigma_1}$	
			& ~~and~~ 
			&  (2)~ $\eiJudge{H_1}{t_1}{H_1'}{t_1'}{B_1}$ 
\\
	~and~~		&~ (3)~ $\tyJudge{\Gamma}{\Sigma_2}{t_2}{\tau_2}{\sigma_2}$
			& ~~and~~ 
			&  (4)~ $\eiJudge{H_2}{t_2}{H_2'}{t_2'}{B_2}$ 
\\
	~and~~		& \mc{3}{~ (5)~ NonInterfering($\Gamma,~ \sigma_1,~ \sigma_2$)} \\
	then~~		& \mc{3}{~CommutableActions($B_1,~ B_2$)}
\end{tabular}

\end{lemma}

\begin{proof}
\medskip
After assuming (1..5) we prove the six conjuncts of CommutableActions$(B_1,~ B_2)$ in turn, each using proof-by-contradiction.
\tabbedstmts{
	\textbf{(G1)}
		\> Suppose $\neg(\rMakes(B_1) \cap \rMakes(B_2) = \emptyset)$
\\
(6)		\> ~~ Case: $o \in \rMakes(B_1)$ and $o \in \rMakes(B_2)$ 
				for $o$ one of~
				$\rho$,~
				$(\rmutable~ \rho)$,~ 
				$(\rconst~ \rho)$ \\
(7)		\> ~~~~ By the definition of $\rMakes()$ these properties must come from $\rcreate$ actions. \\
(8)		\> ~~~~ By inspection of evaluation rules, the only rule that causes these actions is (EiLetR), \\
		\> ~~~~~~ and when it does the $\rho$ is fresh. Hence, the same $o$ cannot be in $\rMakes(B_2)$.
\\
(9)		\> ~~Case: $o = l^\rho$ \\
(10)		\> ~~~~ Similarly to previous, these must come from $\ralloc$ actions via (EiAlloc), when \\
		\> ~~~~ it evaluates the $l$ is fresh. Hence, the same $l^\rho$ cannot be in $\rMakes(B_2)$.
\\[1ex]
	\textbf{(G2)}
		\> Suppose $\neg(\rNeeds(B_1) \cap \rMakes(B_2) = \emptyset)$  \\
(11)		\> ~~ Case: $o \in \rNeeds(B_1)$ and $o \in \rMakes(B_2)$ 
				for $o$ one of~
				$\rho$,~
				$(\rmutable~ \rho)$,~ 
				$(\rconst~ \rho)$ \\
(12)		\> ~~~~ For $o \in \rNeeds(B_1)$ these come from $\rtest$s via (EiAlloc),~ (EiUpdate),~ or (EiSuspend). \\
(13)		\> ~~~~ For $o \in \rMakes(B_2)$ these come from $\rcreate$ actions via (EiLetR). 
\\[1ex]
(14)		\> ~~~~ $\rho$ is fresh
		\> (EiLetR 13)
\\
(15 16)		\> ~~~~ $\eiJudge{H_3}{\kletregion~ r~ \kin~ t_3}{H_3'}{v_3^\circ}{B_3}$,~~ 
				$(\rcreate~ o) \in B_3$ \\
		\> ~~~~~~~ for some $H_3,~ H_3',~ r,~ t_3,~ v_3^\circ,~ B_3$
		\> (Inv. 4 13)
\\[1ex]
(17)		\> ~~~~ Case: Derivation of (2) involves (EiAlloc).
\\

(18 19)		\> ~~~~~~ $\eiJudge{H_4}{K~ \un{\rho}~ \ov{\varphi'}~ \ov{t'}}{H_4'}{v_4^\circ}{B_4}$,~~
				$(\rtest~ o) \in B_4$ \\
		\> ~~~~~~~~ for some $H_4,~ H_4',~ \varphi',~ t'$
		\> (Inv. 2 12)
\\[1ex]
(19)		\> ~~~~~~ $r \in \ifv(t_2)$
		\> (14 15 17 18)
\\
(20)		\> ~~~~~~ $r : \% \in \Gamma$
		\> (3 19) BROKEN...... FIXME
		
\\[1ex]
\\
		\> By the corresponding typing rules and \\
		\> ~~~~ (KiHandle), (KiConst) and (KiMutable) we have $\alpha \in \Sigma$. However, as per \\
		\> ~~~~ the previous. case any $\rho$ in $\rMakes(B_2)$ is fresh, hence $\alpha \notin \Sigma$. Contradiction.
\\
		\> Case: $\alpha$ one of ~$\rmalloc~ l^\rho$,~ $\rpalloc~ l^\rho$ \\
		\> ~~ Similarly to previous case. If we had $\rmalloc~ l^\rho \in \rNeeds(B_1)$ then we must have \\
		\> ~~ $l : \tau \in \Sigma$ for some $\tau$. However, by (EiAlloc) $l$ must be fresh. 
\\
	\textbf{(G3)}
		\> $\rMakes(B_1) \cap \rNeeds(B_2) = \emptyset$ \\
		\> Similarly to previous goal.
\\
	\textbf{(G4)}
		\> $\rWrites(B_1) \cap \rWrites(B_2) = \emptyset$ \\
	(6)	\> Suppose $(\rwrite~ l^\rho \in B_1)$ and $(\rwrite~ l^\rho \in B_2)$~ for some $\rho,~ l$ \\
	(7)	\> ~~ $\rho \in \Sigma$
		\> \hspace{-5em}(As per G1,~ $\rho$ cannot be fresh 6 -- LEMMIFY) 
\\
	(8)	\> ~~ $\iWrite~ \rho \in \sigma_1$ ~~~~~~and~~ $\iWrite~ \rho \in \sigma_2$
		\> \hspace{-5em}(Visible Actions 1 2 7 6 )  
\\
	(9)	\> ~~ $\rWrites(\sigma_1) = \emptyset$ ~~~~or~~~ $\rWrites(\sigma_2) = \emptyset$
		\> \hspace{-5em}(def. NonInterfering 5) 
\\
		\> ~~ Contradiction.
		\> \hspace{-5em}(8 9)
\\
	\textbf{(G5)}
		\> $\rWrites(B_1) \cap \rReads(B_2) = \emptyset$ \\
	(10)	\> Case: $(\rwrite~ l^\rho \in B_1)$ and $(\rmread~ l^\rho \in B_2)$~ for some $\rho,~ l$. 
\\
	(11)	\> ~~ $\rho \in \Sigma$
		\> \hspace{-5em}(As per G1,~ $\rho$ cannot be fresh 6 -- LEMMIFY) 
\\
	(12)	\> ~~ $\iWrite~ \rho \in \sigma_1$ ~~and~~  $\iRead~ \rho \in \sigma_2$
		\> \hspace{-5em}(Visible Actions 1 2 10 11) 
\\
	(14)	\> ~~ $w : \iMutable~ \rho \in \Gamma$
		\> \hspace{-5em}(By -- LEMMIFY)
\\
	(15)	\> ~~ $\rWrites(\sigma_1) = \emptyset$  \\
		\> ~~~~ or ~~~ $\setof{\iRead~ \varphi \in \sigma_2 ~~\trm{where}~~ w : \iMutable~ \varphi \in \Gamma} = \emptyset$
		\> (def. NonInterfering 5)
\\
	(16)	\> ~~ Contradiction.
		\> \hspace{-5em}(12..15)
\\
	\textbf{(G6)}	
		\> $\rReads(B_1) \cap \rWrites(B_2) = \emptyset$ \\
		\> Similarly to previous goal.
}	

\end{proof}