
\clearpage{}
% -----------------------------------------------------------------------------
\begin{lemma}[Commutable Actions Yield Commutable Residues]

\medskip
\statement{
	If~~	& $(1)$~~ $\eiJudge{H}{t_1}{H \succ R_1}{t_1'}{B_1}$ \\
	~and~	& $(2)$~~ $\eiJudge{H}{t_2}{H \succ R_2}{t_2'}{B_2}$ \\
	~and~	& $(3)$~~ CommutableActions($B_1$,~ $B_2$) \\
	then~	& CommutableResidues($R_1$,~ $R_2$)
}
\end{lemma}

\begin{proof}
By Contradiction.	

\begin{tabbing}
MMx \= MMMMMMMMMMMMMMMMMMMMMMM \= \kill
	(1..3)	\> ...
		\> (assume)
\\
	(4)~	\> Suppose $\neg$ CommutableResidues($R_1$,~ $R_2$)
\\	

	% ------------
	(5)	\> Case:	$l \mtoa{\rho} \mu \in R_1$ and $l \mtoa{\rho} \mu' \in R_2$ 
				for some $l,~ \rho,~ \mu,~ \mu'$. 
\\[1ex]
		\> By inspection of the evaluation rules, the only rules that can add or modify bindings \\
		\> to the heap are (EiAlloc) and (EiUpdate). This results in either $(\ralloc~ l^\rho \in B_1)$ \\
		\> or $(\rwrite~ l^\rho \in B_1)$ or both, and likewise for $B_2$.
\\[1ex]
	(6)	\>~~~~ Case: $(\ralloc~ l^\rho \in B_1)$ and $(\ralloc~ l^\rho \in B_2)$ / EiAlloc / EiAlloc \\
	(7)	\>~~~~~~~~ $\rMakes(B_1) \cap \rMakes(B_2) = \emptyset$ 
		\> (def. Commutable Actions 3 6) 
\\
	(8)	\>~~~~~~~~ $\setof{l} \cap \setof{l} = \emptyset$.~ Contradiction.
		\> (def. Makes~ 8)
\\[1ex]
	(9)	\>~~~~ Case: $(\ralloc~ l^\rho \in B_1)$ and $(\rwrite~ l^\rho \in B_2)$ / EiAlloc / EiUpdate 
\\
	(10)	\>~~~~~~~~ $\rMakes(B_1) \cap \rNeeds(B_2) = \emptyset$ 
		\> (def. Commutable Actions 3 9) 
\\
	(11)	\>~~~~~~~~ $\setof{l} \cap \setof{l} = \emptyset$.~ Contradiction.
		\> (def. Makes, Needs 8)
\\[1ex]
	(12)	\>~~~~ Case: $(\rwrite~ l^\rho \in B_1)$ and $(\ralloc~ l^\rho \in B_2)$ / EiUpdate / EiAlloc \\
		\>~~~~~~~~ Similarly.
\\[1ex]
	(13)	\>~~~~ Case: $(\rwrite~ l^\rho \in B_1)$ and $(\rwrite~ l^\rho \in B_2)$ / EiUpdate / EiUpdate 
\\
	(14)	\>~~~~~~~~ $\rWrites(B_1) \cap \rWrites(B_2) = \emptyset$
		\> (def. Commutable Actions 3 13)
\\	(15)	\>~~~~~~~~ $\setof{l} \cap \setof{l} = \emptyset$. Contradiction.
		\> (def. Writes, Reads 12)
\\[1ex]

	% ------------
	(16)	\> Case:	$(\rmutable~ \rho \in R_1)$ and $(\rconst~ \rho \in R_2)$ \\[1ex]
		\> By inspection of the evaluation rules, the only rule that can add properties \\
		\> to the heap is (EiLetR). When it does so $\rho$ is fresh, so two reductions \\
		\> cannot create a property referring to the same $\rho$. Contradiction.

\end{tabbing}
\end{proof}

