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.