\renewcommand\cfile{eqtr.tex}

It has been noted above that often
an \M-sequent can be translated to several \dRA-sequents.
In these cases it is necessary
to show that these \dRA-sequents are provably equivalent,
in that any one may be derived from any other.

\begin{lemma} \label{lem:samepv}
Suppose an \M-sequent can be translated to different \dRA-sequents,
using steps \ref{Mst1} to \ref{Mstlst},
using the same pair of point variables
(but possibly in reverse order).
Then the \dRA-sequents are provably equivalent in \dRA.
\end{lemma}

\proof\
We give only a sketch of a proof,
dealing with representatives of the situations that can arise 
where there is a choice of how to translate an \M-sequent.
In particular, we omit any proof that of any two translations,
one may be converted to the other by the rearrangements dealt with in the
following.
%However we do address every situation where there may be a choice as to which
%step of \ref{Mst2} to \ref{Mstlb1} to perform next, where that choice affects
%the final result.

Consider two different translations using 
steps \ref{Mst1} to \ref{Mstlst}, and
using the same pair of point variables.
We can consider the steps used in terms of their effect on the corresponding
graph, as described on \page{grtr}.

We first look at a graph that does not have loops.
Note that, as we look at the \emph{undirected} graph
(ie, ignoring the direction of edges), 
only steps \ref{Mst,} and \ref{Mst;} change the shape of the graph.
Each vertex (other than the two which are still there at step \ref{Mstfin})
is removed by a \ref{Mst;} step. 
Step \ref{Mst,} collapses multiple edges (including the case where
one edge was created by a \ref{Mst;} step),
which may create further vertices of degree 2,
to enable further \ref{Mst;} steps to occur.
Where the \ref{Mst;} and \ref{Mst,} steps depend on each other in this way,
it is not possible to arbitrarily re-order them.
The fact that an \ref{Mst;} step can only occur to remove a vertex of degree 
exactly 2 means that, where an \ref{Mst;} step uses an edge produced by
a preceding \ref{Mst,} step, eg
$$x[P]y, x[Q]y, y[R]z \vdash \quad \stackrel {\ref{Mst,}} \longrightarrow
\quad x[P,Q]y, y[R]z \vdash \quad \stackrel {\ref{Mst;}} \longrightarrow 
\quad x[(P,Q);R]z \vdash $$
the \ref{Mst;} step which removes $y$ cannot be put before the
\ref{Mst,} step.
Likewise, where an \ref{Mst,} step collapses an edge produced by
a preceding \ref{Mst;} step, eg
$$x[P]z, x[Q]y, y[R]z \vdash \quad \stackrel {\ref{Mst;}} \longrightarrow
\quad x[P]z, x[Q;R]z \vdash \quad \stackrel {\ref{Mst,}} \longrightarrow 
\quad x[P,(Q;R)]z \vdash $$
the \ref{Mst;} step which removes $y$ must be before the
\ref{Mst,} step.

On the other hand, where there are two consecutive  
\ref{Mst;} and \ref{Mst,} steps,
where the later one does not use an edge produced by the earlier one, 
then the order of the two
steps may be interchanged without affecting the result.

It can be seen therefore
that the only cases where steps \ref{Mst,} and \ref{Mst;} 
can be re-ordered so as to make a difference to the final result are
where several \ref{Mst,} steps are re-ordered, 
or where several \ref{Mst;} steps are re-ordered.
These cases can be handled by a number of relatively trivial observations.

Firstly, where the \M-sequent (or partly translated \M-sequent) includes (say)
$x[P]y, x[Q]y, x[R]y$,
then in translating it,
rearranging two consecutive \ref{Mst,} steps 
can give
$$ x[(P,Q),R]y \qquad x[P,(Q,R)]y \qquad x[(P,R),Q]y \qquad \ldots $$
which eventually become
$$ (P,Q),R \quad\ \ \qquad P,(Q,R)
\quad\ \ \qquad (P,R),Q \quad\ \ \qquad \ldots $$
These are all equivalent in \dRA\ by virtue of the commutativity and
associativity rules, 
($P \vdash $), ($\vdash P $), ($A \vdash $), and ($\vdash A $).

