\renewcommand\cfile{mim.tex}

\begin{thm} \label{mim} Given any \M-proof whose
whose premises $\mathcal P_i$ and conclusion $\mathcal C$
can be translated into \dRA,
there is a \dRA-proof
whose premises and conclusion are \dRA-translations of
$\mathcal P_i$ and $\mathcal C$.
\end{thm}

\proof\
By virtue of Theorem~\ref{mmp} we look instead at an \Mp-proof,
and by virtue of Theorem~\ref{pw} we look at an \Mp-proof $\mathcal T$ 
in which a monotonicity step precedes only a ($\circ \vdash$)-step 
or another monotonicity step,
or is at the end of the proof.

We show that each step in the \Mp-proof
can be mimicked by a corresponding step in a \dRA-proof,
except where an intermediate \M-sequent 
cannot be translated into \dRA.
In this case we will have to look at a portion of the
\Mp-proof tree, where the premises and conclusion of that portion
can be translated into \dRA, 
although the intermediate sequents in that portion cannot.

We need to rearrange the \Mp-proof tree $\mathcal T$
to minimize the size of those portions.
We repeatedly apply the following transformation to $\mathcal T$,
wherever possible:
\begin{quote}
for any internally-$K_4^*$ sub-tree of $\mathcal T$
which consists of cuts,
use Lemmas \ref{lem:reoc} and \ref{lem:scuts} 
to replace the sub-tree by another proof tree consisting of cuts
(with maybe monotonicity steps at the end),
all of whose internally-$K_4^*$ parts use fewer distinct cut-formulae.
\end{quote}

Each application of this transformation reduces the number of
internally-$K_4^*$ sub-trees with $n$ distinct cut-formulae
(although at the expense of increasing arbitrarily the number of
internally-$K_4^*$ sub-trees with at most $n-1$ distinct cut-formulae,
and of increasing the size of the proof tree).
Repeated application of this procedure will therefore eventually terminate,
giving a proof tree $\mathcal T'$.

We now prove the theorem, for the rearranged proof tree 
$\mathcal T'$, by induction on the number of steps in it.

\textbf{Base case :} The base case of the induction is where $\mathcal T'$ is
a proof of length~1, that is, an axiom of \Mp.

We show that all the axioms of \Mp\ can be translated into theorems 
(provable sequents) of \dRA.
\tbl{axtr} shows the axioms of \Mp\ and their translations into \dRA.

\begin{table}[htbp]
\begin{center}
\begin{tabular}{c@{\hspace{10mm}}c}
\Mp-axioms & \dRA\ equivalents \\[1.0ex]
$ {x[R]y \vdash x[R]y} $ & $R, *R \vdash I $ \\
$ {x[\bot] y \vdash } $ & $ \bot \vdash I $ \\
$ {\vdash x[\top] y} $ & $ *\top \vdash I $ \\
$ {\vdash x[\1]x} $ & $ *\1, \1 \vdash I $ \\
{ $ x[R]z, z[\1]y \vdash x[R]y $ }  & $ (R;\1), *R \vdash I $ \\
 $ x [\lnot R]y, x[R]y \vdash$ & $\lnot R, R \vdash I $ \\ 
 $ \vdash x[R]y, x [\lnot R]y$ & $*R, * \lnot R \vdash I $ \\ 
$ y [\smile R]x \vdash x[R]y$   & $ \smile R, \bullet *R \vdash I $ \\
$ x[R]y \vdash y [\smile R]x$   & $ R, \bullet *\smile R \vdash I $ \\
$ x[R \lor S]y \vdash x[R]y, x[S]y$  & $ R \lor S, *R, *S \vdash I $ \\
$ x[R]y \vdash x[R \lor S]y$  & $ R, *(R \lor S) \vdash I $ \\
$ x[S]y \vdash x[R \lor S]y$   & $ S, *(R \lor S) \vdash I $ \\
$ x[R \land S]y\vdash x[R]y $  & $ R \land S, *R \vdash I $ \\
$ x[R \land S]y\vdash x[S]y $  & $ R \land S, *S \vdash I $ \\
$ x[R]y, x[S]y\vdash x[R \land S]y $ & $ R, S, *(R \land S) \vdash I $ \\
$ x[R]y, y[S]z\vdash x[R \circ S]z $ & $ (R;S), *(R \circ S) \vdash I $ \\
\end{tabular}
\end{center}
\caption{\Mp-axioms and their \dRA\ equivalents}
\label{tbl:axtr}
\end{table}

