\section{Soundness} \label{sec:minimp:system:proof}
\subsection{Soundness of The Monolithic
  Algorithm} \label{sec:minimp:mono:proof}

The soundness of $\mcalgo$ is expressed by the following theorem.

\begin{teom}
  $\model \models \cotriplenoloc{}$ iff for any positive $n$ such that  \\
  $\mcalgo(\model, \cotriplenoloc{}, n) = \textbf{T}$
  \label{teom:mc:sound}
\end{teom}

\noindent\textbf{Proof}
Theorem \ref{teom:mc:sound} is a consequence of lemma
\ref{lema:mc:concretize} and \ref{lema:mc:prop:preserve}. $\qed$

Let $\textsf{concretize}\colon{} \sym \rightarrow{} \dom$ be a
function that maps symbols to concrete values.  Besides, we abuse
$\textsf{concretize}$ by

\begin{itemize}

\item letting $\textsf{concretize}(e)$ denote a concrete value that is obtained
  by replacing every symbol $X$ in a symbolic expression $e$ with
  $\textsf{concretize}(X)$;

\item letting $\textsf{concretize}(\omega)$ denote a state that is
  obtained by 1) replacing every symbolic expression $e$ in a state
  $\omega$ by $\textsf{concretize}(e)$; and then 2) getting rid of the
  path condition;
  

\item letting $\textsf{concretize}(t)$ denote a transition that is
  obtained by 1) replacing the states of $t$ with
  $\textsf{concretize}(\mysrc(t))$ and
  $\textsf{concretize}(\mydest(t))$, respectively; and then 2)
  replacing every symbolic expression $e$ in $\myact(t)$ with
  $\textsf{concretize} (e)$;
  
\item letting $\textsf{concretize}(\rho)$ denote a path that is
  obtained by replacing every transition $t$ in $\rho$ with
  $\textsf{concretize}(t)$.
\end{itemize}

\begin{lema}
  An execution $\pi$ searched by
  $\mcalgo(\model, \cotriplenoloc{}, n)$ is feasible iff there is a
  function $\textsf{concretize}\colon{} \sym \rightarrow{} \dom$ such
  that $\textsf{concretize}(\pi)$ is an execution in the state space
  graph $G$ of $C$ with $n$ processes, and $\psi$ and
  $\myallemptyguard$ hold on $\mysrc(\textsf{concretize}(\pi))$.
  \label{lema:mc:concretize}
\end{lema}

\noindent\textbf{Proof.}  We first show that if $\pi$ is feasible,
$\textsf{concretize}(\pi)$ is in the state space graph of $C$ for some
function $\textsf{concretize}$.  Since $\pi$ is feasible, for any
state $\omega \in \mypathstates(\pi)$, $\mypathcond(\pi)$ is
satisfiable.  So for any such $\omega$, $\textsf{concretize}(\omega)$
is a state in $G$.  Then we need to show that for any
$t \in \mypathtrans(\pi)$,
$\mydest(t) \in I(\mysrc(t), \myproc(t), \alpha)$, where $\alpha$ is
the local transition associated with $\textsf{concretize}(t)$.  This
can be done by induction on $I$.  We skip the induction.

Now we show the other direction.  Let $\pi'$ be an execution in $G$
such that $\psi$ holds on $\mysrc(\pi')$.  We construct a state
$\omega_0 = (s, \textsf{pc})$ by letting $s$ be obtained by assigning
every variable $v$ in $\mysrc(\pi')$ with a fresh new symbol $X$.  At
the same time, let $\textsf{concretize}$ be a function that maps every
such $X$ to the value of such $v$ in $\mysrc(\pi')$.  Let $\textsf{pc}
= \bigwedge\limits_{p \in \nprocs{n}}\myeval{\psi}(s, p)$.  Let
$t\in\mypathtrans(\pi)$ be a transition and be $\omega$ a state in the
searching space of $\mcalgo(\model, \cotriplenoloc{}, n)$.  Let
$\alpha$ be the local transition associated with $t$.  We need to show
that if $\textsf{concretize}(\omega) = \mysrc(t)$, then there is
$\omega' \in I^{\sym}(\omega, \myproc(t), \alpha)$ such that
$\mypathcond(\omega')$ is satisfiable.  This can be done by induction
on $I^{\sym}$.  We skip the induction for brevity. $\qed$


\begin{lema}
  Let $\textsf{concretize}\colon{} \sym \rightarrow \dom$ be a
  function.  Let $\pi$ and $\textsf{concretize}(\pi)$ be two
  executions in the searching space of $\mcalgo^{\Delta}(\model,
  \cotriplenoloc{}, n)$ and the state space graph $G$ of $C$ with $n$
  processes, respectively.  The execution $\pi$ is feasible.  Let
  $\lambda$ be an absence assertion, $\pi \vdash{} \lambda$ iff
  $\textsf{concretize}(\pi) \vdash \lambda$.
  \label{lema:mc:prop:preserve}
\end{lema}

\noindent\textbf{Proof.}
The interpretation of an absence assertion is about the order of some
specific transitions representing the three kinds of events.  We show
that the order of these specific transitions in $\pi$ is preserved by
$\textsf{concretize}(\pi)$.  let $g$ be a procedure called inside $C$.
For a transition $t\in\mypathtrans(\pi)$,

\begin{itemize}
\item if $t$ is labeled by $\myactsend{$v$}{$p$}$,
  $\textsf{concretize}(t)$ is labeled by \\
  $\myactsend{\textsf{concretize}$(v)$}{\textsf{concretize}$(p)$}$;

\item if $t$ is $\myenter^{\textsf{body}(g)}_{p, \pi}$ (resp.\
  $\myexit^{\textsf{body}(g)}_{p, \pi}$), obviously $\textsf{concretize}(t)$ is
  $\myenter^{\textsf{body}(g)}_{p, \textsf{concretize}(\pi)}$ (resp.\
  $\myexit^{\textsf{body}(g)}_{p, \textsf{concretize}(\pi)}$).
\end{itemize}
Therefore, the order of the specific transitions in $\pi$ is preserved
by $\textsf{concretize}(\pi)$.  $\qed$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Soundness of The Composite And Modular Algorithm
} \label{sec:minimp:modular:proof} The soundness of the algorithm
$\mcalgo^{\Delta}$ can be expressed by the following theorem:

\begin{teom}
  $\model \models \cotriplenoloc{}$, iff for any number $n$ of
  processes, we have
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cotriplenoloc{}}, n)
  = \textbf{T}$.
\end{teom}

\noindent{}\textbf{Proof} Let  $\{C_0, C_1, ...\ , C_{m-1}\}$ be the set of
call statements.  For each $C_i$, $0 \leq{} i < m$, the procedure
$f_i$ of $C_i$ is specified by
$\mycosubtriple{i}{\psi_i}{\phi_i}{\textsf{body}(f_i)}$
$\in \textsf{Tri}$.

Let $\{S_0, S_1, ...\}$ be the set of statement sequences such that no
triple in $\textsf{Tri}$ specifies $S_j$ or a sub-statement sequence
of $S_j$, $j \geq 0$.  Note $S_j$ can be nothing (i.e., $\epsilon$).
Since collective style procedures must be called collectively, we have
\[
C = S_0C_0S_1C_1S_2\ldots{}S_{m-1}C_{m-1}S_{m}
\]
or
\[
  \cocond{\psi} \overrightarrow{C} \subseteq{}
  \overrightarrow{S_0C_0S_1C_1S_2\ldots{}S_{m-1}C_{m-1}S_{m}}.
\]
For either case, we have $\model \models \cotriplenoloc{}$ iff for any
number $n$ of processes,
\[
  \mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{ \cocond{\psi,
      \Gamma}~S_0C_0\ldots{}S_{m-1}C_{m-1}S_m~\cocond{\phi,
      \Upsilon}}, n) = \textbf{T}.
\]
Then, this theorem is a consequence of the repeated applications of
Lemma \ref{lema:modular:2} and \ref{lema:modular:3}.  $\qed$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%  THEOREM-LEMMA-1 %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{lema}
  Assuming that $\cosubtriple{1} \in \textsf{Tri}$, for some statement
  sequence $C_0$,
  we have
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
      \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}, n) = \textbf{T}$ iff
  
  \begin{enumerate}
  %\item $\model \models \cosubtriple{1}$ and
  \item exists a contract of $C_0$ s.t.\
    $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cosubtriple{0}}, n) =
    \textbf{T}$, and
      
  \item all four side conditions of the sequence rule
    \[
      \frac{\cosubtriple{0},\, \cosubtriple{1}}{\cocond{\psi,
          \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}
    \] hold.
  \end{enumerate}
  \label{lema:modular:2}
\end{lema}

\noindent{}\textbf{Proof} We first show that
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
      \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}, n) = \textbf{T}$ implies
