work done to Wed Apr 26 on cut admissibility for logics in
Bimbo and Dunn, New Consecution Calculi for Implicational Rt
general stuff defining the logics (file bddefs.thy)
datatype ('l, 'r) sequent = Sequent "'l" "'r"
("((_)/ |- (_))" [6,6] 5)
datatype formula = Bimp formula formula ("_ -> _" [61,61] 60)
| T
| FV string (* formula variable *)
| PP string (* primitive proposition *)
datatype 'f structr = SemiC "'f structr" "'f structr" ("_; _" [20,21] 20)
| Sf 'f
consts
ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
intrs
ipsL "(P, P -> Q) : ipsubfml"
ipsR "(P, Q -> P) : ipsubfml"
consts
iid_rls, lctr_rls, impL, sbimpL, impR, tL, tR,
LRi, LRit, LRisb, LRitsb :: "(formula multiset, formula) sequent psc set"
sqbr :: "'a => 'a multiset => 'a multiset set"
(* sqbr - square brackets, defined near bottom of pg 497 of
Bimbo and Dunn, New Consecution Calculi for Implicational Rt. *)
inductive "sqbr dist fmls"
intrs
I "cms <= mins dist fmls ==>
set_of (mins dist fmls) = set_of cms ==>
ALL fml. count fmls fml <= Suc (count cms fml) ==>
cms : sqbr dist fmls"
inductive "impL"
intrs
I "([alpha |- A, mins B beta |- C],
mins (A -> B) alpha + beta |- C) : impL"
inductive "sbimpL"
intrs
I "cms : sqbr (A -> B) (alpha + beta) ==>
([alpha |- A, mins B beta |- C], cms |- C) : sbimpL"
other rules omitted
inductive "LRi"
intrs
id "psc : iid_rls ==> psc : LRi"
impL "psc : impL ==> psc : LRi"
impR "psc : impR ==> psc : LRi"
W "psc : lctr_rls ==> psc : LRi"
LRit, LRisb, LRitsb omitted
framework for proofs of cut admissibility
uses gen_step2 (slightly different from gen_step2sr previously)
"gen_step2 ?P ?A ?sub (dls, drs) ((psl, cl), (psr, cr)) =
(ALL A'. (A', ?A) : ?sub -->
(ALL dl:dls. ALL dr:drs. ?P A' (dl, dr))) -->
(ALL pl:set psl. pl : dls & ?P ?A (pl, cr)) -->
(ALL pr:set psr. pr : drs & ?P ?A (cl, pr)) -->
cl : dls --> cr : drs --> ?P ?A (cl, cr))"
This is for proving a property of two sequents, eg, that
cut-admissibility of a particular formula ?A holds between them.
dls and drs will usually be the set of derivable sequents.
Where the property P of formula A is cut admissibility on A,
this allows an induction scheme where you can assume
(1) cut admissibility holds in respect of a smaller cut-formula A'
(2) cut admissibility holds between the sequent on the right and
the preceding sequents in the derivation on the left
(3) cut admissibility holds between the sequent on the left and
the preceding sequents in the derivation on the right
gen_step2_lem:
"[| ?A : wfp ?sub;
ALL A. ALL (psa, ca):?rlsa. ALL (psb, cb):?rlsb.
gen_step2 ?P A ?sub (derrec ?rlsa {}, derrec ?rlsb {})
((psa, ca), psb, cb)
?seqa : derrec ?rlsa {}; ?seqb : derrec ?rlsb {} |] ==>
?P ?A (?seqa, ?seqb)"
This says that if seqa and seqb are derivable, and gen_step2 P holds generally,
then P A holds between seqa and seqb.
$LR_\to$ and $LR^t_\to$ (file LRica.ML)
$LR^t_\to$ is a slight extension of $LR_\to$.
Now when admissibility of cut, or anything else, holds of a logic, it
does not necessarily hold of any containing logic.
However it is noteworthy that each step of the proof of cut-admissibility for
$LR_\to$ is mimicked in $LR^t_\to$, with $LR^t_\to$ requiring extra steps only
for the extra rules contained in $LR^t_\to$.
Now proving cut-admissibility requires us to prove gen_step2 P
for each possibility of the last rules used in proving the premises of the
proposed cut
We can express these results like this, in a way which allows them to be used
for any containing logic.
gsm_impR_R ;
"impR <= ?rls
==> gen_step2 (mcd ?rls) ?A ?any (?drsl, derrec ?rls {})
((?psl, ?cl), [mins ?G ?alpha |- ?H], ?alpha |- ?G -> ?H)"
This says that if the rule set contains the ($\vdash\to$) rule,
and the rule on the right is an instance of the ($\vdash\to$),
then gen_step2 P holds. Notice that in this case it doesn't matter how
the left premise cl is derived, just that (as contained in the definition of
gen_step2) cut-admissibility (in the sense of mcd, not mcd, see below)
holds between it and the premises psr of the final
rule on the right.
The form of this result allows it to be used as one of the cases for any
logic containing the ($\vdash\to$) rule.
The most difficult of these results were
gsm_impL_R_ne;
"[| impL <= ?rls; All (lctr_adm ?rls); ?Lc ~= ?Ab -> ?Bb |]
==> gen_step2 (mcd ?rls) ?A ?any (?drsl, derrec ?rls {})
((?psl, ?D |- ?Lc), [?F |- ?Ab, mins ?Bb ?G |- ?C],
mins (?Ab -> ?Bb) ?F + ?G |- ?C)"
($\to\vdash$) on the right, where the principal formula is not the cut-formula,
and
gsm_imp_C8 ;
"All (lctr_adm ?rls)
==> gen_step2 (mcd ?rls) ?cf ipsubfml (derrec ?rls {}, derrec ?rls {})
(([mins ?A ?D |- ?B], ?D |- ?A -> ?B), [?F |- ?A, mins ?B ?G |- ?C],
mins (?A -> ?B) ?F + ?G |- ?C)"
where the cut-formula is an implication which is principal on both sides.
The form of the theorem proved gives a clue as to which part of the inductive
hypothesis is used: for example, the third argument of gen_step is either ?any
or ipsubfml depending on whether or not cut-admissibility for subformulae
needs to be assumed.
Our property P we prove of a pair of derivable sequents is mcd ?rls
mcd ;
"mcd ?rls ?A (?cl, ?cr) =
(ALL Xl Xr n B.
?cl = (Xl |- ?A) & ?cr = (Xr + times (Suc n) {#?A#} |- B) -->
(Xl + Xr |- B) : derrec ?rls {})"
that is, that the result of multi-cutting cl and cr on cut-formula A is
derivable.
Using multicut instead of cut as the property we prove inductively
removes the difficulty caused by the contraction rule.
Using all the cases we proved
mca_LRi ;
"mca LRi ?A (?cl, ?cr)"
mca is like mcd but assuming that cl and cr are themselves derivable
mca;
"mca ?rls ?A (?cl, ?cr) =
(?cl : derrec ?rls {} -->
?cr : derrec ?rls {} --> mcd ?rls ?A (?cl, ?cr))"
Now it is not difficult to extend this result to $LR^t_\to$,
as it is necessarily to prove only a few more simple cases of
gen_step2, involving the new ($t\vdash$) and ($\vdash t$).
Thm 2.2
mca_LRit ; "mca LRit ?A (?cl, ?cr)"
$[LR_\to]$ and $[LR^t_\to]$ (file LRisbcca.ML)
These calculi modify $LR_\to$ and $LR^t_\to$ by deleting the
contraction rule, but modifying the ($\to\vdash$) rule to allow a limited
amount of contraction to follow ($\to\vdash$), calling the new rule
($[\to\vdash]$).
Bimbo & Dunn (Theorem 2.4) state that the cut rule is admissible,
by a proof similar to that for $LR^t_\to$ (Theorem 2.2).
I couldn't prove the result in this way (account of the problem
on handwritten docs), but I could prove contraction admissibility.
This was by a technique similar to that for cut-admissibility, but simpler, as
it is a property of one sequent, not two.
lca_LRisb ; "lca LRisb ?A ?c"
lca_LRitsb ; "lca LRitsb ?A ?c"
where lca is defined by
lca;
"lca ?rls ?A ?c == ?c : derrec ?rls {} --> lcd ?rls ?A ?c"
lcd;
"lcd ?rls ?A ?c == ALL X B.
?c = (X + {#?A#} + {#?A#} |- B) -->
(X + {#?A#} |- B) : derrec ?rls {}"
Having proved contraction admissibility for LRisb and LRitsb,
we prove that the rules of LRi are admissible in LRisb and
the rules of LRisb are derivable in LRi, whence these systems are equivalent
LRi_LRisb ; "LRi <= adm LRisb"
LRisb_LRi ; "LRisb <= derl LRi"
LRisb_eqv_LRi ; "derrec LRisb {} = derrec LRi {}"
Similarly for the versions with 't'. This gives part of Lemma 2.5
From this we get cut-admissibility, Theorem 2.4
mca_LRisb ; "mca LRisb ?A (?cl, ?cr)"
mca_LRitsb ; "mca LRitsb ?A (?cl, ?cr)"
The consecution calculi $LT^t_\to$ $LR^t_{\to;}$ $LT^{\textcircled{t}}_\to$
(file LTitca.ML)
consts
sctxt :: "'f structr relation trf"
lctxt :: "'f structr relation => ('f structr, 'f) sequent psc set"
lcimpR, lcimpL, LTit, LRitsc, LTitc ::
"(formula structr, formula) sequent psc set"
lcid :: "('f structr, 'f) sequent psc set"
LTit_lcsub, LTit_lc, lcC :: "'f structr relation"
KIt, Kt, Tt :: "'f => 'f structr relation"
To illustrate sctxt and lctxt,
in the terms of the rules in the paper (eg (B|-)),
C[B; (C; D)], C[B; C; D]) \in sctxt ({(B; (C; D), B; C; D)})
and (C[B; (C; D)] |- E, C[B; C; D] |- E) \in lctxt ({(B; (C; D), B; C; D)})
sctxt
inductive "sctxt r" (* closure of rule structure relation under context *)
intrs
scL "(a, b) : sctxt r ==> (C;a, C;b) : sctxt r"
scR "(a, b) : sctxt r ==> (a;C, b;C) : sctxt r"
scid "(a, b) : r ==> (a, b) : sctxt r"
inductive "lctxt r"
intrs
I "(As, Bs) : sctxt r ==> ([As |- E], Bs |- E) : lctxt r"
Note that sctxt R = \bigunion_{p \in R} sctxt p
and similarly lctxt (not true of strrep, below, but in fact we only every
use strrep for singleton sets)
(* rules in LTit which involve context on the left (deep structural rules) *)
LTit_lcsub are the pairs (X, Y) which form rules of the form
(below, under LTit_lc)
where X and Y consist only of substitutable structure variables
(ie unlike the rules involving t)
inductive "LTit_lcsub" (* fully substitutable rules *)
intrs
B "(Bs; (Cs; Ds), Bs; Cs; Ds) : LTit_lcsub"
Bd "(Bs; (Cs; Ds), Cs; Bs; Ds) : LTit_lcsub"
W "(Bs; Cs; Cs, Bs; Cs) : LTit_lcsub"
inductive "lcC" (* another fully substitutable rule *)
intrs
I "(Bs; Cs; Ds, Bs; Ds; Cs) : lcC"
LTit_lc are the pairs (X, Y) which form rules in LTit of the form
C[X] |- E
---------
C[Y] |- E
inductive "LTit_lc"
intrs
sub "psc : LTit_lcsub ==> psc : LTit_lc"
KIt "psc : KIt T ==> psc : LTit_lc"
Mt "(Sf T; Sf T, Sf T) : LTit_lc"
inductive "LTit"
intrs
id "psc : lcid ==> psc : LTit"
impR "psc : lcimpR ==> psc : LTit"
impL "psc : lcimpL ==> psc : LTit"
lcrules "psc : lctxt LTit_lc ==> psc : LTit"
definitions of lcid, lcimpR, lcimpL omitted
LRitsc, LTitc omitted
Most of the rules of these calculi are expressed as "deep inference" rules,
where the antecedent of the conclusion is a structure which
has a substructure which is altered, giving a corresponding structure
which becomes the antecedent of one of the premises.
We express this using the inductively defined set function sctxt.
Since these calculi have a contraction rule we want to use something like the
approach described for the multiset-sequent systems, where we showed
admissibility of multicut rather than cut.
However we couldn't work out exactly what that should mean in this context.
In fact we found a similar solution: given sequents X |- A and Y |- B,
we consider the sort of 'multicut' where any number of the occurrences of A in
Y (not necessarily all of them) are replaced by X, to give, say Z:
then the property is that such Z is derivable.
We no doubt could have done this for the multiset-sequent systems, which
would have meant showing the admissibility of
X |- A Y, A^n |- B
-------------------
X^n, Y |- B
(whereas what we actually proved was X, Y |- B)
So we define the relationship between Y and Z above, calling it strrep
consts
strrep :: "'f structr pair set => 'f structr pair set"
inductive "strrep S"
intrs
same "(s, s) : strrep S"
repl "p : S ==> p : strrep S"
sc "(u, v) : strrep S ==> (x, y) : strrep S ==> (u; x, v; y) : strrep S"
This this introduces the issue that where PA and CA are (say) the antecedents
of the premise and conclusion of a rule, and
(PA, CA) \in sctxt r for a relation (set of pairs) r, eg r = {(B;(C;D), B;C;D)}
(for the B|- rule), and ("multi"-)cutting with X |- A would give
CX, ie (CA, CX) \in strrep {(Sf A, X)},
then we need to close the box with PX, where
(PA, PX) \in strrep {(Sf A, X)} and (PX, CX) \in sctxt r
The easiest instance of this is where r is a set of pairs which are entirely
substitutable (ie like {(B;(C;D), B;C;D)} for the B|- rule,
not like {A, (t;A)} (for the KI_t|- rule)
strrep_sctxt_lcsub;
"[| (?PA, ?CA) : sctxt LTit_lcsub; (?CA, ?CX) : strrep {(Sf ?A, ?X)} |]
==> EX PX.
(?PA, PX) : strrep {(Sf ?A, ?X)} & (PX, ?CX) : sctxt LTit_lcsub"
Here LTit_lcsub is the set of pairs of the form found in the
rules B|-, B'|-, W|- for $LT^t_\to$
"(?Bs; (?Cs; ?Ds), ?Bs; ?Cs; ?Ds) : LTit_lcsub",
"(?Bs; (?Cs; ?Ds), ?Cs; ?Bs; ?Ds) : LTit_lcsub",
"(?Bs; ?Cs; ?Cs, ?Bs; ?Cs) : LTit_lcsub"
Where the fixed formula T is involved, the corresponding result is
(for example)
strrep_sctxt_KIt ;
"[| (?PA, ?CA) : sctxt (KIt T); ?A ~= T;
(?CA, ?CX) : strrep {(Sf ?A, ?X)} |] ==>
EX PX. (?PA, PX) : strrep {(Sf ?A, ?X)} & (PX, ?CX) : sctxt (KIt T)"
Here is another similar but slightly different rule required in some cases:
strrep_sctxt_ext;
"[| (?PA, ?CA) : sctxt {(?p, ?ca)}; (?CA, ?CX) : strrep {(Sf ?A, ?X)} |]
==> EX PX cx. (?PA, PX) : strrep {(Sf ?A, ?X)} &
(?ca, cx) : strrep {(Sf ?A, ?X)} & (PX, ?CX) : sctxt {(?p, cx)}"
So the "multicut"-admissibility property we prove inductively is
mclcd;
"mclcd ?rls ?A (?cl, ?cr) =
(ALL Xl Xr Y B.
?cl = (Xl |- ?A) -->
?cr = (Xr |- B) -->
(Xr, Y) : strrep {(Sf ?A, Xl)} --> (Y |- B) : derrec ?rls {})"
where the version conditional on cl and cr being derivable is
mclca ;
"mclca ?rls ?A (?cl, ?cr) =
(?cl : derrec ?rls {} -->
?cr : derrec ?rls {} --> mclcd ?rls ?A (?cl, ?cr))"
So mclca says that if Xl |- A and Xr |- B are derivable, and Y is got from
Xr by replacing some instances of A by Xl, then Y |- B is derivable.
So we get a variety of lemmas of which a sample follow:
With any rule of the form
C[X] |- E
---------
C[Y] |- E
on the left, the inductive step is easy.
gsmcl_lc_L ;
"[| lctxt ?prs <= ?rls; (?psl, ?cl) : lctxt ?prs |]
==> gen_step2 (mclcd ?rls) ?A ?any (derrec ?rls {}, ?drsr)
((?psl, ?cl), ?psr, ?cr)"
With these rules on the right, we have the following result
for the fully substitutable rules only:
gsmcl_lc_R ;
"[| lctxt LTit_lcsub <= ?rls; (?psr, ?cr) : lctxt LTit_lcsub |]
==> gen_step2 (mclcd ?rls) ?A ?any (?drsl, derrec ?rls {})
((?psl, ?cl), ?psr, ?cr)"
For the non fully substitutable rules of this form, we get
similar results for each such rule, assuming that the cut formula is not T
gsmcl_KIt_R_ne ;
"[| lctxt (KIt T) <= ?rls; ?A ~= T; (?psr, ?cr) : lctxt (KIt T) |]
==> gen_step2 (mclcd ?rls) ?A ?any (?drsl, derrec ?rls {})
((?psl, ?cl), ?psr, ?cr)"
When the cut formula is T, then (unlike in the paper!) we don't need any
further work specifically for that case, since the results for all
the possible rules on the left cover all possibilities.
Other easy rules are for the identity rule on the left or right,
and the impR rule on the right and impL on the left.
Finally we have the impL rule on the right, where the cut formula is not the
principal formula
gsmcl_impL_R_ne ;
"[| lcimpL <= ?rls; ?A ~= ?B -> ?D;
(?Cd, ?Cbda) : sctxt {(Sf ?D, Sf (?B -> ?D); ?As)} |]
==> gen_step2 (mclcd ?rls) ?A ?any (?drsl, derrec ?rls {})
((?psl, ?cl), [?As |- ?B, ?Cd |- ?E], ?Cbda |- ?E)"
and where the cut formula is the principal formula,
which was the most difficult to prove
gsmcl_imp_C8 ;
"[| lcimpL <= ?rls; (?Cd, ?Cbda) : sctxt {(Sf ?D, Sf (?B -> ?D); ?As)} |]
==> gen_step2 (mclcd ?rls) (?B -> ?D) ipsubfml
(derrec ?rls {}, derrec ?rls {})
(([?Xl; Sf ?B |- ?D], ?Xl |- ?B -> ?D), [?As |- ?B, ?Cd |- ?E],
?Cbda |- ?E)"
This last result also covers the case
where cut formula is the principal formula,
but the principal instance of that formula is not among the copies of that
formula which are replaced. It is only for that case that we require
the assumption lcimpL <= ?rls. The proof for that case is very much like that
of gsmcl_impL_R_ne above.
There is no such result for the impR rule on the left, other than these last two
results which also require the impL rule on the right. Results for other
rules on the right cover all the possibilities where the rule on the left is
impR.
Notice how all these results are expressed to apply to a rule set which is a
superset of a given set. Thus they are useful for
all of the consecution calculi
$LT^t_\to$ $LR^t_{\to;}$ $LT^{\textcircled{t}}_\to$
In fact we combined all the results above to get
gsmcl_LTit ;
"[| LTit <= ?rls; (?psl, ?cl) : LTit; (?psr, ?cr) : LTit |]
==> gen_step2 (mclcd ?rls) ?A ipsubfml (derrec ?rls {}, derrec ?rls {})
((?psl, ?cl), ?psr, ?cr)"
This gave us the result for $LT^t_\to$
(* assertion line 10, pg 500, New Consecution Calculi for Implicational Rt,
cut rule is admissible in LTt-> *)
mclca_LTit ; "mclca LTit ?A (?cl, ?cr)": thm
and made it quite easy to extend the proof to the other logics
$LR^t_{\to;}$ and $LT^{\textcircled{t}}_\to$, since for these we only
needed to deal with the cases involving a few additional rules on either side.
(* Thm 5.2, pg 504, New Consecution Calculi for Implicational Rt,
cut rule is admissible in LTcirct-> *)
mclca_LTitc ; "mclca LTitc ?A (?cl, ?cr)": thm
(* Thm 3.2, pg 500, New Consecution Calculi for Implicational Rt,
cut rule is admissible in LRt->; *)
mclca_LRitsc ; "mclca LRitsc ?A (?cl, ?cr)": thm
ADDED LATER re PI and TAU transformations
Tue May 2 12:22:36 AEST 2017
The second paper, Bimbo and Dunn,
On the dedidability of implicational ticket entailment
introduces transformations $\pi$ and $\tau$ between the logics
$LR_\to$ and $LT^{\textcircled{t}}_\to$
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 $LT^{\textcircled{t}}_\to$,
when we turn the structure in its antecedent into a multiset of formulae,
the resulting sequent is provable in $LR_\to$;
and the method of our proof followed the definition of $\pi$ in the paper.
We use some auxiliary functions:
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"
ms_of_str turns a structure into a multiset.
ap_ant applies a function to the antecedent of a sequent.
ap_psc applies a to each premise and to the conclusion of a rule.
Our first lemma was that for each rule in $LT^{\textcircled{t}}_\to$,
when we turn the consecutions into multisets, we get
a derived rule of $LR_\to$.
pi_lem ;
"(?ps, ?c) : LTitc ==> ap_psc (ap_ant ms_of_str) (?ps, ?c) : derl LRit"
We extend this to the result that any derived rule of
$LT^{\textcircled{t}}_\to$, translated, is a derived rule of
$LR_\to$.
Since 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 pi_der, which says simply that a provable sequent in
$LT^{\textcircled{t}}_\to$ is a provable sequent in $LR_\to$.
(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)
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 {}":
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 lcB, 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:
lctxt_sctxt_rtc ;
"lctxt ((sctxt ?r)^*) <= derl (lctxt ?r)"
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.
t_BA = "(?A; ?B, Sf T; (?B; ?A)) : (sctxt LTitc_lc)^*"
When we instantiate A and B in t_BA to A;B and C, to get
t_C_AB = "(?A; ?B; ?C, Sf T; (?C; (?A; ?B))) : (sctxt LTitc_lc)^*"
and apply rules B|- or B'|- we get
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)^*"
Of the four ways of composing these two, t_ACB then t_ACB gives the identity,
the other three give three more permutations of ?A ?B ?C
in "(?A; ?B; ?C, Sf T; (x; y; z)) : (sctxt LTitc_lc)^*"
The sixth permutation is the identity,
in "(?A; ?B; ?C, Sf T; (?A; ?B; ?C)) : (sctxt LTitc_lc)^*"
which is given simply by KIt|-
The other six case of Lemma 10 are got by taking these six results
and then applying t_BA (with left context T). This give two instances
of T at the left, which we can reduce to one, looking like
A; B; C
-------
T; (x; y; z)
------------------- t_BA
T; (T ; (z; (x; y)))
--------------------B|-
T; T ; (z; (x; y))
------------------Mt|-
T ; (z; (x; y))
Thus we get the other six cases of Lemma 10.
Composing these last six with B|- we get
T ; (z; (x; y))
--------------- B|-
T ; z ; (x; y)
and composing these with B|- we get
T ; z ; (x; y)
--------------- B|-
T ; z ; x; y
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.