SKELETON of how the decidability proof might go, and check in Isabelle that
the bits of it hang together

the decision procedure starts with a finite number of (potential) proofs of
a given formula in LRitsb,
so we need to show that from one of these, a finite procedure will give a vliad
proof in LTit.

Here our finite set of potential proofs will be the irredundant partial proofs
which use the rules of LRitsb (partial means it still may have unproved
leaves).

Isabelle proof is underway, that as we keep developing a partial proof, we 
can't in so doing create an infinite branch. Coupling this with the fact that
at each point in the construction of a proof we have a finite number of choices
(since an actual proof tree has a finite branching factor, and so finitely many
branches, and finitely many choices of the next step at each branch).
(Note - these are the details omitted from the paper because it confuses
proof tree with proof search tree).
So this should give that the proof search tree is finite.  (This is the point
that is not quite so obvious, I think, but that is Konig's lemma).

So it is a finite procedure to get all the valid proofs in LRitsb.

So the decision procedure starts with these.

So the decidability assertion starts with

"valid LTit dt --> (EX dtsb. valid LRitsb dtsb & lctr_irred dtsb & \ ..."

that is, if A is a theorem of Tt-> (ie, if there is a proof tree dt such that
valid LTit dt and conclDT dt = A),
there is an irredundant proof tree dtsb, valid in LRitsb,
which enables us to establish that there is a proof in Tt->,
ie from dtsb we get a proof in LTit of A
(that is, we get a proof tree dtt such that valid LTit dtt,
and conclDT dtt = conclDT dt).

Since the method presented involves starting with dtsb, 
turning it into a proof in LRit, and removing the |- t rules,
and then applying tau to the result,
we want dtt such that dtt : tau (mk_tRfree (dest_sb dtsb))

so the following assertion is how we would prove decidability
  "valid LTit dt --> (EX dtsb. valid LRitsb dtsb & lctr_irred dtsb & \
      \ (EX dtt. dtt : tau (mk_tRfree (dest_sb dtsb)) & valid LTit dtt & \
            \ conclDT dtt = conclDT dt))"

actually there is a bit more to decidability than that:
tau of any tree must give a finite set of trees,
tau must be constructive,
mk_tRfree and dest_sb must be constructive (eg, we can't define dest_sb
just by saying we know such tree must exist, and choose one,
although Isabelle's logic would be fine with such a definition)

Anyway, how do we prove this?  Well, the first point is that the existence of
dt must lead to the existence of dtt.  
Two plausible approaches to this
(1) dtt is equal (or similar, or somehow related) to dt
(2) tau must produce, as a matter of course, a sufficient set of proof trees 
that you can be sure that if there is a proof tree in LTit, then tau will give
you one (at least, when tau is applied to all LRitsb proofs (after
applying dest_sb and mk_tRfree to them))

All the stuff about pi (which is mentioned in the proof of Lemma 11, last two
lines) seems only relevant to (1).  The only relevance of pi can be for an
argument along the lines of the following:
  NOTE - proof of "completeness" of decision procedure starts here
  if dt exists (a proof of t |- A in LTit), then
  pi dt is a proof of t |- A in LRit
  mk_sb (pi dt) is a (related) proof of t |- A in LRitsb
  mk_lctr_irred (mk_sb (pi dt)) is a (related) irredundant
    proof of t |- A in LRitsb
  NOTE - actual decision procedure starts here
  mk_lctr_irred (mk_sb (pi dt)) is one of the finitely many valid
    irredundant proofs found by the decision procedure
  dest_sb (mk_lctr_irred (mk_sb (pi dt))) is a proof in LRit
    (may differ from pi dt in that contractions are moved relative to ->|-)
  mk_tRfree (dest_sb (mk_lctr_irred (mk_sb (pi dt)))) is a (|-t)-free
    proof in LRit
  then tau (mk_tRfree (dest_sb (mk_lctr_irred (mk_sb (pi dt)))))
    hopefully contains a proof dtt in LTit,
    and (if pi is at all relevant) dtt should be
    either dt or some sort of transform of dt

So the proof in Isabelle of the result above depends on the assertion which
I've made, without proof, that

tau_irr_sb_pi ; "valid LTit ?dt ==>
  ?dt : tau (mk_tRfree (dest_sb (mk_lctr_irred (mk_sb (pi ?dt)))))"

This assertion strikes me as dubious.  Allowing that it would be true that
dt is in tau (pi dt), we should consider how different the proofs 
pi dt and mk_tRfree (dest_sb (mk_lctr_irred (mk_sb (pi ?dt)))) are.
Now mk_lctr_irred simplifies a proof (it excises parts of a proof, and uses
height-preserving contraction admissibility), and mk_tRfree makes changes which
are probably insignificant.  But the dest_sb (mk_sb ...) combination moves
contractions around, relative to occurrences of ->|-.  (This is potentially a
significant point, the fact that pi alone doesn't do such movements is Lemma 6).

OTHER ASSERTIONS we use in the proof of this result are:
mk_sbt; "valid LRit ?dt ==> valid LRitsb (mk_sb ?dt)"
mk_lctr_irred_valid ; "valid LRitsb ?dt ==> valid LRitsb (mk_lctr_irred ?dt)"
mk_lctr_irred ; "lctr_irred (mk_lctr_irred ?dt)"
valid_pi ; "valid LTitc ?dt ==> valid LRit (pi ?dt)"

Mostly these are because I haven't yet defined these transformations of
proof trees.
For example, I have proved

pi_der ;
    "(?a |- ?c) : derrec LTitc {} ==> (ms_of_str ?a |- ?c) : derrec LRit {}"

whose proof uses the construction described in the paper as pi
(shallow embedding of derivations)
but we haven't yet defined pi as a transformation of proof trees
(which are deeply embedded derivations) in Isabelle

Likewise, mk_sb would be the construction of a proof tree
expressing the fact that "derrec LRitsb {} >= derrec LRit {}"
where we have proved

LRitsb_eqv_LRit ; "derrec LRitsb {} = derrec LRit {}": thm

and mk_lctr_irred would be the construction of a proof tree
expressing the fact that

ex_lctr_irred_lem ;
"valid LRitsb ?x ==> EX dtr.  lctr_irred dtr & valid LRitsb dtr &
  conclDT dtr = conclDT ?x & heightDT dtr <= heightDT ?x"

OTHER THINGS PROVED since submitted version

that the contraction admissibility of LRisb and LRitsb
is height-preserving:

we previously proved contraction admissibility of LRisb and LRitsb as
 lctr_adm_LRitsb ; "lctr_adm LRitsb ?A"
 lctr_adm_LRisb ; "lctr_adm LRisb ?A"

 where
 lctr_adm_def;
    "lctr_adm ?rls ?A ==
          ALL Xl B.
	           (Xl + {#?A#} + {#?A#} |- B) : derrec ?rls {} -->
		            (Xl + {#?A#} |- B) : derrec ?rls {}"

but to prove height-preserving contraction admissibility we need to 
deal with proof trees, whose height we can define, thus we prove 

 hplctr_LRisb ; "hplctr LRisb ?A ?dt"
 hplctr_LRitsb ; "hplctr LRitsb ?A ?dt"

 where 

hplctr_def ; "hplctr ?rls ?A ?dt == valid ?rls ?dt -->
      (ALL X B.  conclDT ?dt = (X + {#?A#} + {#?A#} |- B) -->
          (EX dtn.  valid ?rls dtn &
              conclDT dtn = (X + {#?A#} |- B) & heightDT dtn <= heightDT ?dt))"

Recall from previous work

valid_derrec ; "valid ?rls ?dt ==> conclDT ?dt : derrec ?rls {}"
derrec_valid ; "?a : derrec ?rls {} ==> EX dt. valid ?rls dt & conclDT dt = ?a"

As a matter of fact we don't _have_ to prove height-preserving contraction
admissibility this way, we could define a new inductive set in place of derrec, 
where A : derrec_n n rls prems means 
"A is provable from premises prems using rules rls in at most n steps"
(which I think is what was done in that paper by Nipkow et al which you showed
me and was rejected).

Note that proving height-preserving contraction admissibility this way
still doesn't give us the function which constructs the relevant tree, 
and I think we would need that function to define mk_lctr_irred

I've proved the completeness of LRitc and LRitsc for Rt->

Ri_LRitsc ;
   "?f : R1 (A1 Un A2 Un A3 Un A4 Un A5) ==> (Sf T |- ?f) : derrec LRitsc {}"
Ri_LTitc ;
   "?f : R1 (A1 Un A2 Un A3 Un A4 Un A5) ==> (Sf T |- ?f) : derrec LTitc {}"

and the completeness or LTit for Tt->

Ti_LTit ;
 "?f : R1 (A1 Un A2 Un A4 Un A5) ==> (Sf T |- ?f) : derrec LTit {}"

and started to prove soundness, not got very far
(for LTitc, LRitsc, wrt Rt->, need to show can get any permutation of 
antecedents from A3 and A2)
(for LTit wrt Tt->, because the proof in the paper seems to use atomic
contraction)

I started on the