Condition 1 and 2.

We construct the contract of $C_0$ as the follow:

\begin{itemize}
\item $\psi_0 = \psi$ and $\phi_0 = \psi_1$,
  
\item $\Gamma_0$ is the maximum subset of $\Gamma$ s.t.\
  $\Upsilon_1~\ruleguarantee{_\pi}~\Gamma_0$ for every feasible
  execution $\pi$ searched by
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
      \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}, n)$,

\item $\Upsilon_0 = \textsf{noSend}(\Upsilon)$.
\end{itemize}

Such a contract of $C_0$ makes all the side conditions of the sequence
rule for $C_0C_1$ be satisfied, hence Condition 2 is proved.

We prove Condition 1 by first showing that
$\mcalgo^{\Delta}(\model,
\frac{\mymath{Tri}}{\mycosubtriple{0}{\psi}{\psi_1}{C_0}}, n)$
searches in a sub-graph $G'$ of the graph $G$ searched by
$\mcalgo^{\Delta}(\model, \frac{\mymath{Tri}}{\cocond{\psi,
    \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}, n)$.

The $G$ and $G'$ share the same initial state, which is a pre-states
of $C_0$ where $\psi$ and $\myallemptyguard$ hold for all processes.
Obviously $\transT_{\textsf{Tri}}(C_0, l)$ is a subset of
$\transT_{\textsf{Tri}}(C_0C_1, l)$.  Then, for any state in $G'$ that
is reachable from the initial state over
$\transT_{\textsf{Tri}}(C_0, l)$, it must also be in $G$.  Therefore,
$G'$ is a sub-graph of $G$.  As a consequence, for an execution $\pi'$
in $G'$, there must be an execution $\pi$ in $G$ such that $\pi'$ is a
prefix of $\pi$.

Now we show that $\pi'$ is error-free with the fact that $\pi$ is
error-free by elaborating the kinds of violations checked by
$\mcalgo^\Delta$.

\begin{itemize}
\item[\textbf{DL}] Since $\pi'$ is a prefix of $\pi$ and $\pi$ is free of
  \textbf{deadlock},  $\pi'$ is free of \textbf{deadlock} as well.
  
\item[\textbf{SGV}] $\mydest(\mytail(\pi'))$ is also the pre-state of
  $C_1$ in $\pi$.  Since $\pi$ is error free, $\psi_1$ and
  $\myallemptyguard$ hold for all processes on
  $\mydest(\mytail(\pi'))$.  Therefore, there is no \textbf{SGV} on
  $\pi'$.

\item[\textbf{ITF}] Assuming that there is a state
  $\omega' \in \mypathstates(\pi')$ s.t.\ for some processes
  $p, q \in \nprocs{n}$,
  \begin{align}
    &\mayInterfere_{G'}(\omega', p, q) \text{ and } \nonumber\\
    &\forall{r\in\nprocs{n}}.
      \texttt{\acslgamma{$p$}{$q$}{$r$}} \not\in_{\pi'} \Gamma_0, \nonumber\\
    &\text{and } \omega' \text{ appears before } \myexit^{C_0}_{r, \pi'}
      \text{ on } \pi'. \nonumber
  \end{align}


  Since $\pi'$ is a prefix of $\pi$, $\omega'$ is also in $\pi$.  Note
  $C_1$ follows $C_0$, hence
  $\myenter^{C_1}_{p, \pi} \in \emana_G(\omega')$.  Consequently,
  $\mayInterfere^{\Delta}_\pi(\omega', p, q)$.  Then there must be
  \[    
    \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon_1.
  \]

  Otherwise, $\pi$ contains \textbf{ITF-II}.  This contradicts
  the assumption $\Upsilon_1~\ruleguarantee{_\pi}~\Gamma_0$.
 
\item[\textbf{PGV}] According to the construction of $\Upsilon_0$,
  there is only one kind of absence assertions that can be in
  $\Upsilon_0$.  Let
  \begin{center}
    $\upsilon = $ \texttt{\acslguarantee{$e_0$}{$e_1$}{$e_2$}}.
  \end{center}
  Note $\upsilon \in \Upsilon_0 \cap{} \Upsilon$.  Assuming
  $\pi' \vdash{} \neg\myaeval{\upsilon}_{C_0}(\mysrc(\myhead(\pi')),
  k)$, for some $k\in\nprocs{n}$.  Consequently,
  $\pi \vdash{} \neg\myaeval{\upsilon}_{C_0}(\mysrc(\myhead(\pi)),
  k)$, for the same process $k$. Note for the form of $\upsilon$,
  $\myaeval{~}_{C_0, \pi} = \myaeval{~}_{C_0C_1, \pi}$.  It
  contradicts the assumption that $\pi$ is error-free.

\item[\textbf{SRV}] Assume that there is a sub-statement sequence $C_2$
  of $C_0$ such that the state-requirement fails to hold on
  $\mycspre{\pi'}{C_2}$.  Since $\pi'$ is a prefix of $\pi$, the same
  violation happens at $\mycspre{\pi}{C_2}$ as well.  Contradicting the
  assumption that $\pi$ is error free.
\end{itemize}

Similar to the proof of the free of \textbf{SRV} in $\pi'$ above, the
free of \textbf{PRV}, \textbf{PRV-II}, \textbf{PRV-III} ,
\textbf{ITF-II} and \textbf{PGV-II} in $\pi'$ can be
proved with the same idea. Hence we skip the proof for these kinds of
violations.

Now we prove for the other direction, i.e., if Condition 1 and 2 are
satisfied, we have
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
    \Gamma}~C_0C_1~\cocond{\phi, \Upsilon}}, n) = \textbf{T}$.  We
show that a feasible execution $\pi$ in $G$ is error free via
elaborating all kinds of violations.

Since all side conditions of the sequence rule application are
satisfied, $C_0$ cannot be interfered by $C_1$.  Recall Lemma
\ref{lema:gen:non-interfere-sufficient}, for $\pi$, there is an
extended execution $\zeta$ of $C_0$ in $G$ such that
$\zeta = \pi' \circ{} \xi_1$, where $\pi'$ is in $G'$ and $\xi_1$ is a
path emanating from a pre-state of $C_1$.  In addition, by Condition
1, $\pi'$ is error free.

  \begin{itemize}
  \item[\textbf{DL}] Since $C_1$ is specified by a triple in
    $\textsf{Tri}$, $C_1$ is translated to a $\myactrefresh{}$
    statement.  Thus $C_0C_1 = C_0\myactrefresh{;}$.  Since
    $\myactrefresh{}$ 
    is independent with any communication statement,  it cannot
    introduce new deadlock.

  \item[\textbf{SGV}] The final state of $\pi$ is a post-state of
    $C_1$, which is equivalent to $\mycspost{\pi}{C_1}$.  Recall that
    if $\phi$ or $\myallemptyguard{}$ fail to hold on
    $\mycspost{\pi}{C_1}$, $\pi$ is infeasible.  It contradicts the
    assumption that $\pi$ is feasible.

  \item[\textbf{ITF}] Assuming that there is a state
    $\omega \in \mypathstates(\pi)$ s.t.\ for some
    $p, q\in\nprocs{n}$,
    \begin{align}
      &  \mayInterfere_G(\omega, p, q), \text{ and} \nonumber \\
      &  \neg\exists{r \in\nprocs{n}}.\,
        \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma \nonumber \\
      &  \text{and } \omega \text{ appears before } \myexit^{C_1}_{r, \pi}
        \text{ on }\pi. \nonumber
    \end{align}        
    Transition swapping cannot falsify $\mayInterfere_G$, and $C_1$ is
    translated to $\myactrefresh{}$, so there must be a state
    $\omega' \in \mypathstates(\pi')$ s.t.\
    $\mayInterfere_{G'}(\omega', p, q)$.  And we know $G'$ is error
    free, there must be
    \begin{align}
      & \gamma_0 = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\pi'} \Gamma_0 \nonumber \\
      &\text{and } \omega' \text{ appears before } \myexit^{C_0}_{r, \pi'}
        \text{ on }\pi'. \tag{a} \label{mc:delta:one:proof:a}
    \end{align}
    By our construction of the contract of $C_0$, $\gamma_0\in \Gamma$
    as well.  For the transition $t \in \emana_G(\omega)$ s.t.\
    $\myproc(t) = q$ and $\myact(t) = \myactrecv{$v$}{$p$}$, the order
    of $\myexit^{C_0}_r$ and $t$ is preserved from $\pi$ to $\zeta$.
    Thus such $\myexit^{C_0}_{r,\pi'}$ can only appear before
    $\omega'$ on $\pi'$.  Contradicting Condition
    \ref{mc:delta:one:proof:a}.

    
  \item[\textbf{PGV}]
    There are two cases depending on the form of  $\upsilon \in
    \Upsilon$. 
    
    \textbf{1.} For some processes $p, q, r \in \nprocs{n}$,
    \[
    \upsilon = \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon,
    \]
    assuming $\upsilon$ is violated on $\pi$.  It means that
    \[
       t \text{ appears before } \myenter^{C_0}_{r, \pi} \text{ on } \pi,
    \]
    where $\myact(t) = \myactsend{$v$}{$q$}$ and $\myproc(t) = p$.
    Both the transitions $t$ and $\myenter^{C_0}_{r, \pi}$ can only
    appear before $\myexit^{C_0}_{p, \pi}$ and
    $\myexit^{C_0}_{r, \pi}$, respectively.  Hence their order is
    preserved from $\pi$ to $\pi'$.  In addition, by our construction
    of $\Upsilon_0$ that $\Upsilon_0 = \nosendsubset(\Upsilon)$, we
    have that $\pi'$ fails to satisfy $\Upsilon$ since $\pi$ and
    $\pi'$ share the initial state, where $\Upsilon$ evaluates.
    Contradicting the assumption that $G'$ is error free.
    
  \textbf{2.} For
    \[
      \upsilon = \texttt{\acslwaitsfor{$p$}{$q$}} \in_\pi \Upsilon,
    \]
    assuming $\pi$ violates $\upsilon$.  By Side Condition 4 of the
    sequence rule,
    $\Upsilon \subseteq{_\pi} \Upsilon_0{} \cup{} \Upsilon_1{}$.
    Besides, $\Upsilon_0 = \nosendsubset(\Upsilon)$, by our
    construction for $\Upsilon_0$.  We have
    $\upsilon \in_\pi \Upsilon_1$.
    Since $\pi$ is feasible,
    \[
    \forall{k\in\nprocs{n}}. \pi \vdash{}
    \myaeval{\textup{$\Upsilon$}}_{C_1}(\mycspre{\pi}{C_1},
    k).
  \]
  It means that $p$ cannot exit $C_0C_1$ before $q$ entering $C_1$.
  It contradicts the assumption that $\pi$ violates $v$, which implies
  that $p$ exits $C_0C_1$ even before $q$ entering $C_0$.
    
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[\textbf{SRV}] Assuming that there is a sub-statement $C_2$ of
  $C_0C_1$ s.t.\
    \[
    \cosubtriple{2} \in \textsf{Tri} \text{ and }
    \psi_2 \text{ fails to hold on } \mycspre{\pi}{C_2}.
    \]
    There are two cases.
    
  \begin{itemize}
  \item[1.] If $C_2$ is a sub-statement of $C_0$, $\pi'$
    inevitably contains \textbf{SRV} as well.  It contradicts that
    assumption that $G'$ is error free.
    
  \item[2.] Otherwise, $C_2 = C_1$.  Then $\psi_2 = \psi_1 = \phi_0$.
    Since $\mydest(\mytail(\pi')) = \mycspre{\pi}{C_2}$, $\pi'$
    contains \textbf{SGV}.  It contradicts the assumption that $G'$ is
    error free.
  \end{itemize}
  

\item[\textbf{PRV}] Assuming that there is a sub-statement $C_2$ of
  $C_0C_1$ s.t.\ $\cosubtriple{2}$ $\in \textsf{Tri}$.  Let
  $p, q, r \in \nprocs{n}$.   Suppose 
  \begin{align}
    &
      \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_2, \nonumber \\
    &\text{and } \myexit^{C_2}_{p, \pi} \text{ appears before } t
   \text{ and } t \text{ appears before } \myexit^{C_2}_{r, \pi}
      \text{ on } \pi, \nonumber
  \end{align}
  where $\myact(t) = \myactsend{$v$}{$q$}$ and $\myproc(t) = p$.
  Then there are two cases.
  
  \begin{itemize}
  \item[1.] If $C_2$ is a sub-statement of $C_0$, $\pi'$ must
    also contain \textbf{PRV}. 
    
  \item[2.] Otherwise, $C_2 = C_1$.  But no transition labeled by a
    send action can appear after $\myenter^{C_1}_{p, \pi}$ on $\pi$,
    since the definition of $C_1$ has been abstracted away.
  \end{itemize}
  Both cases arrive at a contradiction to the assumption.

\item[\textbf{PRV-II}] Assuming that there is a sub-statement
  $C_2$ of $C_0C_1$ s.t.\ $\cosubtriple{2}$ $\in \textsf{Tri}$.  Let
  $p, q, r, r' \in \nprocs{n}$.    Suppose 
  \begin{align}
    & \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_2
      \nonumber \\
    & \text{and } \myexit^{C_1}_{p, \pi} \text{ appears before }
      \myexit^{C_2}_{k, \pi} \text{ and } \myexit^{C_2}_{k, \pi}
      \text{ appears before } \myexit^{C_1}_{r, \pi} \text{ on } \pi.
      \nonumber
  \end{align}
  But there is no such $r' \in \nprocs{n}$ that
  \begin{align}
    & 
      \texttt{\acslgamma{$p$}{$q$}{$r'$}} \in_\pi \Gamma\nonumber \\
    & \text{and } \myexit^{C_2}_{k, \pi} \text{ appears before }
      \myexit^{C_1}_{r', \pi} \text{ on }\pi. \nonumber
  \end{align}
  There are two cases.
  
  \begin{itemize}
  \item[1.]  $C_2$ is a sub-statement of $C_0$.  Obviously,
    the same violation can happen in $\pi'$ if $\Gamma_0$ is not
    stronger than $\Gamma$.  By our construction,
    $\Gamma_0 \subseteq_\pi \Gamma$, which implies
    $\Gamma_0 \subseteq_{\pi'} \Gamma$ since $\pi$ and $\pi'$ share
    the initial state.
    Thus $\pi'$ contains
    \textbf{PRV-II}.  It contradicts the assumption that $G'$ is error
    free.

  \item[2.]  Otherwise, $C_2 = C_1$. But by Side Condition 5 of
    the sequence rule, $\Gamma_1 \subseteq{_\pi} \Gamma$. Our assumption
    itself becomes invalid.
  \end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[\textbf{PRV-III}] Assuming that there are sub-statements
  $C_2$ and $C_3$ of $C_0C_1$ s.t.

  \begin{itemize}
  \item $C_2$ lexically precedes $C_3$
  \item $\cosubtriple{2}, \cosubtriple{3} \in \textsf{Tri}$, and
  \item $\Gamma_2$ may be violated due to the weakness of $\Upsilon_3$
    $\pi$.
\end{itemize}
There are two cases.

 \begin{itemize}
 \item[1.] Both $C_2$ and $C_3$ are sub-statements of $C_0$.  Then
   similar to the proofs above, the assumption will result in a
   contradiction that $\pi'$ contains \textbf{PRV-III}.

 \item[2.] Otherwise, $C_2$ is a sub-statement of $C_0$ and
   $C_3 = C_1$.  Then, by our construction,
   $\Upsilon_3(\Upsilon_1)~\ruleguarantee_\pi~\Gamma_0$, it goes back
   to the case that we had proved for free of \textbf{PRV-II}.
 \end{itemize}

\item[\textbf{ITF-II}] Assuming that there is a sub-statement $C_2$ of
  $C_0C_1$ s.t.\ $\cosubtriple{2} \in \textsf{Tri}$.  Now suppose that
  there is $\omega \in \mypathstates(\pi)$ s.t.\ for
  $p, q\in\nprocs{n}$, $\mayInterfere^{\Delta}_{\pi}(\omega, p, q)$,
  and $\Upsilon_2$ is not strong enough to prevent $C_2$ from sending
  a message from $p$ to $q$ that can be received by a transition
  emanating from $\omega$ in an actual execution of $C_0C_1$.

  There are two cases.
  
  \begin{itemize}
  \item[1.] $C_2$ is a sub-statement of $C_0$.  With a
    similar idea to the proofs of previous cases, we can eventually
    arrive at a contradiction that $\pi'$ contains
    \textbf{ITF-II}.

  \item[2.] $C_2 = C_1$.  Then, by $\Upsilon_2 (\Upsilon_1)$
    $\ruleguarantee_\pi$ $\Gamma_0$, it goes back to the case that we have
    proved for the free of \textbf{ITF}.
  \end{itemize}

\item[\textbf{PGV-II}] Assuming there is a sub-statement
  $C_2$ of $C_0C_1$ s.t.\ 
  $\cosubtriple{2} \in \textsf{Tri}$.  Suppose $\Upsilon_2$ is not
  strong enough to guarantee that an actual definition $C_2$ will not
  violate $\nosendsubset(\Upsilon)$.

There are two cases.

  \begin{itemize}
  \item[1.]  $C_2$ is a sub-statement of $C_0$.  Since
    $\Upsilon_0 = \nosendsubset(\Upsilon)$, we can derive a
    contradiction that $\pi'$ contains \textbf{PGV-II} too
    with a similar idea to the proofs of previous cases above.
    
  \item[2.]  Otherwise, $C_2 = C_1$.  By Side Condition 3 of the
    sequence rule that\\
    $\myruleinfer{\Upsilon_0}{\Upsilon_2(\Upsilon_1)}{\Upsilon}{\pi}$, the
    assumption itself is invalid.
  \end{itemize}
\end{itemize}
$\qed{}$
\param{}
%%%%%%%%%%%%%%%% END OF PROOF 1 %%%%%%%%%%%%%%

\begin{lema}
  Given a statement sequence $C_0C_1C_2$ and a triple set
  $\textsf{Tri}$, suppose that $\cosubtriple{1} \in \textsf{Tri}$ and
  there is no triple for any sub-statement of $C_2$ in $\textsf{Tri}$.
  Then, we have
  \begin{center}
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
        \Gamma}~C_0C_1C_2~\cocond{\phi, \Upsilon}}, n) = \textbf{T}$ iff
    there exists $\mu$, $\Gamma_0, \Upsilon_0, \Gamma_2$ and $\Upsilon_2$
    such that
  \begin{enumerate}
  \item $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{
        \cocond{\psi, \Gamma_0}~C_0C_1~\cocond{\mu, \Upsilon_0} 
      }, n) = \textbf{T}$,

  \item
    $\mcalgo(\model, \cocond{\mu, \Gamma_2}~C_2~\cocond{\phi,
    \Upsilon_2}, n) = \textbf{T}$, and

  \item all the side conditions of the sequence rule $\frac{\cocond{\psi,
        \Gamma_0}~C_0C_1~\cocond{\mu, \Upsilon_0}
      ,\, \cocond{\mu, \Gamma_2}~C_2~\cocond{\phi, \Upsilon_2}}{\cocond{\psi,
        \Gamma}~C_0C_1C_2~\cocond{\phi,
        \Upsilon}}$ are satisfied.
  \end{enumerate}
  \end{center}
      \label{lema:modular:3} 
\end{lema}

%%%%%%%%%%%%%%%%% START PROOF 2 %%%%%%%%%%%%%%%%%%
\noindent{}\textbf{Proof.}
Let $G$ be the state space graph searched by
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
    \Gamma}~C_0C_1C_2~\cocond{\phi, \Upsilon}},
n)$, $G'$ be the state space graph searched by
$\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
    \Gamma_0}~C_0C_1~\cocond{\mu, \Upsilon_0} }, n)$ and
