(* the systems [LR->] and [LRt->] ("sb" = Square Brackets) *)
LRisbcca = LRica (* or maybe just bdseq *) + gentree +
consts
(* mk_sb: make an LRi(t) derivation into a LRi(t)sb one,
in the canonical way (where no sequent is contractible)
dest_sb: convert a proof in LRi(t)sb to LRi(t) (note, gives a
choice of ordering of single formula contractions *)
(* need to define these given tree with unlabelled rules *)
mk_sb, dest_sb :: "(formula multiset, formula) sequent dertree trf"
(* height-preserving left contraction *)
hplctr :: "(formula multiset, formula) sequent psc set =>
formula => (formula multiset, formula) sequent dertree => bool"
defs
mk_sb_def "mk_sb dt == @dtsb. valid LRitsb dtsb & conclDT dtsb = conclDT dt"
dest_sb_def "dest_sb dtsb == @dt. valid LRit dt & conclDT dt = conclDT dtsb"
defs
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))"
end