
\begin{figure}

\boxfig{
\begin{center}
\fbox{$\wcJudge{H}{\delta}{\delta'}$}
\end{center}
	
\[	\begin{array}{rlr}
		{H ~;~ \iMkPureBot}
		&\hspace{-1em} ~\lto~ {\un{\rpure~ \bot}}
		&(\trm{EwPureBot})
	\\[1ex]
		{H[~ const~ \rho ~] ~;~}
		{\iMkConst \ \un{\rho}}
		&\hspace{-1em} ~\lto~ {\un{\rconst~ \rho}}
		&(\trm{EwConst})
	\\[1ex]
		{H[~ mutable~ \rho ~] ~;~ }
		{\iMkMutable~ \un{\rho}}
		&\hspace{-1em} ~\lto~ {\un{\rmutable~ \rho}}
		&(\trm{EwMutable})
	\\[1ex]
		{H ~;~ \iMkPurifyRead~ \un{\rho}~ \un{\rconst~ \rho}}
		&\hspace{-1em} ~\lto~ {\un{\rpure~ (\iRead~ \rho)}}
		&(\trm{EwPurifyRead})
	\\[1ex]
		{H ~;~ \iMkPurifyAlloc~ \un{\rho}~ \un{\rconst~ \rho}}
		&\hspace{-1em} ~\lto~ {\un{\rpure~ (\iAlloc~ \rho)}}
		&(\trm{EwPurifyAlloc})
	\end{array}
\]
\[	\frac	{ \wcJudge{H}{\delta_1}{\delta_1'} \qq \wcJudge{H}{\delta_2}{\delta_2'}}
		{ \wcJudge
			{H}
			{\delta_1 \lor \delta_2}
			{\delta_1' \lor \delta_2'} }
		~~~~ \trm{(EwJoinContext)}
\]
\[		{ \wcJudge
			{H}
			{\un{\rpure~ \sigma_1}  \lor \un{\rpure~ \sigma_2}}
			{\un{\rpure~ (\sigma_1 \lor \sigma_2)}} }
		~~~~ \trm{(EwJoinPure)}
\]

} % boxfig
\smallskip
\caption{Witness Phase Change}
\label{fig:WitnessConstruction}
\end{figure}
