Your proof, page 228, in paras 3 and 4, say to
"generate all the permutations and groupings" of a multiset of formulae,
and I take it that this relies on your Lemmas 8, 9 and 10,
which say that each of the permutations and groupings of
two or three structures (with t added in certain positions)
can be proved using LT-circle-t->.
Later in Lemma 11, proof, para 2, you say "LT-circle-t->
can generate all the permutations and groupings of formulas in a
sequent". (I see this following from Lemmas 8 to 10).
Then you say
"Since all the possible permutations and grouping are considered in both
cases, those that do not use K_t|- or T_t|- are also included"
You then look at the proof concerned, to see if it uses K_t|- or T_t|-,
and if there is no proof which does not use K_t|- or T_t|-,
then that decides the formula is not Tt-> provable.
We have a problem here: is it not possible that some relevant
"permutation and grouping" has multiple proofs, some using K_t|- or T_t|-,
and other not? As far as we can see, this possibility is not consistent with
your argument outlined above.
Furthermore - since it may be possible to decide which of the 12 possibilities
in each of Lemmas 9 and 10 have proofs which do not use K_t|- or T_t|-,
there remains the point that when doing a permutation and grouping of
more than 3 structures, you would use Lemmas 8 to 10 several times:
there may be different ways of using different instances of
Lemmas 8 to 10, and also there may be ways of doing a permutation and grouping
of 4 or more structures which have proofs which cannot be separated out into
proofs of the various instances of Lemmas 8 to 10.