\subsection{Equivalence of multiset and consecution calculi}

The second paper, Bimbo and Dunn,
On the dedidability of implicational ticket entailment
FIND CITATION

introduces transformations $\pi$ and $\tau$ between the logics 
$\lrarrow$ and $\ltarrowtcircstr$ 

Now when we do a shallow embedding of proofs, we do not actually have a proof
object on which we can define such a function, or prove properties about it
such as Lemma 6, or that $\pi$ and $\tau$ are (in some sense) inverse.

However we proved Lemma 4 to the extent that we proved that,
given a sequent provable in $\ltarrowtcircstr$,
when we turn the structure in its antecedent into a multiset of formulae,
the resulting sequent is provable in $\lrarrow$, 
and the method of our proof followed the definition of $\pi$ in the paper.

We use some auxiliary functions:

\begin{verbatim}
consts
  ms_of_str :: "'f structr => 'f multiset"
  ap_ant :: "('a => 'b) => ('a, 'c) sequent => ('b, 'c) sequent"
  ap_psc :: "('a => 'b) => 'a psc => 'b psc"
\end{verbatim}

\texttt{ms\_of\_str} turns a structure into a multiset. \\
\texttt{ap\_ant} applies a function to the antecedent of a sequent. \\
\texttt{ap\_psc} applies a to each premise and to the conclusion of a rule.

\begin{lemma}
For each rule in $\ltarrowtcircstr$,
when we turn the consecutions into multisets, we get
a rule derivable in $\lrarrow$.
\end{lemma}
\begin{verbatim}
pi_lem ;
    "(?ps, ?c) : LTitc ==> ap_psc (ap_ant ms_of_str) (?ps, ?c) : derl LRit"
\end{verbatim}

We extend this to the result that any derived rule of
$\ltarrowtcircstr$, translated, is a derived rule of $\lrarrow$.

Since \texttt{derl}, which gives the derived rules of a system,
gives the shape of rules
(ie, premises in a particular order, and no extraneous premises - the
premises are the leaves of an actual proof tree), this says something about 
the similarity between proof trees in the two systems, 
more than \texttt{pi\_der}, which says simply that a provable sequent in
$\ltarrowtcircstr$ is a provable sequent in $\lrarrow$.

(I was going to write theorem for provable sequent,
but that raises the issue that A is a theorem if t |- A is a provable sequent)

\begin{verbatim}
pi ;
   "(?ps, ?c) : derl LTitc
         ==> ap_psc (ap_ant ms_of_str) (?ps, ?c) : derl LRit"

pi_der =
   "(?a |- ?c) : derrec LTitc {} ==> (ms_of_str ?a |- ?c) : derrec LRit {}":
\end{verbatim}
     
The tau translation.
I only got as far as proving Lemmas 8 to 10.

Since the proofs shown on page 226 consist of a sequence of single-premise
rules, and our functions sctxt and lctxt operate on pairs of structures rather
than rules, and we have defined the relevant rules 
(eg \texttt{lcB}, \texttt{lcW}, etc)
as sets of pairs,
we expressed our results in terms of the transitive closure of the
set of rules.

We needed lemmas to translate this notion to that of derived rules:

\begin{verbatim}
 lctxt_sctxt_rtc ;
  "lctxt ((sctxt ?r)^*) <= derl (lctxt ?r)"
\end{verbatim}
 
Here, you compose a sequence of rules, expressed as pairs of antecedent
structures (where each rule individually may be augmented by some context),
and then turn the result into a rule in the usual form (list of premises and
conclusion).  The theorem says that the result is derivable from 
lctxt of the set of pairs used.

So now we look at proving Lemmas 8 to 10 in terms of transitive closure.

This is the proof of Lemma 8 up to the penultimate line.
\begin{verbatim}
t_BA = "(?A; ?B, Sf T; (?B; ?A)) : (sctxt LTitc_lc)^*"
\end{verbatim}

When we instantiate A and B in \texttt{t\_BA} to A;B and C, to get
\begin{verbatim}
t_C_AB = "(?A; ?B; ?C, Sf T; (?C; (?A; ?B))) : (sctxt LTitc_lc)^*"
\end{verbatim}

and apply rules \strbleft\ or \strbpleft\ we get 
\begin{verbatim}
 t_CAB = "(?A; ?B; ?C, Sf T; (?C; ?A; ?B)) : (sctxt LTitc_lc)^*"
 t_ACB = "(?A; ?B; ?C, Sf T; (?A; ?C; ?B)) : (sctxt LTitc_lc)^*"
\end{verbatim}

Of the four ways of composing these two,
\texttt{t\_ACB} then \texttt{t\_ACB} gives the identity,
the other three give three more permutations of ?A ?B ?C in
\begin{verbatim}
"(?A; ?B; ?C, Sf T; (x; y; z)) : (sctxt LTitc_lc)^*"
\end{verbatim}

The sixth permutation is the identity, in
\begin{verbatim}
"(?A; ?B; ?C, Sf T; (?A; ?B; ?C)) : (sctxt LTitc_lc)^*"
\end{verbatim}
which is given simply by \strkitleft.

The other six case of Lemma 10 are got by taking these six results
and then applying \texttt{t\_BA} (with left context $\verum$).
This give two instances of $\verum$ at the left,
which we can reduce to one, looking like

\begin{center}
\begin{prooftree}
\AxiomC{A; B; C}
\RightLabel{}
\UnaryInfC{$\verum$; ($x$; $y$; $z$)}
\RightLabel{t\_BA}
\UnaryInfC{$\verum$; ($\verum$ ; ($z$; ($x$; $y$)))}
\RightLabel{\strbleft}
\UnaryInfC{$\verum$; $\verum$ ; ($z$; ($x$; $y$))}
\RightLabel{\strmtleft}
\UnaryInfC{$\verum$ ; ($z$; ($x$; $y$))}
\end{prooftree}
\end{center}

Thus we get the other six cases of Lemma 10.

Composing these last six with \strbleft\ we get

\begin{center}
\begin{prooftree}
\AxiomC{$\verum$ ; ($z$; ($x$; $y$))}
\RightLabel{\strbleft}
\UnaryInfC{$\verum$ ; $z$ ; ($x$; $y$)}
\end{prooftree}
\end{center}

and composing these with \strbleft\ we get 

\begin{center}
\begin{prooftree}
\AxiomC{$\verum$ ; $z$ ; ($x$; $y$)}
\RightLabel{\strbleft}
\UnaryInfC{$\verum$ ; $z$ ; $x$; $y$}
\end{prooftree}
\end{center}

giving the twelve cases of Lemma 9.

(As I understand Lemmas 9 and 10 - in fact I find the statement of Lemma 10
unclear, but an helped by the statement that it has 12 cases).
Since I was able to prove Lemma 10 first and then use it to prove Lemma 9,
clearly I didn't do it the same way they did.

