
\section{Proof of simulations \label{sec:simproof}}

     All our simulation results can be regarded as special cases of
the result in section \ref{sec:EATMsim}.  That result is proved here.
First we need an auxilliary lemma.
\begin{lemma}
\label{lem:WGtW}
\setcounter{equation}{0}
Suppose $W$ and $W'$ are both sets of subsets of $A$ (ie, elements
of $\Pow \Pow A$) where the set $A$ indexes a set of processes
$\{P_{\setvar{e}} \suchthat \setvar{e} \in A \}$.  If the union of
the elements of $W$ contains the union of the elements of $W'$
\begin{displaymath}
(\bigcup_{w' \in W'} w') \subset (\bigcup_{w \in W} w),
\end{displaymath}
and any $w'$ in $W'$ contains some $w$ from $W$, ie
\footnote{\em This condition
is sometimes \cite{ATP} written as $W' \subset \subset W$}
\begin{displaymath}
\forall w':W' \truethat \exists w:W \truethat w' \supset w
\end{displaymath}
then
\begin{displaymath}
(\begin{array}{c} \ndchoice \\ w' \in W' \end{array}
\begin{array}{c} \choice \\ e' \in w' \end{array} P_e) \sqsupseteq
(\begin{array}{c} \ndchoice \\ w \in W \end{array}
\begin{array}{c} \choice \\ e \in w \end{array} P_e)
\end{displaymath}
\end{lemma}
\begin{proof}
First we show
\begin{equation}
a \choice b \sqsupseteq a \ndchoice (a \choice b \choice c)
\label{eq:abGtaabc}
\end{equation}
This follows because
\begin{eqnarray*}
a & \sqsupseteq & a \ndchoice (a \choice c) \\
b & \sqsupseteq & a \ndchoice b
\end{eqnarray*}
both of which are due to $A \sqsupseteq A \ndchoice B$.
Then monotonicity of $\choice$ gives
\begin{displaymath}
a \choice b \sqsupseteq
(a \ndchoice (a \choice c)) \choice (a \ndchoice b) =
a \ndchoice ((a \choice c) \choice b)
\end{displaymath}
where the equality depends on distribution of $\ndchoice$ over
$\choice$.  This yields \ref{eq:abGtaabc}.  Now, introduce
$w_1$ and $\cal W$ satisfying
$w_1 \subset w' \subset {\cal W}$, and identify
\begin{eqnarray*}
a & = & \begin{array}{c} \choice \\ e \in w_1 \end{array} P_e \\
b & = & \begin{array}{c} \choice \\ e \in w' - w_1 \end{array} P_e \\
c & = & \begin{array}{c} \choice \\ e \in {\cal W} - w' \end{array} P_e.
\end{eqnarray*}
\ref{eq:abGtaabc} becomes
\begin{equation}
\begin{array}{c} \choice \\ e \in w' \end{array} P_e \sqsupseteq
(\begin{array}{c} \choice \\ e \in w_1 \end{array} P_e) \ndchoice
(\begin{array}{c} \choice \\ e \in {\cal W} \end{array} P_e).
\label{eq:WGtWW}
\end{equation}
If $w_1 \in W$,
\begin{displaymath}
\begin{array}{c} \choice \\ e \in w_1 \end{array} P_e \sqsupseteq
(\begin{array}{c} \ndchoice \\ w \in W \end{array}
\begin{array}{c} \choice \\ e \in w \end{array} P_e)
\end{displaymath}
because $A \sqsupseteq A \ndchoice B$.
If, also, ${\cal W} = \bigcup_{w \in W} w$,
\begin{displaymath}
\begin{array}{c} \choice \\ e \in {\cal W} \end{array} P_e =
(\begin{array}{c} \choice \\ w \in W \end{array}
\begin{array}{c} \choice \\ e \in w \end{array} P_e) \sqsupseteq
(\begin{array}{c} \ndchoice \\ w \in W \end{array}
\begin{array}{c} \choice \\ e \in w \end{array} P_e)
\end{displaymath}
because $A \choice B \sqsupseteq A \ndchoice B$.
Subsituting these two results in \ref{eq:WGtWW}, using monotonicity and
idempotence of $\ndchoice$, gives
\begin{displaymath}
\begin{array}{c} \choice \\ e \in w' \end{array} P_e \sqsupseteq
(\begin{array}{c} \ndchoice \\ w \in W \end{array}
\begin{array}{c} \choice \\ e \in w \end{array} P_e).
\end{displaymath}
This inequality depended only on the assumptions that there existed
$w_1 \in W$ such that $w_1 \subset w'$, and that
$w' \subset \bigcup_{w \in W} w$.
Monotoniciy and idempotence of $\ndchoice$ now establish the lemma.
\end{proof}

     Now, suppose $G$ is a simulation
in the sense of definition \ref{def:EATMsim} from
the EATM $(S, A, T, U, V)$ to the ATM $(S', A, T', W')$.

\begin{lemma}
There exists a function $I^U:S \rightarrow \Nat $ such that
\begin{displaymath}
\forall j:U (i) \truethat I^U (j) < I^U (i)    \label{index}
\end{displaymath}
\end{lemma}
{\bf Proof}: $I^U$ can be constructed as
\begin{displaymath}
I^U (i) = \min \{ n \suchthat 
		  \tilde{U}^n \{i\} = \emptyset \}
\end{displaymath}
Well-definedness of this function is guaranteed by the nilpotence of $U$.
The required property (which will be used in a proof by complete
induction) follows easily.
\newline

\begin{definition}
\label{def:X'}
For any $i'$ in $\ran G$ define
\begin{displaymath}
X' (i') = \begin{array}{c} \Ndchoice \\ j \infix{G} i' \end{array} \function{Proc} (j)
\label{Xdef}
\end{displaymath}
\end{definition}

\begin{lemma}
\label{lem:ProcGtX'}
If $i \infix{G} i'$,
\begin{displaymath}
\symbol{Proc} (i) \sqsupseteq X' (i').
\end{displaymath}
\end{lemma}
\begin{proof}
From the law $A \sqsupseteq A \ndchoice B$.
\end{proof}

\begin{corollary}
\label{cor:RGtR}
If $i \infix{G} i'$,
\begin{displaymath}
R (w, T (i)) (\symbol{Proc}) \sqsupseteq R (w, T' (i')) (X')
\end{displaymath}
for any $w \subset \dom T (i)$.
\end{corollary}
\begin{proof}
By clauses 1 and 2 in \ref{def:EATMsim}, $T (i) (e) \infix{G} T' (i') (e)$
for and $e$ in $\dom T (i)$.  So, by the lemma
\begin{displaymath}
\function{Proc} (T (i) (e)) \sqsupseteq X' (T' (i') (e))
\end{displaymath}
The definition of $R$, and monotonicity of the choice operation,
then imply the corollary.
\end{proof}

We can now derive the principle lemma needed to prove
theorem \ref{th:EATMsim}:
\begin{lemma}
\label{lem:ProcGtP}
\setcounter{equation}{0}
If $i \infix{G} i'$ then
\begin{displaymath}
\function{Proc} (i) \sqsupseteq
 \begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\end{displaymath}
\end{lemma}
\begin{proof} We use complete induction.  The induction hypothesis is that the
lemma is satisfied for all states $j$ in $\dom G$ with $I^U (j) < n$,
and we must show that it holds for any state $i$ with $I^U (i) = n$.
First we show
\begin{equation}
P (u, w, T (i)) (\symbol{Proc}) \sqsupseteq
\begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\label{PGtR}
\end{equation}
for any $(u, w) \in V (i)$.
There are two cases to consider: $u = \emptyset$ and $u \not= \emptyset$.

Case I: $P$ reduces to $R$, and
\begin{displaymath}
\begin{array}{ll}
R (w, T (i)) (\symbol{Proc}) \sqsupseteq &
R (w, T' (i')) (X') \sqsupseteq \\ &
\begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\end{array}
\end{displaymath}
where the first inequality follows from lemma \ref{cor:RGtR}
and the second inequality uses final clause in the definition
of $G$, together with lemma \ref{lem:WGtW}, choosing $W = \{ w \}$.

Case II: $P$ contains two terms.  First
\begin{displaymath}
\begin{array}{ll}
Q (u) (\symbol{Proc}) =  &
\begin{array}{c} \ndchoice \\ j \in u \end{array} \function{Proc} (j)
\sqsupseteq \\ &
\begin{array}{c} \ndchoice \\ j \in u \end{array}
\begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
= \\ &
\begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\end{array}
\end{displaymath}
The first inequality follows because,
according to the third clause in the definition of $G$, for each
term in the left-hand side $j \infix{G} i'$.  So, by
the properties of $I^U$, the induction hypothesis is applicable to
the individual terms---the inequality then follows
from monotonicity of $\ndchoice$.
The subsequent equality is due to idempotence of $\ndchoice$.
The second term in $P$ is
\begin{displaymath}
\begin{array}{l}
Q (u) (\symbol{Proc}) \choice R (w, T (i))(\symbol{Proc})
\sqsupseteq \\
( \begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array}
  R (w', T' (i')) (X') ) \choice R (w, T'(i'))(X')
= \\
 \begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array}
 R (w' \cup w, T' (i')) (X')
\sqsupseteq \\
\begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\end{array}
\end{displaymath}
The first inequality depends on monotonicity of $\choice$,
using the result above and corollary \ref{cor:RGtR}.
The middle equality follows from the definition of $R$,
using the fact that $\choice$ distributes over $\ndchoice$.
The final inequality is an application of \ref{lem:WGtW} with
$W = \{ \setvar{w}' \cup w \suchthat \setvar{w}' \in W' (i') \}$.
In $P$, these two terms are combined non-deterministically.  Due to
the monotonicity and idempotence of $\ndchoice$, $P$ satisfies
the same inequality as its two terms.  This establishes
\ref{PGtR}, and the induction step follows from the equation
satisfied by $\symbol{Proc} (i)$, namely
\begin{displaymath}
\function{Proc} (i) = \begin{array}{c} \ndchoice \\ (u, w) \in W (i) \end{array}
		      P (u, w, T (i)) (\symbol{Proc}),
\end{displaymath}
using monotonicity and idempotence of $\choice$.
\end{proof}

Now, from the definition \ref{def:X'}, lemma \ref{lem:ProcGtP}, and
the monotonicity and idempotence of $\ndchoice$,
\begin{displaymath}
X' (i') \sqsupseteq
 \begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (X')
\end{displaymath}
On the other hand, by definition, the system $\symbol{Proc}'$ is the
least solution of
\begin{displaymath}
\symbol{Proc}' (i') =
 \begin{array}{c} \ndchoice \\ w' \in W' (i') \end{array} R (w', T' (i')) (\symbol{Proc}')
\end{displaymath}
Since least fixpoints are also least pre-fixpoints\footnote{A
pre-fixpoint of $F$ satisfies $X \sqsupset F X$}, we can conclude that
\begin{displaymath}
X' (i') \sqsupseteq \symbol {Proc}' (i')
\end{displaymath}
Theorem \ref{th:EATMsim} follows from lemma \ref{lem:ProcGtX'}.

