Hi Raj,

You asked me to set out the quotations from the paper relevant to
the question of whether contractions in LTt-> can be replaced by
contractions of only single formulae.

In Extracting-BB'IW-Inhabitants, paged 152, in the last nine lines,
we have

"We would like to work with certain types of proofs of theorems.
First of all, we consider proofs in which (W|-) contracts
atomic structures.  In proofs of theorems,
a complex structure must be disassociated because of the (|-->) rule,
hence, every theorem has a proof that satisfies this constraint."

That seems to mean that every theorem of LTt-> has a proof whose 
contractions are all of structures which are a single formula.

And this seems to be used on page 157, step 4, the para starting with 
B;C;C, where it seems to be assumed that C is a (possibly annotated)
simple formula

In 'On the dedidability of implicational ticket entailment', page 231,
item 3 of the proof of Lemma 11 seems to say you can't replace
a contraction of a complex structure with multiple contractions of
atomic structrures (ie, formulae).

It says

3. Step 5 [of the definition of the tau transformation, on page 228]
allows the same as well as more powerful contractions that LR -> does,
which guarantees that a contraction step that is legitimate in LT -> 
(and is a series of W |- steps in LR ->) does not need
to be rendered as a series of contractions on atomic formulas,
which would require a regrouping of formulas in a way that is
potentially not allowed for a T → theorem.

Furthermore, in step 5 of the tau transformation,
you look at the consecutive (formula) contractions in the LRt-> proof,
and consider these as several contractions,
each of several of these formula at once, in all possible ways
(and then each grouping of several formulae is turned into a structure
in all possible ways).  

The reason for doing this would presumably be that, in LTt->, contraction
of complex structures is sometimes necessary, ie, it can not always be
replaced by contractions of single formula.

So the question arising from these is, is it possible to prove any
theorem of LTt-> using contractions of only single formulae?

Jeremy