The results in the right-hand column have all been proved in \dRA\
using Isabelle, as
\ttdef{max}, \ttdef{m11}, \ttdef{mR1} and
\ttdef{mRS} \insrc{thmisc.ML}.
These translations are not unique, but Theorem~\ref{eqtrthm} shows
that any other translation is equivalent in \dRA, and therefore is 
provable in \dRA.

We note, however, that the \dRA-translations are different
from the above if two of the
point variables are the same,
but they are still theorems of \dRA.
For example,
$ x[R]y, y[S]y\vdash x[R \circ S]y $ 
(the last one in the table above, with $z=y$)
translates not to $ (R;S), *(R \circ S) \vdash I $ 
but to $ (R;(S,1)), *(R \circ S) \vdash I $.
However this second sequent is also a theorem of \dRA;
it follows from the first
by the \dRA\ monotonicity rule
($M \vdash$) and the display postulates.

\textbf{Inductive step :}
We consider an \M-proof tree $\mathcal T'$,
and assume that any \M-proof tree with fewer steps can be mimicked in \dRA.

We break up the \M-proof into steps, or in some cases 
a combination of steps considered as a unit,
and turn each of these portions into a proof in \dRA.
By virtue of Theorem~\ref{eqtrthm}, which showed that any
two \dRA-translations of an \M-sequent are equivalent
(inter-derivable) in \dRA,
we can turn each step (or combination of steps)
of the \Mp-proof into \dRA\ independently.
That is, let 
$M_i$ be \M-sequents, and $D_i',D_i''$ be \dRA-translations of
$M_i$, and suppose we are trying to mimic an \Mp-proof 
$M_1 \Longrightarrow M_2 \Longrightarrow M_3$.
Then it is sufficient to show that
$D_1' \Longrightarrow D_2'$ and 
$D_2'' \Longrightarrow D_3''$ in \dRA,
for Theorem~\ref{eqtrthm} gives us  
$D_2' \iff D_2''$.
(This example supposes that the two steps or portions of the \M-proof
both have just one premise; the argument is similar for more or fewer
premises).

An \M-proof tree $\mathcal T'$
that is longer than a single axiom must contain an 
instance $\rho$ of an inference rule,
so next we look at the inference rules of \Mp.
We will show that $\rho$, or some portion $\mathcal R$
of $\mathcal T'$ containing $\rho$, can be mimicked in \dRA;
deleting $\rho$ or $\mathcal R$ from $\mathcal T'$ will leave one or more
separate proof trees $\mathcal T' _i$.
Each $\mathcal T' _i$ has fewer steps than $\mathcal T'$.
Therefore, by the induction hypothesis,
each $\mathcal T' _i$ can be mimicked in \dRA\ also.
When we put these \dRA-proofs together
(using Theorem~\ref{eqtrthm}, as described in the last paragraph,
where necessary),
we will have a \dRA-proof mimicking $\mathcal T'$.

We now consider all the inference rules of \Mp;
we intend to show that, for each instance $\rho$ of a rule, 
either $\rho$ or a suitably chosen $\mathcal R$ containing $\rho$
can be mimicked in \dRA.