Similarly, in translating $x[P]y, y[Q]z, z[R]w$,
re-ordering two consecutive \ref{Mst;} steps 
can give
$ (P;Q);R $ or $ P;(Q;R)$, these are equivalent 
by the associativity rules for `;', 
($A; \vdash $) and ($\vdash A; $).

There is a also a similar
case where a single step can be performed in two different ways.
For $x[P]y, x[Q]y$ can become either
$x[P,Q]y$ or $ x[Q,P]y$, depending on how step \ref{Mst,} is read.
Eventually these give $(P,Q)$ or $(Q,P)$ respectively
in the \dRA-sequent;
these are interchangeable in \dRA\ by virtue of the commutativity 
rules ($P \vdash $) and ($\vdash P $).

We turn now to the rules involving loops;
%\ref{Mst;'} and \ref{Mst;`}
%and the various cases of how they can be re-ordered with other rules.
we consider the various ways in which a loop can be removed,
and how there can be a choice as to how or when to remove a loop.
Firstly, where $x,y,z$ and $w$ are not all distinct in $x[P]y, y[Q]z, z[R]w$,
the two possible orderings of the relevant 
\ref{Mst;}, \ref{Mst;'} or \ref{Mst;`} steps 
give equivalent results, again by the 
associativity rules ($A; \vdash $) and ($\vdash A; $).
For example, from $x[P]y, y[Q]z, z[R]z$ we can get
$ (P;Q);(R,1) $ or $ P;(Q;(R,1))$, which are equivalent.

More complex is a case like
$x[P]x, x[Q]x, x[R]w$,
where a loop can be removed by step \ref{Mst;'} or by step \ref{Mst,}.
We could eventually get
%$((P,Q),1);R$ or
%$(P,1);((Q,1);R)$ or
%$(Q,1);((P,1);R)$.
$$((P,Q),1);R \quad \mbox{or} \quad
(P,1);((Q,1);R) \quad \mbox{or} \quad
(Q,1);((P,1);R)$$
Of these, the latter two are (by associativity of `;') equal to
$((P,1);(Q,1));R$ and
$((Q,1);(P,1));R$ respectively, which are both equal in \dRA\ to
$((P,Q),1);R$ by 
\ttdef{cor78i} (\page{cor78i})
and the commutativity, idempotence and associativity of `,'.

Note that to use \texttt{cor78i} here we have to replace $E$ by \1.
This is justified by the display postulates and
the rules ($\1 \vdash $) and its converse, which is
obtained from (cut) and ($\vdash \1 $).
The same applies to several other theorems mentioned below.
Similarly, in using some theorems we will have to replace $I$ by $\top$,
which is justified by the rules ($\top \vdash $) and its converse, which is
obtained from (cut) and ($\vdash \top $).

A loop could be removed by different uses of step \ref{Mst;'}.
For example, $x[P]x, x[Q]w, x[R]w$
could eventually become
%$(P,1);(Q,R)$ or
%$((P,1);Q),R$ or
%$((P,1);R),Q$.
$$(P,1);(Q,R) \quad \mbox{or} \quad
((P,1);Q),R \quad \mbox{or} \quad
((P,1);R),Q$$
Of these, the first two are equal in \dRA\ by 
\ttdef{th78sr} (\page{th78sr});
also the first equals $(P,1);(R,Q)$ which, by
\texttt{th78sr}, equals $((P,1);R),Q$.

Alternatively, we may have (say)
$x[P]x, x[Q]y, x[R]z$, where the next \ref{Mst;'} step could give either
$x[(P,1);Q]y, x[R]z$ or $x[(P,1);R]z, x[Q]y$.
This case is discussed at the end of the proof.

We now consider the step \ref{Mstbl}.
Firstly, it permits changing 
$y [P]x$ to 
$x [\bullet P]y$ and then to $y [\bullet \bullet P]x$.
For this case, we have that $P$ and $\bullet \bullet P$
are equivalent in \dRA\ by the display postulate \texttt{rbbA}.
Step \ref{Mstbl} also permits changing $x[P]x$ to $x [\bullet P]x$.
Now, by steps \ref{Mst1} to \ref{Mstlst}, these will eventually appear
as $P,1$ and $\bullet P,1$
or as $(P,\ldots),1$ and $(\bullet P,\ldots),1$.
By \ttdef{blcEa} (\fig{sdr}),
$P,1$ and $\bullet P,1$ are equivalent in \dRA;
to show the \dRA-equivalence of
$(P,\ldots),1$ and $(\bullet P,\ldots),1$,
we need \texttt{blcEa} and
the commutativity and associativity of `,'.

Secondly, there are many possibilities for performing step \ref{Mstbl}
either before or after 
steps \ref{Mst,} or \ref{Mst;}.
The equivalence of the resulting \dRA-sequents
relies on the distributivity, in \dRA, of
$\bullet$ over the binary operators, and the fact that $\bullet \bullet X$ 
can be replaced by $X$.
Thus, for example, where 
$x[P]y, y[Q]x$ could become $x[P, \bullet Q]y$ or
$y [\bullet P, Q]x$, we have
$ \bullet (P, \bullet Q) = (\bullet P, \bullet \bullet Q) = (\bullet P, Q)$.
Where 
$x[P]y, x[Q]z$ could become $y [\bullet P; Q]z$ or $z [\bullet Q; P]y$,
we have 
$ \bullet (\bullet P;Q) = (\bullet Q; \bullet \bullet P) = (\bullet Q; P)$.

Thirdly, step \ref{Mstbl} can be re-ordered with steps \ref{Mst;'} and
\ref{Mst;`}.
For example, we can translate 
$x[P]x, x[Q]y $ to
$x[(P,1);Q]y $ by step \ref{Mst;'}, or to 
$x[P]x, y[\bullet Q]x $ by step \ref{Mstbl} and then to 
$y[\bullet Q; (P,1)]x $ by step \ref{Mst;`}.
To show that 
$ \bullet ((P,1);Q) $ equals
$\bullet Q; (P,1) $ we use the display postulates and the rules indicated
below.
We have
\begin{eqnarray*}
 \bullet ((P,1);Q) & = & \bullet Q ; (\bullet P,\bullet \1) 
  \qquad \mbox{(by \texttt{blscdista} and \texttt{blcdista})}
 \\ & = & \bullet Q ; (\bullet P,\1) \qquad \mbox{(by \texttt{bEa})}
 \\ & = & \bullet Q ; (P,\1) \qquad \textrm{(by \texttt{blcEa})}
\end{eqnarray*}

Finally, we look at the case of translations using the same two point
variables, but in the opposite order.
A sequent $x[P]y \vdash $ can be translated to 
$P \vdash I$, or to 
$y[\bullet P]x \vdash $ and thence to
$\bullet P \vdash I$.  That these are equivalent is shown by the 
\texttt{mblob} display postulate and the ($\vdash \bullet I$) rule.

In general, to show that two translations give results
which can be shown equivalent in \dRA\ 
requires a combination of the cases discussed above.
As noted above, we omit any proof that this can always be done.
However, by way of example, we consider the case of translating
$x[P]x, x[Q]y, x[R]z$, where the next \ref{Mst;'} step could give either
$x[(P,1);Q]y, x[R]z$ or $x[(P,1);R]z, x[Q]y$.
If subsequent steps give
$z[\bullet R; ((P,1);Q)]y$ or
$y[\bullet Q; ((P,1);R)]z$ respectively,
then this case is essentially covered by the
remarks about steps \ref{Mst;}, \ref{Mst;'}, \ref{Mst;`}
and \ref{Mstbl}, above.
Otherwise, we suppose that the remainder of two translations could
be rearranged as necessary to make the situation similar to that of
translating $x[P]x, x[Q]y, x[R]z, y[S]w, z[T]w $ in the
following two ways.

{ \small

\vpf
\bpf
\A "$x[P]x, x[Q]y, x[R]z, y[S]w, z[T]w $" 
\U [:] "$x[(P,1);Q]y, x[R]z, y[S]w, z[T]w $" "\ref{Mst;'}"
\U [:] "$x[((P,1);Q);S]w, x[R;T]w $" "\ref{Mst;}"
\U [:] "$x[(((P,1);Q);S), (R;T)]w $" "\ref{Mst,}"
%\U [:] "$(((P,1);Q);S), (R;T) $" "\ref{Mstfin}"
\epf
\hfill
\bpf
\A "$x[P]x, x[Q]y, x[R]z, y[S]w, z[T]w $" 
\U [:] "$x[Q]y, x[(P,1);R]z, y[S]w, z[T]w $" "\ref{Mst;'}"
\U [:] "$x[Q;S]w, x[((P,1);R);T]w $" "\ref{Mst;}"
\U [:] "$x[(Q;S), (((P,1);R);T)]w $" "\ref{Mst,}"
%\U [:] "$(Q;S), (((P,1);R);T) $" "\ref{Mstfin}"
\epf
}

The results of these translations are equivalent in \dRA\ by 
a combination of the results used above.
$\Box$


More difficult are the cases where we can obtain different translations
either by doing the translation using a different pair of point variables,
or by changing the \M-sequent (by virtue of \lem{misc}).
We first look at the case where the \M-sequent is changed
using \lem{mtl}.

\lem{mtl} shows that an \M-sequent
$\Gamma \vdash \Delta$
is equivalent to 
$ \Gamma, x [\top] y \vdash \Delta$.
Suppose that
$\Gamma \vdash \Delta$ can be translated into 
\dRA\ using $(x,y)$.
We now show that $ \Gamma, x [\top] y \vdash \Delta$
can be translated to an equivalent \dRA-sequent.

\begin{lemma} \label{lem:addT}
\begin{enumerate}
\renewcommand\labelenumi{(\roman{enumi})}
\renewcommand\theenumi{(\roman{enumi})}
\item \label{dRAtl}
In \dRA, $V \vdash W \iff V,\top \vdash W$
\item \label{addT}
In a \dRA-sequent, any sub-structure $X$ in an antecedent position
can be changed to $X,\top$
or to $\top, X$ to give an equivalent sequent.
\item \label{addTtr}
Suppose the \M-sequent $\Gamma \vdash \Delta$
can be translated to $V \vdash I$ in \dRA\ using $(x,y)$.
Then $ \Gamma, x [\top] y \vdash \Delta$
can be translated to the equivalent \dRA-sequent $V,\top \vdash I$.
\end{enumerate}
\end{lemma} 

\proof\
\begin{enumerate}
\renewcommand\labelenumi{(\roman{enumi})}
\item 
The forward direction is an instance of the monotonicity rule ($M \vdash $).
The reverse direction requires the display postulates, cutting with the 
($\vdash \top $) rule, $I \vdash \top $, and using the $I$-identity rule
($\vdash I$).
\item
This follows from (i), by use of the display postulates and the
commutativity rules ($P \vdash $) and ($\vdash P $).
\item
We translate
$ \Gamma, x [\top] y \vdash \Delta$ into \dRA\ using $(x,y)$,
using steps similar to those used in the translation of $\Gamma \vdash \Delta$.
Doing this we get to a point where we have 
$ x[V]y, x [\top] y \vdash \ $.
We can then translate this to $ x[V,\top] y \vdash \ $,
and then to $ V,\top \vdash I$.
These two \dRA-translations are equivalent in \dRA\ by part \ref{dRAtl}.
$\Box$
\end{enumerate}

We next deal with the case where one of the alternative \dRA-translations
uses a pair $(x,x)$.

\begin{lemma} \label{lem:(x,x)}
Suppose an \M-sequent $\Gamma \vdash \Delta$
can be translated in \dRA\ using 
steps \ref{Mst1} to \ref{Mstlst} and the pair
of point variables $(x,x)$, and suppose $x$ is not the only point variable
in the \M-sequent.
Then there is a pair of point variables $(x,y)$ such that 
the translations of $\Gamma \vdash \Delta$ into \dRA\ using $(x,y)$
are equivalent to the translations using $(x,x)$.
%$\Gamma \vdash \Delta$ can be translated to $V \vdash I$ in \dRA\
%using $(x,y)$,
%and $U \vdash I$ and $V \vdash I$ are equivalent in \dRA.
\end{lemma}

\proof\
Consider a translation of $\Gamma \vdash \Delta$ using $(x,x)$.
The last step in the translation which removed a point variable other than $x$
(call it $y$)
must have been \ref{Mst;}, as only \ref{Mst;} and \ref{Mstfin} remove
point variables.
Suppose that step took 
$x[P_1]x, x[P_2]x, \ldots, x[P_n]x, x[Q]y, y[R]x \vdash$ to
$x[P_1]x, x[P_2]x, \ldots, x[P_n]x, x[Q;R]x \vdash$.

Note that, by virtue of \lem{samepv}, we need only show the
\dRA-equivalence of two translations of our own choosing, one using
$(x,x)$ and one using $(x,y)$.
Now
$x[P_1]x, x[P_2]x, \ldots, x[P_n]x, x[Q]y, y[R]x \vdash$ 
can be translated to
$x[P]x, x[Q;R]x \vdash$ and to $(P, (Q;R)), \1 \vdash I$ by using $(x,x)$,
where $P$ is $(P_1, P_2, \ldots, P_n)$.
Alternatively, it can be translated to
$x[P]x, x[Q, \bullet R]y \vdash$ and to $(P, \1); (Q, \bullet R) \vdash I$,
using $(x,y)$.

Theorem \ttdef{tpq} \insrc{peirce.ML} shows
the equivalence in \dRA\ of 
$(P, (Q;R)), \1 \vdash I$ and $(P, \1); (Q, \bullet R) \vdash I$.

The case where $n = 0$
can be treated as a special case of the above, with 
\mbox{$P = \top$,} using Lemmas \ref{lem:mtl} and \ref{lem:addT}\ref{dRAtl}.
More simply, 
$x[Q]y, y[R]x \vdash$ can be translated to
$x[Q;R]x \vdash$ and to $ (Q;R), \1 \vdash I$ by using $(x,x)$.
Alternatively, it can be translated to
$x[Q, \bullet R]y \vdash$ and to $ Q, \bullet R \vdash I$.
Theorem \ttdef{meo} \insrc{peirce.ML} shows
the equivalence in \dRA\ of 
$ (Q;R), \1 \vdash I$ and $Q, \bullet R \vdash I$.
$\Box$

We now look at translations using any pair of point variables and
possibly using \lem{misc}.
We confine ourselves to \M-sequents using at most four point variables, 
and much of the proof involves looking at particular cases,
according to the shape of the corresponding graphs.
We first prove a number of lemmata concerning 
specific cases of \M-sequents which can be translated into 
\dRA\ in different ways.
We first look at the example given on \page{5alt},
where five \dRA-translations are given.

\begin{lemma} \label{lem:5alteq}
The five alternative \dRA-translations of
$x[A]y, y[B]z, x[C]z, x[G]w, w[H]z \vdash $, shown on \page{5alt},
are equivalent.
\end{lemma}

\proof\
This is proved using Isabelle \insrc{thmisc.ML}, as \ttdef{t5}.
In fact the proofs are particularly straightforward, using 
the display postulates, the $I$-identity axioms, and the 
derived rules in \dRA\ giving distributivity 
of `$*$' and `$\bullet$' over `;' and `,'.
For example (and note that all the steps in this proof are reversible),
\vpf
\begin{center}
\bpf
\A "$A, ((C, (G; H)); \bullet B) \vdash I$"
\U "$A, * ((* (G; H), * C); * \bullet B) \vdash I$" "(dp, $*$-dist)"
\U "$A \vdash I, ((* (G; H), * C); * \bullet B)$" "(dp)"
\U "$A \vdash ((I, * (G; H)), * C); * \bullet B$" "(dp, $\vdash I$)"
\U "$((A; B), C), (G; H) \vdash I$" "(dp)"
\epf
\end{center}
$\Box$

In the following Lemma, if $\bullet H$ is set to the identity \1,
we get $(ii) \iff (i)$ of \cite{CT}, Theorem 2.1.

\begin{lemma} \label{lem:eq4}
The following two \dRA-translations of 
$x[A]y, y[B]z, x[C]z, w[H]z \vdash $ are equivalent:
$$
((\bullet A;C), B);\bullet H \vdash I
\qquad \qquad
((A;B), C);\bullet H \vdash I 
$$
\end{lemma} 

\proof\
The following proof shows the forward direction; the reverse direction is
similar.
\vpf
\begin{center}
\bpf
\A "$((\bullet A; C), B); \bullet H \vdash I$"
\U "$(B, (\bullet A; C)); \bullet H \vdash I$" "($P \vdash $)"
\U "$(B, * (* \bullet A; * C)); * \bullet * \bullet \bullet H \vdash I$"
    "(dp, $*$-dist, $*$-dbl, $\bullet$-dbl, $*\bullet$-comm)"
\U "$(B, * (* \bullet A; * C));
    * \bullet * \bullet \bullet H \vdash * \bullet A; I$" "(ExI)"
\U "$B, * (* \bullet A; * C) \vdash (* \bullet A; I); * \bullet \bullet H$"
    "(dp)"
\U "$B, * (* \bullet A; * C) \vdash * \bullet A; (I; * \bullet \bullet H)$"
    "($\vdash A; $)"
\U "$B \vdash (* \bullet A; (I; * \bullet \bullet H)), (* \bullet A; * C)$"
    "(dp)"
% \U "$B \vdash (* \bullet A; ((I; * \bullet \bullet H), * C)),
    % (* \bullet A; ((I; * \bullet \bullet H), * C))$" "($\vdash M $)"
\U "$B \vdash * \bullet A; ((I; * \bullet \bullet H), * C)$"
  "(\texttt{sccldists})"
\U "$((A; B), C); \bullet H \vdash I$" "(dp)"
\epf
\end{center}
$\Box$

The next lemma will be used to show equivalence of translations of 
the sequent given on \page{3star}, and discussed following \lem{misc}.

\begin{lemma} \label{lem:eqst}
The following two \dRA-translations of 
$y[B]z, x[C]z, w[H]z \vdash $ are equivalent:
$$
((\top ;B), C);\bullet H \vdash I 
\qquad \qquad
(C, (\top ;H)); \bullet B \vdash I
$$
\end{lemma} 

\proof\
By \lem{addT}\ref{dRAtl} these are respectively equivalent to
$$
(((\top ;B), C);\bullet H), \top  \vdash I
\qquad \mbox{and} \qquad
\top, ((C, (\top;H)); \bullet B) \vdash I
$$
These are the cases $(x,w)$ and $(x,y)$ of the five on 
\page{5alt}, with $A$ and $G$ set to $\top$.
They are therefore equivalent by \lem{5alteq}. $\Box$


\begin{thm} \label{eqtrthm}
Suppose an \M-sequent can be translated to different \dRA-sequents,
using steps \ref{Mst1} to \ref{Mstlst} and \lem{misc}.
Then the \dRA-sequents are equivalent.
\end{thm}

\proof\
Again, we present only a sketch of a proof, covering 
a representative set of examples of the cases where a translation
can be done in different ways.
By virtue of Lemmas \ref{lem:samepv} and \ref{lem:(x,x)},
we need only look at two translations
using different pairs of point variables,
each pair being two distinct point variables,
or which use \lem{misc}.

We first look at cases where \lem{misc}
is used to add a formula $x[\top]y$ to an \M-sequent 
$\Gamma \vdash \Delta$.
\lem{addT}\ref{addTtr} deals with such cases when 
$\Gamma \vdash \Delta$ can be translated using $(x,y)$.
So we look at the cases where 
the \M-sequent corresponds to a graph with a vertex of degree 1.

Firstly, we may use \lem{misc} to translate 
$x[A]y, x[C]z$, where $y$ does not appear anywhere else.
We look at adding $y[\top]x$ or $y[\top]z$,
translating to $x[((A;\top),\1);C]z$
and $x[(A;\top),C]z$ respectively.
To show that these are equal in \dRA, we note that 
since $\top$ and $\1$
in the antecedent part are equivalent to 
$I$ and $E$, the equality of  
$((A;\top),\1);C$
and $(A;\top),C$ is given by (s56)\index{s56} on \page{s56}.

Secondly, where the graph has multiple edges joining $x$ to $y$,
but these are the only edges to $y$,
and there are other edges incident to $x$,
say $x[A]y, y[F]x, x[C]z$, where $y$ does not appear anywhere else.
In translating this we may go to 
$x[A, \bullet F]y, x[C]z$ and proceed as above,
getting $x[((A, \bullet F);\top),C]z$ 
or we may go to
$x[A;F]x, x[C]z$, and get
$x[((A;F),\1);C]z$.
The equality of these two follows from \ttdef{thab} on \page{thab}.

The third case, which is also a special case of \lem{(x,x)},
is where there are no other edges incident to $x$,
say $x[A]y, y[F]x \vdash$ , where the \M-sequent contains no other formulae.
In translating this, 
we finish with the two alternative \dRA-translations
$A, \bullet F \vdash I$ or
$(A;F),\1 \vdash I$.
The equivalence of these is the theorem \ttdef{meo} \insrc{peirce.ML}.

We now look at specific cases of \M-sequents 
with at most four point variables which can be translated into
\dRA\ in different ways.
We can consider these \M-sequents in terms of the shape of the corresponding
graphs.  We first look at the example, with five edges, given in \fig{5altgph},
for which five \dRA-translations are given on \page{5alt}.
\lem{5alteq} shows that these five \dRA-translations are equivalent.

As an illustration of the part of \lem{samepv}
relating to step \ref{Mstbl},
we note that there are five more translations,
which use the same pairs of point variables,
but in the opposite direction.
For example, whereas the translation using $(x,z)$ is
$((A; B), C), (G; H) \vdash I$, that using $(z,x)$ is
$((\bullet B; \bullet A), \bullet C), (\bullet H; \bullet G) \vdash I$.
These two are shown to be equivalent by use of the \texttt{bIs} and
\texttt{mblob} rules, and by repeated use the distributive rules for $\bullet$,
\texttt{blscdista} and \texttt{blcdista}.

We next look at \M-sequents whose graphs have four edges,
and which can be translated in different ways.
Firstly, 
$x[A]y, y[B]z, x[G]w, w[H]z \vdash $ has \dRA-translations
using each pair of point variables.
If we set $C$ to $\top$ in the five translations of 
$x[A]y, y[B]z, x[C]z, x[G]w, w[H]z \vdash $ , shown on \page{5alt},
and use \lem{addT}\ref{addT} to omit the $\top$, then
we have \dRA-translations of $x[A]y, y[B]z, x[G]w, w[H]z \vdash $ 
for five of the possible pairs of point variables.
Then \lem{5alteq} shows that these \dRA-translations are equivalent.

That is, the \dRA-translations using 
$(x,y)$, $(y,z)$, $(x,z)$, $(x,w)$ and $(w,z)$
are equivalent.
By a similar argument, 
the \dRA-translations using 
$(y,z)$, $(z,w)$, $(y,w)$, $(y,x)$ and $(x,w)$ 
are equivalent.
By continuing in this way, it can be seen that
the \dRA-translations using 
each pair of distinct point variables are equivalent.

The most difficult \M-sequent is one of the form
$x[A]y, y[B]z, x[C]z, w[H]z \vdash $~.
To translate this one, we need to add a formula, relying on
\lem{mtl}.
If we add the formula $x [\top] w$, then this gives 
a sequent whose graph is like that in \fig{5altgph};
its \dRA-translations are shown equivalent by \lem{5alteq}.
One of the \dRA-translations, the one using $(x,w)$, is
$(((A;B), C);\bullet H), \top \vdash I$.
By \lem{addT}\ref{dRAtl} it is equivalent to
$((A;B), C);\bullet H \vdash I$.
If, on the other hand,
we add the formula $y [\top] w$,
then this gives a different sequent, whose graph has the same shape.
It therefore has a similar, but different set of \dRA-translations;
these also are equivalent to each other, by \lem{5alteq}.
Of these the one using $(y,w)$ simplifies to
$((\bullet A;C), B);\bullet H \vdash I$.
\lem{eq4} shows that 
$((A;B), C);\bullet H \vdash I$ and
$((\bullet A;C), B);\bullet H \vdash I$
are equivalent.

We next look at \M-sequent whose graphs have three edges.
An \M-sequent of the form $y[B]z, x[C]z, w[H]z \vdash $
gives a graph whose shape is three edges meeting at a single vertex, as
in \fig{3star}.
By \lem{mtl}, if we add the formula $x [\top] y$,
we get an equivalent \M-sequent;
this sequent is of the form we have
just considered, with (\emph{inter alia}) the following two \dRA-translations,
which are equivalent by \lem{eq4}.
% \begin{itemize} 
% \item[] $((\bullet \top ;C), B);\bullet H \vdash I$ (using $(y,w)$
% \item[] $((\top ;B), C);\bullet H \vdash I $ (using $(x,w)$
% \end{itemize}
$$
((\bullet \top ;C), B);\bullet H \vdash I \quad \mbox{(using } (y,w))
\qquad
((\top ;B), C);\bullet H \vdash I \quad \mbox{(using } (x,w))
$$
(in fact $\top $ and $\bullet \top $ are equal, and can be 
interchanged in \dRA).

However, instead of adding $x [\top] y$, 
we could instead have chosen to add
either $x [\top] w$ or $y [\top] w$.
This would have given a different \M-sequent
of the same form, with different \dRA-translations.
For example, if we add $x [\top] w$,
we get (\emph{inter alia}) these two equivalent \dRA-translations
%In the case where we add $x [\top] w$ 
%the \dRA-translation using $(x,y)$ is
$$(C, (\top ;H)); \bullet B \vdash I \quad \mbox{(using } (x,y))
\qquad
((\bullet \top ;C), H); \bullet B \vdash I \quad \mbox{(using } (w,y))$$
\lem{eqst} now shows that all these four
\dRA-translations are equivalent.

The equivalence of the \dRA-translations got by adding
$y [\top] w$ to those above is shown similarly.
It follows that whichever choice we make in translating
$y[B]z, x[C]z, w[H]z \vdash $ , the \dRA-translations are equivalent.

The other possibility for an \M-sequent giving a graph with three edges is
$x[A]y, y[B]z, x[C]z \vdash $ ,
whose graph is a triangle.
This sequent can be translated using each pair of the three
point variables.
\lem{eq4}, with $H$ set to \1,
shows the equivalence of two of the translations.
(Note that $\1 $ and $\bullet \1 $ are equal, and can be 
interchanged in \dRA).
The remaining equivalence could be shown similarly.

It remains to look at \M-sequents whose graph has two edges.
The only tricky case is where the two edges are disconnected,
for example, $x[A]y, w[H]z \vdash $~.
This \M-sequent can be translated by adding any of
$x [\top] w$, $x [\top] z$, $y [\top] w$ or $y [\top] z$.
These give the \dRA-translations 
$$(\bullet A ; \top) ; H \vdash I \qquad
(\bullet A ; \top) ; \bullet H \vdash I \qquad
(A ; \top) ; H \vdash I \qquad
(A ; \top) ; \bullet H \vdash I$$
We show the \dRA-equivalence of these using the associative rule ($A; \vdash$)
and \lem{eq4}, as in the following example.
\vpf
\begin{center}
\bpf
\A "$I \vdash \top$"
\A "$(\bullet A ; \top) ; \bullet H \vdash I$"
\U "$((\bullet A ; \top), \top) ; \bullet H \vdash I$" "(dp, $I \vdash$, VerI)"
\U "$(( A ; \top), \top) ; \bullet H \vdash I$" "(\lem{eq4})"
\B "$( A ; \top) ; \bullet H \vdash I$" "(dp, cut, $I \vdash$)"
\epf
\end{center}

This completes the proof of Theorem~\ref{eqtrthm}. $\Box$

\renewcommand\cfile{}