$G''$ be the state space graph searched by
$\mcalgo(\model, \cocond{\mu, \Gamma_2}~C_2~\cocond{\phi,
  \Upsilon_2}, n)$.
Similar to what the proof of Lemma \ref{lema:modular:2} has showed,
for every execution $\pi'$ in $G'$, there is an execution $\pi$ in $G$
s.t.\ $\pi'$ is a prefix of $\pi$.

We first prove that $\mcalgo^{\Delta}(\model,
\frac{\textsf{Tri}}{\cocond{\psi, \Gamma}~C_0C_1C_2~\cocond{\phi,
    \Upsilon}}, n) = \textbf{T}$ implies Condition 1, 2 and 3.  We
construct $\mu$, $\Gamma_0$, $\Upsilon_0$, $\Gamma_2$ and $\Upsilon_2$
as the follows

\begin{itemize}
\item let $\mu$ be the strongest condition s.t.\ for any post-state
  $\omega'$ of $C_0C_1$, $\mu$ holds on $\omega'$ iff
  $\omega'$ is in $G'$.
  
\item let $\Gamma_0$ be the minimal set s.t.\
  for any subset $\Gamma_0' \subset \Gamma_0$, \\
  $\mcalgo{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
        \Gamma_0'}~C_0C_1~\cocond{\mu, \Upsilon_0}}, n)
    \not= \textbf{T}$;
  
\item let $\Upsilon_0$ be the maximal set s.t.\
  for any super set $\Upsilon_0' \supset \Upsilon_0$, \\
  $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
        \Gamma_0}~C_0C_1~\cocond{\delta, \Upsilon_0'}}, n)
    \not= \textbf{T}$;
  
\item let $\Gamma_2$ be the minimal set such that for any
  $\Gamma_2' \subset \Gamma_2$, \\
  $\mcalgo(\model, \cocond{\mu, \Gamma_2'}~C_2~\cocond{\phi,
    \Upsilon_2}, n) \not= \textbf{T}$;
  
\item let $\Upsilon_2$ be the maximal set such that for any super set
  $\Upsilon_2' \supset \Upsilon_2$,\\
  $\mcalgo(\model, \cocond{\mu, \Gamma_2}~C_2~\cocond{\phi,
    \Upsilon_2'}, n) \not= \textbf{T}$.
\end{itemize}

We show the validity of Condition 1 by showing that an execution
$\pi'$ in $G'$, which is a prefix of some execution $\pi$ in $G$, is
error free.  Note that $\pi'$ is naturally free of \textbf{SGV} due to
the construction of $\mu$.  Similarly, it is free of \textbf{ITF},
\textbf{PGV}, \textbf{PRV-II} or \textbf{PGV-II} due to the
construction of $\Gamma_0$ and $\Upsilon_0$.
  
\begin{itemize}
  \item[\textbf{DL}] If $\pi'$ results in a deadlock, $\pi$
    results in a deadlock too.  It contradicts the assumption that
    $\pi$ is error free.
        
  \item[\textbf{SRV}] Assuming that there is a sub-statement $C_3$ of
    $C_0C_1$ s.t.\ exists $\cosubtriple{3}$ is in $\textsf{Tri}$.
    Suppose $\pi'$ contains \textbf{SRV} for $\psi_3$, i.e., $\psi_3$
    fails to hold on $\mycspre{\pi'}{C_3}$.  Since $\pi'$ is a prefix
    of $\pi$, $\pi$ must also contain \textbf{SRV} for $\psi_3$.  It
    contradicts the assumption that $\pi$ is error free.
    
  \end{itemize}  
  The proof of that $\pi'$ is free of
  \textbf{PRV},
  \textbf{PRV-III} or
  \textbf{ITF-II} can be constructed with the same idea
  that if $\pi'$ contains such error, so does $\pi$, which results in
  a contradiction.  Detailed proof for them is omitted for brevity.


  Next we show that Condition 2 is valid.  A pre-state $\omega''$ of
  $C_2$, where $\mu$ and $\myallemptyguard$ hold, it is equivalent to
  a post-state $\omega'$ of $C_0C_1$.  By the construction of $\mu$,
  $\omega'$ must be in $G'$.  Now let $\pi'$ be an execution in $G'$
  that ends with $\omega'$.  If letting all processes continue to
  execute $C_2$ from $\omega'$, it will results in an execution $\pi'
  \circ{} \pi''$ in $G$.  Since $\pi' \circ{} \pi''$ is in $G$, if it
  ends with a post-state of $C_2$, $\phi$ and $\myallemptyguard$ must
  hold on that post-state.  In addition, since obviously $\pi''$ is an
  execution in $G''$, $\pi''$ cannot contain any violation against
  $\Gamma_2$ and $\Upsilon_2$ according to their construction.
  Therefore, a generic execution $\pi''$ in $G''$ must be free of
  violation with respect to the given contract.

 %%%%%%%%%%%%%%% COND 3 %%%%%%%%%%%%%%% 
  
  Now we prove Condition 3 by induction on all the side conditions of
  the sequence rule.
  
  \begin{enumerate}
    %%%%%%%%%%%% SIDE COND 1 %%%%%%%%%%%%%%%%%
  \item We prove Side Condition 1 by contradiction.  Since $\Gamma_0$
    is minimal for $G'$, if we remove $\gamma_0 \in \Gamma_0$ from
    $\Gamma_0$, there is at least an execution $\pi'$ in $G'$ that
    contains either \textbf{ITF} or \textbf{PRV-II}.  Let $\pi$ be a
    feasible execution in $G$.  Assuming that
    $\Upsilon_2~\ruleguarantee_{\pi}~\{\gamma_0\}$ is not satisfied.
    For $p, q, r\in \nprocs{n}$, $\gamma_0$ partially evaluates to
    \[
      \texttt{\acslgamma{$p$}{$q$}{$r$}},
    \]
    on $\pi$ while
    \[
    \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \not\in_{\pi} \Upsilon_2,
    \]
    where $r' = r$ or $r' = q$.

    Since $\Upsilon_2$ is maximal, there
    is at least one execution $\pi''$ in $G''$ s.t.\ a global
    transition $t$ appears before $\myenter^{C_2}_{r', \pi''}$, and
    $\myproc(t) = p \wedge{} \myact(t) = \myactsend{$v$}{$q$}$ for
    some expression $v$.  It means that there is a path for $p$
    starting from the entry of $C_2$ that ends with such $t$ and is
    independent with process $r'$.

    \begin{itemize}
    \item If $\pi'$ contains \textbf{ITF} without $\gamma_0$, there
      must be a state $\omega' \in \mypathstates(\pi')$
      s.t.\ $\mayInterfere_{G'}(\omega', p, q)$, and $\omega'$ appears
      before $\myexit^{C_0C_1}_{r, \pi'}$ on $\pi'$.  Since process
      $p$ can continue to execute and send a message to $q$ without
      process $r'$ ever executing, $C_2$ can actually interfere
      $C_0C_1$.  Let $\pi$ be an execution in $G$ where the
      interference happens.  Consequently, process $q$ receives more
      messages from some other process $k$ than $p$ before
      $\myexit^{C_0C_1}_{q, \pi}$ than the number of messages sent by
      $k$ to $q$ before $\myexit^{C_0C_1}_{k, \pi}$ on $\pi$.  It
      causes the message channel from $k$ to $q$ be not empty at
      $\mycspre{\pi}{C_1}$.  That is $\pi$ contains
      \textbf{SRV}. Contradicting the assumption that $G$ is error
      free.


  \item 
    If $\pi'$ contains \textbf{PRV-II} without $\gamma_0$, there must
    be a sub-statement  $C_3$ of $C_0C_1$
    s.t.\ 
    
    \begin{enumerate}
    \item $\cosubtriple{3} \in \textsf{Tri}$ and
      \[
      \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\pi'} \Gamma_3,
      \] 

    \item $\myenter^{C_3}_{r, \pi'}$ appears before
      $\myexit^{C_0C_1}_{p, \pi'}$ on $\pi'$, and
      
    \item $\myexit^{C_0C_1}_{p,
      \pi'}$ appears before $\myexit^{C_3}_{r, \pi'}$ on $\pi'$.
    \end{enumerate}
    Similarly, starting from $\mydest(\myexit^{C_0C_1}_{p, \pi'})$,
    process $p$ can continue to execute and send a message to $q$
    without process $r'$ ever executing.  Let $\rho$ be such a
    feasible path in $G$.  Obviously, $\rho$ contains \textbf{PRV}.
    Contradicting the assumption that $G$ is error free.
    
  \end{itemize}

    %%%%%%%%%%%% SIDE COND 2 %%%%%%%%%%%%%%%%%    
  \item We prove Side Condition 2 by contradiction. Let $\upsilon \in
    \nosendsubset(\Upsilon)$. Let $\pi$ be an execution in $G$. Let
    $p, q, r, x \in \nprocs{n}$. On the proper state in $\pi$,
    $\upsilon$ is partially evaluated to
    \[
    \texttt{\acslguarantee{$p$}{$q$}{$r$}}.
    \]
    Suppose that $\myruleinfer{\Upsilon_0}{\Upsilon_2}{\{\upsilon\}}{\pi}$ is not satisfied,
    we have 
    \begin{itemize}
    \item[(1)]$
      \texttt{\acslguarantee{$p$}{$q$}{$r$}} \not\in_\pi \Upsilon_0,
      $
     and
    \item[(2)]  $\texttt{\acslwaitsfor{$x$}{$r'$}} \not\in_\pi
      \Upsilon_0$ or\\
      $
        \texttt{\acslguarantee{$p$}{$q$}{$x$}} \not\in_\pi \Upsilon_2
        $
        where\\
        $r' = r$ $\vee r' = q$, respectively.

    \end{itemize}
    For Case 1, since $\Upsilon_0$ is maximal, we have an execution
    $\pi'$ in $G'$ that violates $\upsilon$.  Since $\pi'$ is a prefix
    of an execution $\pi$ in $G$ and $\upsilon \in \Upsilon$, $\pi$
    violates $\Upsilon$.  Contradicting the assumption that $G$ is
    error free.

    For Case 2, since $\Upsilon_0$ is maximal, there must be an
    execution $\pi'$ in $G'$ s.t.\ $\myexit^{C_0C_1}_{x, \pi'}$
    appears before $\myenter^{C_0C_1}_{r', \pi'}$ on $\pi'$.  Since
    $\Upsilon_2$ is maximal, we know that process $p$ can send a
    message to $q$ without any dependence on $r'$ in $C_2$.
    Therefore, we can let process $p$ continue to execute and send a
    message to $q$ from the state $\mydest(\myexit^{C_0C_1}_{x,
      \pi'})$ without $r'$ executing.  Let $\rho$ be such a new
    feasible path in $G$. Obviously, $\rho$ violates $\upsilon$.
    Contradicting the assumption that $G$ is error free.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      %%%%%%%%%%%% SIDE COND 3 %%%%%%%%%%%%%%%%%
      
  \item By Side Condition 2, we know $\nosendsubset(\Upsilon)
    \subseteq{} \Upsilon_0$.  So we only need to prove by
    contradiction towards absence assertions in such form
    \[
     \texttt{\acslwaitsfor{$e_0$}{$e_1$}}.
    \]
    Let $p, q \in \nprocs{n}$.  Suppose that there is an execution
    $\pi = \pi' \circ{} \pi''$ in $G$ s.t.\ $\pi'$ is in $G'$ and
    $\pi''$ is in $G''$.  Assuming that 
    \[
      \upsilon = \texttt{\acslwaitsfor{$p$}{$q$}} \in_\pi \Upsilon, 
    \]
    but $\upsilon \not\in_\pi \Upsilon_0 \cup \Upsilon_2$.

    Since both $\Upsilon_0$ and $\Upsilon_2$ are maximal, (1) we have
    $\myexit^{C_0C_1}_{p, \pi'}$ appears before $\myenter^{C_0C_1}_{q,
      \pi'}$ on $\pi'$; and (2) process $p$ can exit $C_2$ without any
    dependence on process $q$.  If letting process $p$ continue to
    execute from the state $\mydest(\myexit^{C_0C_1}_{p,\pi'})$ until
    it exits $C_2$ without $q$ executing, it forms a feasible path
    $\rho$ in $G$.  Obviously, $\rho$ violates $\upsilon$.  We arrive
    at a contradiction.

    %%%%%%%%%%%%%%% SIDE COND 4 %%%%%%%%%%%%%%%%%%
  \item We now prove that Side Condition 4 is satisfied.  Let $p, q, r
    \in \nprocs{n}$.  There are two cases.

    \begin{enumerate}
    \item[4.1] Let $\pi' \circ{} \pi''$ be an execution in $G$, where
      $\pi'$ is an execution in $G'$ and $\pi''$ is an execution in
      $G''$.  We show that if there is an element
      $\gamma \in_{\pi'\circ{}\pi''} \Gamma_0$, and
      $\neg(\Upsilon_2~\rulecancels_{\pi'\circ{}\pi''}~\gamma)$, , we
      have have $\gamma \in_{\pi'\circ{}\pi''} \Gamma$.


      Let $\gamma$ be partially
      evaluated on $\pi'$, to
      \[
      \texttt{\acslgamma{$p$}{$q$}{$r$}}.
      \]
      Since $\Gamma_0$ is minimal, without loss of generality, we
      assume that there is a state $\omega' \in \mypathstates(\pi')$
      s.t.\ $\mayInterfere_{G'}(\omega', p, q)$ and $\omega'$ appears
      before $\myexit^{C_0C_1}_{r, \pi'}$ on $\pi'$.  In addition, we
      know that $\neg(\Upsilon_2~\rulecancels_{\pi'\circ{}\pi''}~\gamma)$, so
      \[
      \texttt{\acslwaitsfor{$p$}{$r'$}} \not\in_{\pi''} \Upsilon_2,
      \]
    where $r' = r~\vee~r' = q$.  Since $\Upsilon_2$ is maximal, we
    know that process $p$ can exit $C_2$ without any dependency on
    process $r'$.  Hence, similar to the proofs for previous cases, we
    can conclude a path $\rho$ in $G$ that forks from $\omega'$ by
    letting process $p$ continue to execute until exiting $C_2$
    without $r'$ executing.  Consequently, $\gamma \in \Gamma$,
    otherwise $\rho$ contains \textbf{ITF}.
    
    

  \item[4.2] Let $\gamma \in \Gamma_2$ and $\pi' \circ{} \pi''$ be an
    execution in $G$, where $\pi'$ is an execution in $G'$ and $\pi''$
    is an execution in $G''$.  Since $\Gamma_2$ is minimal, without
    loss of generality, $\pi''$ can be assumed to contain \textbf{ITF}
    if $\gamma$ is removed from $\Gamma_2$.  Then, obviously, if there
    is no element in $\Gamma$ that is partially evaluated at the
    proper state on $\pi' \circ{} \pi''$ to the same assertion, $\pi'
    \circ{} \pi''$ contains \textbf{ITF} as well.  It will lead to a
    contradiction.
  \end{enumerate}
\end{enumerate}

%%%%%%%%%%% OTHER DIRECTION %%%%%%%%%%%%%%%%%%%%
Now we prove for the other direction, i.e., Condition 1, 2 and 3 imply
\\ $\mcalgo^{\Delta}(\model, \frac{\textsf{Tri}}{\cocond{\psi,
    \Gamma}~C_0C_1C_2~\cocond{\phi, \Upsilon}},
n) = \textbf{T}$.  We prove a feasible execution $\pi$ in $G$ is error
free by induction on the cases of violations.

Note that $C_0C_1$ cannot be interfered by $C_1$.  So we can always
apply Lemma \ref{lema:gen:non-interfere-sufficient} and
\ref{lema:seq:reproduce} to executions in $G$.


\begin{enumerate}
\item[\textbf{DL}] Assuming that $\pi$ ends with a state where a
  \textbf{DL} happens.  According to Lemma
  \ref{lema:gen:non-interfere-sufficient}, there is another feasible
  execution $\rho' \circ{} \rho''$ in $G$, where $\rho'$ and $\rho''$
  are feasible paths in $G'$ and $G''$ respectively, shares the final
  state with $\pi$.  Since the final state is where deadlocked, it is
  either in $\pi'$ or $\pi''$.  In other words, either $G'$ or $G''$
  contains \textbf{DL}.  It contradicts the assumed Condition 1 and 2.
   
  
\item[\textbf{SGV}] By Lemma \ref{lema:gen:non-interfere-sufficient},
  there is a feasible execution $\pi' \circ{} \pi''$ in $G$ s.t.\ 1)
  it shares the initial and final state with $\pi$; and 2) $\pi'$ is a
  feasible execution in $G'$ and $\pi''$ is a feasible execution in
  $G''$.  Since $G'$ is error free, $\mu$ and $\myallemptyguard$ hold
  at $\mysrc(\myhead(\pi''))$.  And, $G''$ is error free, $\phi$ and
  $\myallemptyguard$ must hold at $\mydest(\mytail(\pi''))$.  Since
  the final state is shared by $\pi''$ and $\pi$, no \textbf{SGV} in
  $\pi$.

  
\item[\textbf{ITF}] For the execution $\pi$ in $G$, assuming that
  there is a state $\omega \in \mypathstates(\pi)$.  For
  $p, q \in \nprocs{n}$, we have $\mayInterfere_{G}(\omega, p, q)$ and
  \begin{align}
    \neg\exists{}&\texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma.\,
    \nonumber \\
    &\omega\text{ appears before }\myexit^{C_0C_1C_2}_{r,
      \pi}\text{ on } \pi\text{ for some }r \in \nprocs{n}. \nonumber
  \end{align}

  According to Lemma \ref{lema:gen:non-interfere-sufficient}, there is
  another feasible execution $\pi' \circ{} \pi''$ in $G$ sharing
  initial and final states with $\pi$ s.t.\ $\pi'$ is a feasible
  execution in $G'$ and $\pi''$ is a feasible execution in $G''$.
  Swapping transitions cannot falsify $\mayInterfere_G$, so
  there are two cases.

  \begin{enumerate}
  \item There is a state $\omega'$ in $\pi'$ s.t.\
    $\mayInterfere_{G'}(\omega', p, q)$.  By Side Condition 4 of
    the sequence rule,  there are two sub-cases.

    \begin{enumerate}
    \item
      $\texttt{\acslgamma{$p$}{$q$}{$r$}} \not\in_{\pi'} \Gamma_0$.
      It results in \textbf{ITF} on $\pi'$.  Contradicting the
      assumption that $G'$ is error free.

    \item Let $\gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}}$.
      We have $\gamma \not\in_{\pi'} \Gamma_0$ and
      $\Upsilon_2~\rulecancels_{\pi;}~\gamma$.  Since
      $\omega' \in \mypathstates(\pi')$, we can conclude that process
      $q$ and $r$ have not exited $C_0C_1$ at state $\omega$ on $\pi$.
      By Lemma \ref{lema:seq:reproduce}, there must be a feasible path
      $\rho$ in $G''$ that ends with $\myexit^{C_2}_{p, \rho}$ and
      contains no transition associated with $q$ or $r$.  Obviously,
      $\rho$ violates $\Upsilon_2$.  Contradicting the assumption that
      $G''$ is error free.
  \end{enumerate}
    
    
\item There is a state $\omega''$ in $\pi''$ s.t.\
  $\mayInterfere_{G''}(\omega'', p, q)$.  By Side Condition 4 of the
  sequence rule,  we have
  \[
    \texttt{\acslgamma{$p$}{$q$}{$r$}} \not\in_{\pi''} \Gamma_2
  \]
   So $\pi''$ contains \textbf{ITF} as well.
  Contradicting the assumption that $G''$ is error free.
  \end{enumerate}
  
  
\item[\textbf{PGV}] For any $\upsilon \in_\pi \Upsilon$, by Side
  Condition 3 of the sequence rule, we have
  $\upsilon_0 \in_\pi \Upsilon_0$ or $\upsilon_2 \in_\pi \Upsilon_2$.
  If $\pi$ violates $\upsilon$, by Lemma
  \ref{lema:gen:non-interfere-sufficient}, we will arrive at a
  contradiction by finding an alternative execution in $G'$ or $G''$
  that violates $\upsilon_0$ or $\upsilon_2$, respectively.  Detailed
  proof is omitted for brevity.
\end{enumerate}

Recall that $C_1$, as well as any sub-statement of $C_1$, is not
specified by a triple in $\textsf{Tri}$.   Therefore, 
for any collective state associated with $\pi$, there must be an
execution $\pi'$ in $G'$ s.t.\ an equivalent collective state is also
associated with $\pi'$.  Hence the free of
\textbf{SRV},
\textbf{PRV},
\textbf{PRV-III} or
\textbf{ITF-II} can all be proved with the idea that if
$\pi$ contains such an error, so does $\pi'$, which contradicts the
assumption that $G'$ is error free. I omit the proof for these cases.

\begin{enumerate}
  
\item[\textbf{PRV-II}] Let $C_3$ be a sub-statement of $C_0C_1$ s.t.\
  $\cosubtriple{3} \in \textsf{Tri}$.  Suppose for
  $p, q, r \in \nprocs{n}$,
  \begin{align}
    &\myexit^{C_0C_1C_2}_{p, \pi} \text{ appears before }
      \myexit^{C_3}_{r, \pi} \text{ on } \pi \text{ and} \nonumber \\
    & \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\pi} \Gamma_3 \text{
      and} \nonumber\\
    & \text{there is no } \gamma = \texttt{\acslgamma{$p$}{$q$}{$r'$}}
      \in_{\pi} \Gamma \nonumber \\
    & \text{ s.t.\ }\myexit^{C_3}_{r, \pi} \text{ appears before }
      \myexit^{C_0C_1C_2}_{r', \pi} \text{ on } \pi \nonumber
  \end{align}

  By Side Condition 4 of the sequence rule, we have
  $\gamma \not\in_{\pi} \Gamma_0$ or
  $\Upsilon_2~\rulecancels_{\pi}~\gamma$.
  
  For the former case, there must exist a feasible execution $\pi'$ in
  $G'$ s.t.\ $\myexit^{C_0C_1}_{p, \pi'}$ appears before
  $\myexit^{C_3}_{r, \pi'}$ on $\pi'$, by Lemma
  \ref{lema:gen:non-interfere-sufficient}.  Then $\pi'$ contains
  \textbf{PRV-II}. Contradicting the assumption that $G'$ is error
  free.

  For the latter case, there is
  \[
    \texttt{\acslwaitsfor{$p$}{$r'$}} \in_{\pi} \Upsilon_2,
  \]
  where $r' = r \vee{} r' = q$.  Again, by Lemma
  \ref{lema:gen:non-interfere-sufficient}, an execution $\pi''$ in
  $G''$ can be obtained via swapping transitions in $\pi$ s.t.\
  $\myexit^{C_2}_{p, \pi''}$ appears before
  $\myenter^{C_2}_{r', \pi''}$ on $\pi''$.  Obviously $\pi''$ violates
  $\Upsilon_2$.  Contradicting the assumption that $G''$ is error
  free.
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
\item[\textbf{PGV-II}] Let $C_3$ be a sub-statement of
  $C_0C_1$ s.t.\ $\cosubtriple{3} \in \textsf{Tri}$.  For $\pi$,
  suppose $\myenter^{C_3}_{p, \pi}$ appears before
  $\myenter^{C_0C_1C_2}_{r, \pi}$, where $p, r \in \nprocs{n}$.  In
  addition, assuming that
  \[
    \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_{\pi} \Upsilon
  \] but there is no
  \[
    \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_{\pi} \Upsilon_2
  \]
  s.t.\ $\myenter^{C_0C_1C_2}_{r, \pi}$ appears before
  $\myenter^{C_3}_{r', \pi}$ on $\pi$, for $q, r' \in \nprocs{n}$.

  By Lemma \ref{lema:gen:non-interfere-sufficient}, there is a
  feasible execution $\pi'$ in $G'$ s.t.\ $\pi'$ has the form:
  \[
    \pi' = \ldots{} \myenter^{C_3}_{p, \pi'} \ldots{}
    \myenter^{C_0C_1C_2}_{r, \pi'} \ldots{} \myenter^{C_0C_1C_2}_{r',
      \pi'}\ldots{}
  \]
  By Side Condition 2 of the sequence rule,
  $\nosendsubset(\Upsilon) \subseteq{} \Upsilon_0$, so $\pi'$ contains
  \textbf{PGV-II} as well, which contradicts the assumption
  that $G'$ is error free.
\end{enumerate}
$\qed$
%%%%%%%%%%%%%%%%% END OF PROOF 2 %%%%%%%%%%%%%%%%%%