{\bfseries \boldmath ($\circ \vdash $):} 
if an instance $\rho$ of the ($\circ \vdash $) rule is
${\Gamma, x[R]y, y[S]z \vdash \Delta} \Longrightarrow
{\Gamma, x[R \circ S]z \vdash \Delta}$,
then the condition that
$y$ cannot appear in $\Gamma$ or $\Delta$
is precisely the condition needed for using step
\ref{Mst;} to translate the premise to 
$\Gamma, x[R;S]z \vdash \Delta$.
After the rest of the translation into \dRA,
using similar steps for both premise and conclusion,
we have 
$X[R;S] \vdash I \Longrightarrow X[R \circ S] \vdash I $.
(Here the meaning of $X[\cdot]$ is that $Q$ appears in $X[Q]$
in the same positions that $P$ appears in $X[P]$).
Since $x[R;S]z $ and $x[R \circ S]z $  were in an antecedent position, 
it can be seen that 
$R;S$ and $R \circ S $ are in an antecedent position
in the \dRA-sequents, and so
we can derive 
$X[R;S] \vdash I \Longrightarrow X[R \circ S] \vdash I $
in \dRA\ by displaying $R \circ S$, 
using the ($\circ \vdash $) rule and undisplaying.
%from the ($\circ \vdash $) rule and some display postulates.

We also note here that the condition on $y$ for this rule 
requires that vertex $y$ in the graph of the premise has degree 2,
and that vertex $y$ is absent from the graph of the conclusion.
This implies that neither graph is a $K_4^*$-graph.

{\bfseries \boldmath ($M \vdash $),($\vdash M $):} 
Consider next a sequence of steps using the monotonicity rule.
If it is immediately followed by a 
($\circ \vdash$)-step then the conclusion
of the sequence has a point variable appearing exactly twice,
so the corresponding graph has a vertex of degree~2,
and cannot be $K_4$.
Otherwise the sequence 
is at the end of the proof, and we have assumed that the premises and
conclusion of the proof can be translated.
In either case it follows that
the conclusion of the sequence can be translated into \dRA.

Clearly, if the conclusion of a ($M \vdash $) or ($\vdash M $) step
can be translated into \dRA, then so can its premise.
Thus each sequent in the sequence 
of ($M \vdash $) or ($\vdash M $) steps 
can be translated into \dRA.

