To simplify the program of reasoning a triple, we add two restrictions
on the use of the \texttt{absent} assertions.  The restrictions will
limit the expressive power of the specification but so far we have not
encountered an example whose specification cannot be expressed under
the restrictions.  First, we restrict that if a pre-condition or a
post-condition is converted to a conjunctive normal form, any
\texttt{absent} assertion appears in it will form a conjunctive
clause.  That means that no operator can be applied to an
\texttt{absent} assertion in the conjunctive clause.  For example, a
condition
$P \texttt{ \&\& absent(}\theta_0, \theta_1, \theta_2\texttt{)}$
satisfies the restriction while
$P \texttt{ \&\& !absent(}\theta_0, \theta_1, \theta_2\texttt{)}$ does
not.  Second, we restrict that if an assertion
\texttt{absent($\theta_0$, $\theta_1$, $\theta_2$)} appears in a
pre-condition, $\theta_0$ must have the form \texttt{send(src, dest)}.

\subsection{Proof System for Collective Triples}
To reason about collective triples, we introduce a proof system
$\mathbb{H}_c$ which consists of two inference rules.  The proof
system is given in Figure \ref{fig:proof-rules}.  The proof system
$\mathbb{H}_c$ is not complete but sound. The incompleteness means
that if $\model \models \cotriple{}$, one may not be able to find a
proof in $\mathbb{H}_c$ with some assumptions.  The soundness means
that if there is a proof of $\model \models \cotriple{}$ using rules
in $\mathbb{H}_c$, then $\model \models \cotriple{}$.

\begin{figure}
  \begin{enumerate}
  \item[] 
    \begin{align}
      &\frac{
        \lco{}\psi\rco{} ~C_0~ \lco{}Q\rco{},\,
        \lco{}Q[\textbf{T}/\overrightarrow{a}]\rco{} ~C_1~ \lco{}\phi\rco{}
        }{
        \lco{}\psi[\textbf{T}/\overrightarrow{d}]\rco{} ~C_0 \texttt{;} C_1~ \lco{}\phi\rco{}
        } ~~\text{ (composition) }
        \nonumber 
    \end{align}
    , where
    \begin{itemize}
    \item $Q[\textbf{T}/\overrightarrow{a}]$ denotes a condition which
      is obtained from $Q$ by substituting all expressions in the set
      $\overrightarrow{a}$ in $Q$ by constant $\textbf{T}$; ditto for
      $\psi[\textbf{T}/\overrightarrow{d}]$.
    \item $\overrightarrow{a}$ is the set of all absent assertions
    \item $\overrightarrow{d}$ is the set of \emph{discharged} absent
      assertions by $\phi$
    \end{itemize}
    side codition: \\
    
  \item[] 
    \begin{align}
      &\frac{
        \cotriple
        }{
        \lco{}\phi'\rco{}~C~\lco{}\psi'\rco{}
        }  ~~\text{ (consequence) }  \nonumber
    \end{align}
    side condition \\
  \end{enumerate}
\end{figure}