(* the pi transformation, Bimbo and Dunn,
On the decidability of implicational ticket entailment,
Def 3, Lemma 3, pp 220-1 *)
pi = bdseq + dtree +
(* transformation of proof trees,
need to define effect of pi_rl on (unlabelled) rules,
one rule may transform to a tree (compound or derived) rule,
but note, the definition invariably involves an arbitrary choice
(choice of ordering of single-formula contractions to replace a
structure contraction), so why not just use SOME valid tree,
with the right sequents top and bottom, per pi_lem *)
consts
pi :: "('f structr, 'f) sequent dertree => ('f multiset, 'f) sequent dertree"
pi_rl :: "('f structr, 'f) sequent psc => ('f multiset, 'f) sequent dertree"
rules (* ASSUMED, NOT PROVED *)
valid_pi "valid LTitc dt ==> valid LRit (pi dt)"
concl_pi "valid LTitc dt ==> conclDT (pi dt) = ap_ant ms_of_str (conclDT dt)"
end