Suppose the instance $\rho$ of the monotonicity rule 
$(M \vdash)$ is
$
{\Gamma \vdash \Delta} \Longrightarrow
{\Gamma, \Gamma' \vdash \Delta} 
$ in \Mp.
Let $\Gamma''$ be $\Gamma'$ with each formula $x[R]y$ changed to $x [\top] y$.
Then, by \lem{mtl}, 
${\Gamma \vdash \Delta} \iff {\Gamma, \Gamma'' \vdash \Delta} $.

Suppose that 
${\Gamma, \Gamma' \vdash \Delta} $
can be translated to $X' \vdash I$ in \dRA.
Then suppose
${\Gamma, \Gamma'' \vdash \Delta} $ is translated into \dRA\ using
corresponding steps, with the result \mbox{$X'' \vdash I$.}
So for every formula $R$ in $X'$ that originates from 
some $x[R]y$ in $\Gamma'$,
there is $\top$ in a corresponding antecedent position in $X''$.
%Consider ${\Gamma, \Gamma'' \vdash \Delta} $
%translated into \dRA\ using steps corresponding to those used in 
%translating
%${\Gamma, \Gamma' \vdash \Delta} $.
To derive $X' \vdash I$ from $X'' \vdash I$ in \dRA, 
we use the proof step which changes any occurrence 
of $\top$, in an antecedent position, to anything else we choose.
That is done using the display postulates, cutting with ($I \vdash \top$),
and using the rule (VerI).

%{\bfseries \boldmath ($\vdash M $):} 
The case of the other monotonicity rule 
$(\vdash M )$ is similar, except that we need a variant of 
\lem{mtl} for adding $x [\bot] y$ on the right,
and we use the \dRA\ rules ($\bot \vdash $) and (ExI)
to change $\bot$ on the right to anything else.

{\bfseries \boldmath (cut):} 
There are several cases here.  We handle the simpler one first.

\textbf{Case 1:}
Assume that the premises and conclusion of the cut $\rho$
can each be translated into 
\dRA, ie, none of them is a $K_4^*$-sequent.
That is, each of the premises and conclusion 
is an \M-sequent which has a missing pair of point variables.
%such that no formula in the \M-sequent uses that pair.
There are two cases, depending on whether or not there is \emph{one} pair
which is a missing pair for \emph{all} the premises and conclusion.
%such that no formula in any of the \M-sequents uses that pair.

\textbf{Case 1(a):}
Assume that there is a pair of point variables, say $(y,w)$,
that is a missing pair for all of the premises and the conclusion.
Suppose, by way of example, that the cut-formula is $x[D]z$.
Let us partly translate the premises 
using steps \ref{Mstmv}, \ref{Mstbl}, 
\ref{Mst,}, \ref{Mst;'} and \ref{Mst;`},
to get (assuming that the four point variables are $x,y,z,w$)
$$x[A']y, y[B']z, x[C']z, x[G']w, w[H']z, x[*D]z \vdash$$
and
$$x[A'']y, y[B'']z, x[C'']z, x[G'']w, w[H'']z, x[D]z \vdash $$

Note that, in the translation, where there are formulae of the form
$x[R]x$ or $z[R]z$, we assume that the translation steps are
chosen to avoid using one of the cut formulae
in steps \ref{Mst;'} or \ref{Mst;`}.
That is, we would, for example, translate
$w[J]x, x[R]x, x[D]z$ to $w[J; (R,1)]x, x[D]z$ and \emph{not} to
$w[J]x, x[(R,1); D]z$.
Note also that it may be necessary
to add a formula such as $x \top y$,
by virtue of \lem{mtl}, to enable the translation into \dRA,
as described below.

Alternatively, the cut-formula could use point variables other than
$(x,z)$, say $x[D]y$ or $x[D]w$, for example.
The argument is similar to the above, and in each case we have that
the conclusion of the cut then can be partly translated to
$$x[A',A'']y, y[B',B'']z, x[C',C'']z, x[G',G'']w, w[H',H'']z \vdash $$
Then the premises can be further translated to 
$$\Big(((A';B'), C'), (G';H')\Big), *D \vdash I 
\qquad \textrm{and} \qquad
\Big(((A'';B''), C''), (G'';H'')\Big), D \vdash I$$
and the conclusion to 
$$\Big(\Big((A',A'');(B',B'')\Big), (C',C'')\Big),
  \Big((G',G'');(H',H'')\Big)\vdash I$$

The \dRA-proof of the translation of the conclusion from the translations of
the premises then proceeds as in \fig{1(a)}.

\begin{figure}[htbp]
\vpf
\begin{center}
\bpf
\A "$\Big(((A';B'), C'), (G';H')\Big), *D \vdash I $"
\U "$((A';B'), C'), (G';H') \vdash D$" "(dp)"
\A "$\Big(((A'';B''), C''), (G'';H'')\Big), D \vdash I$"
\U "$D \vdash *\Big(((A'';B''), C''), (G'';H'')\Big), I$" "(dp)"
\B [1em] "$((A';B'), C'), (G';H') \vdash
  *\Big(((A'';B''), C''), (G'';H'')\Big), I$" "(cut)"
\U "$\Big(((A'';B''), C''), (G'';H'')\Big),
  \Big(((A';B'), C'), (G';H')\Big) \vdash I$" "(dp)"
\U "repeated dps and monotonicity"
\U "\begin{tabular}{c}
  $\bigg(\Big(\Big((A',A'');(B',B'')\Big), (C',C'')\Big),
    \Big((G',G'');(H',H'')\Big)\bigg), $
  \hspace{4em} \\ \hspace{13em}
  $\Big(((A';B'), C'), (G';H')\Big) \vdash I$
  \end{tabular}"
\U "repeated dps and monotonicity"
\U "\begin{tabular}{c}
  $\bigg(\Big(\Big((A',A'');(B',B'')\Big), (C',C'')\Big),
    \Big((G',G'');(H',H'')\Big)\bigg), $
  \hspace{4em} \\ \hspace{2em}
  $\bigg(\Big(\Big((A',A'');(B',B'')\Big), (C',C'')\Big),
    \Big((G',G'');(H',H'')\Big)\bigg) \vdash I$
  \end{tabular}"
\U "$\Big(\Big((A',A'');(B',B'')\Big), (C',C'')\Big),
  \Big((G',G'');(H',H'')\Big)\vdash I$" "($C \vdash $)"
\epf
\end{center}
\caption{\dRA-proof for Case 1(a)}
\label{fig:1(a)}
\end{figure}
%The conclusion of this \dRA-proof is a translation of the 
%conclusion of (cut) in the \Mp-proof.

By way of explanation, in the two steps labelled
``repeated dps and monotonicity" in \fig{1(a)}, 
$A''$ is converted to $(A',A'')$ by displaying it and applying
monotonicity, in the first of the two; 
similarly $A'$ is converted to $(A',A'')$ in the second.
This is done simply to set up the final contraction ($C \vdash $) step.

\textbf{Case 1(b):}
As before, for each of the premises and conclusion 
there is a missing pair of point variables.
Assume now that this is not the \emph{same} pair for each of 
the premises and conclusion,
ie, for every pair of point variables
either one of the premises or the conclusion of the cut $\rho$
has a formula using that pair of point variables.
This is in fact a special case of proof tree of the form 
dealt with in \lem{case2} because
\begin{itemize} \shrinklist{0.5}
\item[--] there is only one cut 
(so all the cut-formulae are on the same pair of point variables)
\item[--] there are no intermediate proof states 
(so all the intermediate sequents are $K_4^*$-sequents)
\item[--] the missing pair of point variables
for the conclusion is not a missing pair
for both the premises, so it must be the pair used by the cut-formula
\end{itemize}
Therefore, by \lem{case2}, we can prove, in \dRA, the 
\dRA-translation of conclusion of the (cut)
from the \dRA-translations of its premises.

\textbf{Case 2:}  A premise or the conclusion of the 
instance $\rho$ of (cut) is a $K_4^*$-sequent.
We therefore have to look at a portion of the proof tree,
containing $\rho$, that is larger than just one step.

We look for a minimal sub-tree $\mathcal T''$ of $\mathcal T'$ of which the 
premises and conclusion can be translated into \dRA,
that is, an internally-$K_4^*$ sub-tree,
such that $\mathcal T''$ contains the given instance $\rho$ of (cut).
We know such a tree exists since by hypothesis the conclusion of
$\mathcal T'$ can be translated, as can the premises.
Now the graph of the premise of ($\circ \vdash $)
has a vertex of degree~2, which is removed by the rule, so
the graph of the conclusion of ($\circ \vdash $) has (at most) three vertices;
we know that graphs with at most three vertices can be translated.
Therefore this internally-$K_4^*$ sub-tree $\mathcal T''$
cannot contain any use of the ($\circ \vdash $) rule.
It also does not contain any monotonicity step, because (as noted above)
the conclusion of a monotonicity step can be translated into \dRA,
ie it is not a $K_4^*$-sequent.
It therefore contains only instances of (cut).

We therefore have a proof tree $\mathcal T''$ consisting wholly of cuts, 
which is internally-$K_4^*$, ie, whose
intermediate sequents are $K_4^*$-sequents,
but whose premises and conclusion are not.
Now the process of rearranging $\mathcal T$ to give $\mathcal T'$
minimized the set
of cut-formula appearing in any internally-$K_4^*$ sub-tree of the proof tree.
Therefore, by Theorem~\ref{allcuts}, 
%for any internally-$K_4^*$ sub-tree of the proof tree,
all the cuts in $\mathcal T''$
are on formulae which use the same pair of point variables,
say $\{x,y\}$.
Then $\{x,y\}$ is the only pair missing from the conclusion, 
since any other pair missing from the conclusion
is missing from $\mathcal T''$ entirely;
but as $\mathcal T''$ contains $\rho$,
we know that it contains a $K_4^*$-sequent.
%We need to mimick a proof tree of this form,
%ie, consisting entirely of cuts on formulae which use the same pair of point
%variables, in \dRA.
By \lem{case2} we can mimic this proof tree in \dRA;  
that is we can prove, in \dRA, the 
\dRA-translation of conclusion of the \Mp-proof
from the \dRA-translations of the premises of the \Mp-proof.

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

\renewcommand\cfile{}