\renewcommand\cfile{mimlems.tex}

We turn now to proving that a proof in \M\ (``an \M-proof")
using at most four variables can be mimicked in \dRA.
(Recall from \S\ref{madint}
that these are the \M-proofs whose conclusions hold in \RA).
Naturally we confine our attention to a proof whose premises
and conclusion can be translated into \dRA.
By virtue of Theorems \ref{mmp} and \ref{pw}
we look instead at an \Mp-proof satisfying the conditions in 
Theorem~\ref{pw}.

%show that each step, 
%or, in some cases, a combination of steps, of that proof can be 
We aim to take an \Mp-proof and turn it into a \dRA-proof. 
We would like to do this by turning each step of the \Mp-proof
into a corresponding step of a \dRA-proof.
However, when there are intermediate $K_4^*$-sequents in the \Mp-proof, 
we cannot do this;
we cannot turn a single \Mp-proof step into \dRA\ if one of its premises
or its conclusion cannot be translated into \dRA.
So in these cases, we need to find a larger part of the \Mp-proof
which can be turned into \dRA.

We first need some proof theoretic results about \Mp-proofs.
These will enable us to rearrange the steps of an \Mp-proof 
in such a way that the proof can be divided into parts,
each of which can be turned into a \dRA-proof.

\begin{lemma} \label{lem:reoc}
Any two consecutive cuts in a proof tree can be re-ordered,
in the way shown in the diagrams below.
\end{lemma} 

\proof\
Suppose we have two consecutive cuts, with cut-formulae $\delta$ and $\gamma$.
We thus have the following situation, or a mirror image of it,
with $\delta$ and $\gamma$ not in 
$ \Gamma, \Gamma', \Gamma'', \Delta, \Delta'$ or $ \Delta'' $.
\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \gamma $"
\A "$ \Gamma', \gamma \vdash \Delta', \delta $"
\A "$ \Gamma'', \gamma, \delta \vdash \Delta'' $"
\B "$ \Gamma', \Gamma'', \gamma \vdash \Delta', \Delta'' $" "(cut-$\delta$)"
\B "$ \Gamma, \Gamma', \Gamma'' \vdash \Delta, \Delta', \Delta'' $"
"(cut-$\gamma$)"
\epf
\end{center}

The cuts can be re-ordered thus
\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \gamma $"
\A "$ \Gamma', \gamma \vdash \Delta', \delta $"
\B "$ \Gamma, \Gamma' \vdash \Delta, \Delta', \delta $" "(cut-$\gamma$)"
\A "$ \Gamma \vdash \Delta, \gamma $"
\A "$ \Gamma'', \gamma, \delta \vdash \Delta'' $"
\B "$ \Gamma, \Gamma'', \delta \vdash \Delta, \Delta'' $" "(cut-$\gamma$)"
\B "$ \Gamma, \Gamma', \Gamma'' \vdash \Delta, \Delta', \Delta'' $"
"(cut-$\delta$)"
\epf
\end{center}

Note that $\gamma$ may appear on the left-hand side of only one
of the premises of the first diagram above (rather than twice, as shown);
in this case the re-ordered proof would be simpler, and is not shown.
$\Box$

Note that even though the number of cuts has been increased,
the \emph{set} of cut-formulae used is unchanged.
Further, although we have introduced two cuts on $\gamma$, these are
parallel rather than sequential, ie they are on separate branches of the proof.
We will call two proof steps \bfi{sequential} if they appear in a proof tree,
in one sequence of proof steps, 
ie, one ``above'',or an ancestor of, the other;
they need not be consecutive.
In fact we can avoid repeated sequential cuts on the same formula.

\begin{lemma} \label{lem:scuts}
\begin{enumerate}
\renewcommand\theenumi{\thethm(\roman{enumi})}
\renewcommand\labelenumi{(\roman{enumi})}
\item \label{scuts1}
If an \Mp-proof tree, which consists wholly of cuts, contains 
two sequential cuts on a given formula $\delta$,
then the proof can be re-ordered and simplified to avoid this.
\item \label{scuts2}
If an \Mp-proof tree consists wholly of cuts
then it can be replaced by a proof tree which 
does not contain two sequential cuts on any one formula.
\end{enumerate}
\end{lemma} 

\proof\
(i)
We re-order the proof, repeatedly using the transformation of \lem{reoc},
to move the higher of the 
two cuts downwards until it is immediately above the lower one.
So we get (with $\delta$ not in 
$ \Gamma, \Gamma', \Gamma'', \Delta, \Delta'$ or $ \Delta'' $)
\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \delta $"
\A "$ \Gamma', \delta \vdash \Delta', \delta $"
\A "$ \Gamma'', \delta \vdash \Delta'' $"
\B "$ \Gamma', \Gamma'', \delta \vdash \Delta', \Delta'' $" "(cut-$\delta$)"
\B "$ \Gamma, \Gamma', \Gamma'' \vdash \Delta, \Delta', \Delta'' $"
"(cut-$\delta$)"
\epf
\end{center}

This can be simplified trivially to
\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \delta $"
\A "$ \Gamma'', \delta \vdash \Delta'' $"
\B "$ \Gamma, \Gamma'' \vdash \Delta, \Delta'' $" "(cut-$\delta$)"
\epf
\end{center}
from which we can use monotonicity
to obtain the conclusion
$ \Gamma, \Gamma', \Gamma'' \vdash \Delta, \Delta', \Delta'' $.
The monotonicity step could then be postponed, if desired,
as discussed previously,
to the bottom of a following sequence of cuts.

(ii)
As the transformation of \lem{reoc}
can increase the number of cuts, 
it is not trivial to show that repeated use of part~(i)
eventually terminates.
Where we have two cuts on $\delta$, and are using \lem{reoc}
to move the higher one downwards, then we create two cuts on $\gamma$
(ie, the $\gamma$ of \lem{reoc})
where there was just one.
However, if as a result of the transformation of \lem{reoc}
there is a pair of cuts on $\gamma$
in a sequence, then there was such a pair before the transformation.
(There may be two such pairs after the transformation, in place of one before).
The use of \lem{reoc} does not increase 
the number of cuts on $\delta$,
and when we complete the transformation of part~(i),
the number of cuts on $\delta$ has decreased.

Thus, when we repeatedly use part~(i) we decrease  
the number of cuts on $\delta$,
until eventually there are no sequential cuts on $\delta$.
In so doing, we may have increased the \emph{number}
of pairs of sequential cuts on
other formulae, but we have not 
enlarged the \emph{set} of formulae on which there exists
a pair of sequential cuts, and we have removed $\delta$ from that set.
Therefore we can repeat this process with each other formula on which there
is a pair of sequential cuts, and eventually we will have a proof tree with no
pair of sequential cuts on the same formula.
$\Box$

% We can use this lemma repeatedly to eliminate all instances where two
% cuts, in a sequence of successive cuts, use the same cut-formula.
Define an 
\textbf{\boldmath internally-$K_4^*$ proof tree}%
\index{internally-K4*$@internally-$K_4^*$|textbf}
to be a proof tree whose premises and conclusions 
are not $K_4^*$-sequents (can be translated into \dRA),
but whose intermediate sequents are $K_4^*$-sequents 
(can not be translated into \dRA).
In considering the problem of proof trees with $K_4^*$-sequents,
we consider separately the internally-$K_4^*$ parts of a tree.
We also consider the case where Lemmas \ref{lem:reoc} and \ref{lem:scuts}
have been used to make the internally-$K_4^*$ parts as small as possible.

For an \M-sequent $\Gamma \vdash \Delta$,
we define a \bfi{missing pair} of point variables
to be a pair $\{y,w\}$ of distinct point variables 
which appear in $\Gamma \cup \Delta$ but such that 
none of the formulae in $\Gamma \vdash \Delta$ uses $\{y,w\}$
(see \page{usesuop}).
Missing pairs are important because an \M-sequent 
containing at most four point variables can be translated into
\dRA\ if and only if it has a missing pair, by \thrm{notK4}.

\begin{thm} \label{allcuts}
Suppose an \Mp-proof tree satisfies:
\begin{enumerate}
\renewcommand\labelenumi{(\roman{enumi})}
\item it consists wholly of cuts
\item 
it is internally-$K_4^*$
\item 
it cannot be rearranged, using Lemmas \ref{lem:reoc} and \ref{lem:scuts},
to make a proof tree consisting of cuts
(with maybe a monotonicity step at the end),
all of whose internally-$K_4^*$ parts use fewer distinct cut-formulae.
\end{enumerate}
Then there is one pair of point variables $\{y,w\}$ such that 
all the cut-formulae use that pair,
ie, each cut-formula is $y[R]w$ or $w[R]y$ for some $R$
($R$ may be different for each one).
\end{thm} 

\proof\
Using Lemmas \ref{lem:reoc} and \ref{lem:scuts}, we can re-order the proof tree
so that any given cut-formula $\gamma$ appears at the bottom, and
any other given cut-formula $\delta$ appears immediately above it.
(To do this, \emph{first}
move \emph{all} the cuts on $\gamma$ to the bottom using
\lem{reoc}, making them into one cut using \lem{scuts};
\emph{then} do the same for $\delta$ in the parts of the tree above
the cut on $\gamma$.)
Call the resulting proof tree $\mathcal T$. 
This gives a configuration like the following (where these are the 
only cuts on $\gamma$ or $\delta$ in $\mathcal T$).

\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \gamma, \delta $"
\A "$ \Gamma', \delta \vdash \Delta', \gamma $"
\B "$ \Gamma, \Gamma' \vdash \Delta, \Delta', \gamma $" "(cut-$\delta$)"
\A "$ \Gamma'', \gamma \vdash \Delta'', \delta $"
\A "$ \Gamma''', \gamma, \delta \vdash \Delta''' $"
\B "$ \Gamma'', \Gamma''', \gamma \vdash \Delta'', \Delta''' $" "(cut-$\delta$)"
\B "$ \Gamma, \Gamma', \Gamma'', \Gamma''' \vdash 
  \Delta, \Delta', \Delta'', \Delta''' $"
"(cut-$\gamma$)"
\epf
\end{center}

Note that a cut on $\delta$ may appear on only one side,
and that $\gamma$ may be absent from some of the sequents in which it is 
shown, in which case the argument is similar but simpler.

By the hypothesis, there is an internally-$K_4^*$ 
sub-tree $\mathcal T'$ of $\mathcal T$ which
contains cuts on all the same cut-formulae
(including $\gamma$ and $\delta$).
Since $\mathcal T'$ contains a cut on $\gamma$,
and the last step of $\mathcal T$ (whose bottom part is shown above)
is the only cut on $\gamma$ in $\mathcal T$,
the conclusion of $\mathcal T'$
must be the conclusion of $\mathcal T$, 
ie $ \Gamma, \Gamma', \Gamma'', \Gamma''' \vdash 
  \Delta, \Delta', \Delta'', \Delta''' $.

As $ \Gamma, \Gamma', \Gamma'', \Gamma''' \vdash 
  \Delta, \Delta', \Delta'', \Delta''' $ is
the conclusion of an internally-$K_4^*$ proof tree,
it can be translated into \dRA.
Therefore it has a missing pair of point variables, say $\{y,w\}$.
That is, none of
$ \Gamma, \Gamma', \Gamma'', \Gamma''', 
\Delta, \Delta', \Delta''$ or $\Delta'''$
contains a formula which uses $\{y,w\}$.

As $\mathcal T'$ also contains a cut on $\delta$,
at least one of the premises of the cut on $\gamma$ 
in the diagram above
(namely,
$ \Gamma, \Gamma' \vdash \Delta, \Delta', \gamma $ or
$ \Gamma'', \Gamma''', \gamma \vdash \Delta'', \Delta''' $)
must be a $K_4^*$-sequent.
%As some intermediate sequent \emph{does}
That is, that premise does not have a missing pair,
so it contains a formula which uses $\{y,w\}$.
As no formula in $ \Gamma, \Gamma', \Gamma'', \Gamma''', 
\Delta, \Delta', \Delta''$ or $\Delta'''$ uses $\{y,w\}$,
the formula which uses $\{y,w\}$ must be the cut-formula $\gamma$.

We can Lemmas \ref{lem:reoc} and \ref{lem:scuts} to re-order the proof tree
$\mathcal T$ to give (in several steps) the following proof tree

\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, \gamma, \delta $"
\A "$ \Gamma'', \gamma \vdash \Delta'', \delta $"
\B "$ \Gamma, \Gamma'' \vdash \Delta, \Delta'', \delta $" "(cut-$\gamma$)"
\A "$ \Gamma', \delta \vdash \Delta', \gamma $"
\A "$ \Gamma''', \gamma, \delta \vdash \Delta''' $"
\B "$ \Gamma', \Gamma''', \delta \vdash \Delta', \Delta''' $" "(cut-$\gamma$)"
\B "$ \Gamma, \Gamma', \Gamma'', \Gamma''' \vdash 
  \Delta, \Delta', \Delta'', \Delta''' $"
"(cut-$\delta$)"
\epf
\end{center}

The conclusion
$ \Gamma, \Gamma', \Gamma'', \Gamma''' \vdash 
  \Delta, \Delta', \Delta'', \Delta''' $
is the same as before, and has the missing pair $\{y,w\}$.
As before, by the hypothesis, there is an internally-$K_4^*$ 
sub-tree of this proof tree which
contains cuts on all the same cut-formulae (including $\gamma$ and $\delta$).
By the same argument one of the premises of the bottom cut contains
a formula which uses $\{y,w\}$, and this formula must be $\delta$.
That is, $\gamma$ and $\delta$ are formulae using the same pair of point
variables $\{y,w\}$. $\Box$

\begin{lemma} \label{lem:case2}
Consider an internally-$K_4^*$ \Mp-proof tree,
which consists entirely of cuts on 
formulae which use the same pair $\{y,w\}$ of point variables,
and assume that $\{y,w\}$ is a missing pair for the conclusion.
Then the premises $\mathcal P_i$ 
and conclusion $\mathcal C$ 
of the proof tree can be translated
into \dRA-sequents $\mathcal P_i'$ and $\mathcal C'$ 
such that $\mathcal C'$ can be proved from the $\mathcal P_i'$ 
in \dRA.
\end{lemma}

\proof\
Here we cannot turn the proof into \dRA\ by treating each cut separately,
since the intermediate \M-sequents are $K_4^*$-sequents,
which cannot be translated into \dRA.

We know that each cut-formula uses the pair of point variables $\{y,w\}$.
Now, the crux of the proof below is to view the sequents and graphs
in terms of the cut-formulae and the point variables $\{y,w\}$ which they use.
Note that any formula in any premise $\mathcal P_i$ 
which uses $\{y,w\}$ must be a cut-formula, because the
conclusion $\mathcal C$ contains no formula using $\{y,w\}$.
Then as the premises of the proof tree 
are 4-sequents which can be translated into \dRA,
for each premise $\mathcal P_i$ there is a missing pair of point variables 
such that no formula in $\mathcal P_i$ uses that pair.
Thus the premises, can be partly translated by
steps \ref{Mstmv}, \ref{Mstbl}, \ref{Mst,}, \ref{Mst;'} and \ref{Mst;`},
into (without loss of generality) one of the forms below.
The missing pair,
and a complete translation into \dRA\ using the pair $(y,w)$,
are also shown.

Note that in this translation process,
where there is more than one pair of point variables not used by
any formula in the sequent, it may be necessary
to add a formula such as $x \top y$ to enable translation into \dRA.)
In the translation, where there are formulae of the form
$y[R]y$ or $w[R]w$, we assume that the translation steps are
chosen to avoid using 
a formula $y[D]w$ or $w[D]y$ in steps \ref{Mst;'} or \ref{Mst;`}.
Then, in the translation,
the cut-formulae are only affected by steps \ref{Mstmv}, \ref{Mstbl} and
\ref{Mst,}.
\vspace{-2ex}
%\begin{center}
%\begin{tabular}{c@{\hspace{3em}}c}
%$x[A_1]y, y[B_1]z, x[G_1]w, w[H_1]z , y[D_1]w \vdash$ &
%$ \Big( (\bullet A_1; G_1), (B_1; \bullet H_1) \Big), D_1  \vdash I$ \\
%$x[A_2]y, y[B_2]z, x[C_2]z, w[H_2]z , y[D_2]w \vdash$ &
%$ \Big( ((\bullet A_2; C_2), B_2); \bullet H_2 \Big), D_2  \vdash I$ \\
%$x[A_3]y, y[B_3]z, x[C_3]z, x[G_3]w , y[D_3]w \vdash$ &
%$ \Big( (\bullet A_3, (B_3; \bullet C_3)); G_3 \Big), D_3  \vdash I$ \\
%$y[B_4]z, x[C_4]z, x[G_4]w, w[H_4]z , y[D_4]w \vdash$ &
%$ \Big( B_4; (\bullet H_4, (\bullet C_4; G_4)) \Big), D_4  \vdash I$ \\
%$x[A_5]y, x[C_5]z, x[G_5]w, w[H_5]z , y[D_5]w \vdash$ &
%$ \Big( \bullet A_5; (G_5, (C_5; \bullet H_5)) \Big), D_5  \vdash I$
%\end{tabular}
%\end{center}

\begin{center}
\begin{tabular}{c@{\hspace{1.0em}}c@{\hspace{1.0em}}c}
$\{x,z\}$ &
$x[A_1]y, y[B_1]z, x[G_1]w, w[H_1]z , y \mathcal D_1 w \vdash$ &
$ \Big( (\bullet A_1; G_1), (B_1; \bullet H_1) \Big), D_1  \vdash I$ \\
$\{x,w\}$ &
$x[A_2]y, y[B_2]z, x[C_2]z, w[H_2]z , y \mathcal D_2 w \vdash$ &
$ \Big( ((\bullet A_2; C_2), B_2); \bullet H_2 \Big), D_2  \vdash I$ \\
$\{w,z\}$ &
$x[A_3]y, y[B_3]z, x[C_3]z, x[G_3]w , y \mathcal D_3 w \vdash$ &
$ \Big( (\bullet A_3, (B_3; \bullet C_3)); G_3 \Big), D_3  \vdash I$ \\
$\{x,y\}$ &
$y[B_4]z, x[C_4]z, x[G_4]w, w[H_4]z , y \mathcal D_4 w \vdash$ &
$ \Big( B_4; (\bullet H_4, (\bullet C_4; G_4)) \Big), D_4  \vdash I$ \\
$\{y,z\}$ &
$x[A_5]y, x[C_5]z, x[G_5]w, w[H_5]z , y \mathcal D_5 w \vdash$ &
$ \Big( \bullet A_5; (G_5, (C_5; \bullet H_5)) \Big), D_5  \vdash I$
\end{tabular}
\end{center}

Here $y \mathcal D_i w $ stands for all the cut-formulae which
appear in the respective \M-sequent,
after being modified by application of steps
\ref{Mstmv} and \ref{Mstbl}; so a relational term may have
been preceded by `$*$' or `$\bullet$'.
Then let $y[D_i]w$ stand for the result of applying step \ref{Mst,}
to $y \mathcal D_i w $, 
%ie, $y \mathcal D_i w $ is just $D_i$ 
eg, if $y \mathcal D_i w $ is say $y[D_i']w, y[\bullet D_i'']w, y[* D_i''']w$ 
then $D_i$ is $D_i', \bullet D_i'', * D_i'''$. 

We must now imagine the \Mp-proof in a modified form, using variants
of the \M\ (cut) rule which operate on formulae preceded by the operators
`$\bullet$' and `$*$'.
These variants would be
$$
\frac {\Gamma , y[D]w \vdash \qquad \Gamma' , y[*D]w \vdash}
{\Gamma , \Gamma' \vdash }
\qquad \mbox{and} \qquad
\frac {\Gamma , y[\bullet D]w \vdash \qquad \Gamma' , y[\bullet *D]w \vdash}
{\Gamma , \Gamma' \vdash }
$$
Note that these are not actually rules of \M\ because of the presence
of `$\bullet$' and `$*$';
rather they are the rules which would appear to be used if we took the
proof tree (consisting of cuts) in \Mp,
and partly translated all the sequents into the intermediate forms shown in the
table above.

We can then define corresponding variants of the \dRA\ (cut) rule,
which will be just like the rules above, but without 
reference to the point variables $y$ and $w$, as follows
$$
\frac {\Gamma , D \vdash \qquad \Gamma' , *D \vdash}
{\Gamma , \Gamma' \vdash }
\qquad \mbox{and} \qquad
\frac {\Gamma , \bullet D \vdash \qquad \Gamma' , \bullet *D \vdash}
{\Gamma , \Gamma' \vdash }
$$
These modified \dRA\ ``pseudo-(cut)'' rules will incorporate 
contraction ($C \vdash $), associativity and commutativity
(which are implicit in the \M\ rules, as $\Gamma$ and $\Gamma'$
are \emph{sets}), where where they are needed 
to imitate an instance of the modified \M\ rule.
They can be derived in \dRA\ using the \dRA\ (cut) rule 
and the display postulates, as indicated below, together with contraction and
the associativity and commutativity of `,'.

\vpf
\begin{center}
\qquad
\bpf
\A "$\Gamma' , *D \vdash$"
\U "$\Gamma'  \vdash D $" "(dp)"
\A "$\Gamma , D \vdash $"
\U "$ D \vdash *\Gamma $" "(dp)"
\B "$\Gamma'  \vdash *\Gamma $" "(cut)"
\U "$\Gamma , \Gamma' \vdash $" "(dp)"
\epf
\hfill
\bpf
\A "$\Gamma' , \bullet *D \vdash$"
\U "$\bullet \Gamma'  \vdash D $" "(dp)"
\A "$\Gamma , \bullet D \vdash $"
\U "$ D \vdash \bullet *\Gamma $" "(dp)"
\B "$\bullet \Gamma'  \vdash \bullet *\Gamma $" "(cut)"
\U "$\Gamma , \Gamma' \vdash $" "(dp)"
\epf
\qquad
\end{center}

We can then imitate the modified \Mp-proof with a
\dRA-proof using the variant \dRA\ rules.
This is done by translating every sequent of the intermediate form
of the table above to a corresponding sequent of the final form shown.
The proof steps in the two proofs
will correspond in the way that they use the cut-formulae;
so at corresponding stages of the two proofs the 
same cut-formula $\gamma$ will be present
(as $y[\gamma]w$ in the \Mp-proof, as $\gamma$ in the \dRA-proof).
For each step of the modified \Mp-proof which ``cuts'' on
$y[D]w$ and $y[*D]w$ we have a \dRA-proof step which ``cuts'' on 
$D$ and $*D$.
Likewise, for each step of the modified \Mp-proof which ``cuts'' on
$y[\bullet D]w$ and $y[\bullet *D]w$
we have a \dRA-proof step which ``cuts'' on 
$\bullet D$ and $\bullet *D$.

%If we put all the cut-formulae on the left like this, 
%the ones which were previously on the right will have a `$*$' preceding them;
%they actually need to be displayed on the right to be used as a premise in the
%\dRA\ (cut) rule.
%Note that although each $D_i$ need not be one of the cut-formulae,
%it is made up only of cut-formulae,
%with the operators `$\bullet$' and `,'; 
%this is because once all the 
%cut steps have been done, the resulting sequent has no formula of the form
%$y[R]w$.

Now, all the intermediate form 
sequents in the table above can be combined using the variant \Mp\ (cut) rules
on the terms $y[D_i]w$, with the result
$ x \mathcal A y, y \mathcal B z, x \mathcal C z,
  x \mathcal G w, w \mathcal H z \vdash $ ,
where
\vspace{-1.0ex}
\begin{itemize} \shrinklist{0.5}
\item[--]
$x \mathcal A y$ is an abbreviation for 
$x[A_1]y, x[A_2]y, x[A_3]y, x[A_5]y$, 
\item[--]
$y \mathcal B z$ is an abbreviation for 
$y[B_1]z, y[B_2]z, y[B_3]z, y[B_4]z$,
\end{itemize} 
\vspace{-1.0ex}
and so on. 
Translating this \M-sequent into \dRA\ gives
$ ((A; B), C), (G; H) \vdash I$,
where $A$ is $(((A_1, A_2), A_3), A_5)$ and 
$B$ is $(((B_1, B_2), B_3), B_4)$, and so on.

Note that if there is more than one \M-sequent of one of the five forms in the
table, say
$x[A_1']y, y[B_1']z, x[G_1']w, w[H_1']z , y[D_1']w \vdash$ 
and $x[A_1'']y, y[B_1'']z, x[G_1'']w, w[H_1'']z , y[D_1'']w \vdash$ ,
then the result of combining all the \M-sequents with cut will again be
$ x \mathcal A y, y \mathcal B z, x \mathcal C z,
  x \mathcal G w, w \mathcal H z \vdash $ , with 
$x \mathcal A y$ now abbreviating 
$x[A_1']y, x[A_1'']y, x[A_2]y, x[A_3]y, x[A_5]y$, and so on. 
If we let $A_1$ denote $(A_1', A_1'')$, then 
this also can be translated to
$ ((A; B), C), (G; H) \vdash I$
in \dRA\, 
where $A$ is $((A_1, A_2), A_3), A_5$, and so on, as before. 

If there one of the forms in the table
for which there is no \M-sequent 
(say the first), then set
$A_1 = B_1 = \cdots = \top$ in these results,
and use Lemmas \ref{lem:mtl} and \ref{lem:addT} to handle that case.
(Recall that $\bullet \top = \top$ and that $\top ; \top = \top$,
see \texttt{bIa} in \fig{bsr} and \ttdef{IIa} in \src{peirce.ML}.

The corresponding \dRA-sequents can be combined using (cut) in \dRA,
using steps which correspond to those used in the \Mp-proof,
%in the same order and in the same way,
to get a corresponding result.
%These sequents can be combined using (cut) in \dRA, 
%corresponding to the use of (cut) in the \Mp-proof.
The result will be of the form
%\begin{eqnarray}
%\nonumber
%\lefteqn
$$
{ \Big( \Big( \Big(  (\bullet A_1; G_1), (B_1; \bullet H_1) \Big),
 \Big( ((\bullet A_2; C_2), B_2); \bullet H_2 \Big)\Big),
 \Big( (\bullet A_3, (B_3; \bullet C_3)); G_3 \Big)\Big), }  
$$ \\[-6ex]
\begin{equation}
\label{eqml2}
 \Big( \Big( B_4; (\bullet H_4, (\bullet C_4; G_4)) \Big),
 \Big( \bullet A_5; (G_5, (C_5; \bullet H_5))\Big)\Big)
 \vdash I 
\end{equation}
This sequent has one conjunct of
each of the five forms in the table above.
In fact there may be more than one conjunct of each of the five forms.
Where there is more than one conjunct of one of the five forms,
for example 
$$ \Big(  \Big(  (\bullet A_1'; G_1'), (B_1'; \bullet H_1') \Big),
\Big(  (\bullet A_1''; G_1''), (B_1''; \bullet H_1'') \Big) \Big), Z 
 \vdash I $$
we use steps similar to those in the proof shown under case 1(a) above to get
$$\Big(  (\bullet A_1; G_1), (B_1; \bullet H_1) \Big), Z 
 \vdash I $$
where $A_1$ again denotes $(A_1', A_1'')$.
In this way we get a \dRA-sequent of the form of (\ref{eqml2}).

We then use the result, proved in Isabelle, 
that from (\ref{eqml2}) we can prove
$ ((A; B), C), (G; H) \vdash I$ in \dRA,
where $A$ is $((A_1, A_2), A_3), A_5$ and 
$B$ is $((B_1, B_2), B_3), B_4$ and so on.
A variant form of this result is proved as \ttdef{ml2}\label{ml2}
\insrc{Mad.ML}.

That is, we have proved, in \dRA, the 
\dRA-translation of conclusion of the \Mp-proof,
from the \dRA-translations of the premises of the \Mp-proof,
as required.
$\Box$
\renewcommand\cfile{}