(* this theory shows what we can do without the deletion lemma *) Ldi_rules_nd = Ctr + Wk + consts ldi_rules :: "(structr sequent list * structr sequent) set" inductive "ldi_rules" intrs (* rep_SV "(c, p) : seqrepI (range SV) ==> ([p], c) : ldi_rules" rep_Sf "(c, p) : seqrepI (range Structform) ==> ([p], c) : ldi_rules" *) rep_atom "(c, p) : seqrepI str_atoms ==> ([p], c) : ldi_rules" (* actually, following gives cldi *) wkI "(c, p) : seqdel (stars I) ==> ([p], c) : ldi_rules" idps "rule : rulefs idps ==> rule : ldi_rules" cA "rule : rulefs {cA} ==> rule : ldi_rules" ila "rule : rulefs {ila} ==> rule : ldi_rules" ils "rule : rulefs {ils} ==> rule : ldi_rules" idf "rule : rulefs {idf} ==> rule : ldi_rules" lil_adds "rule : rulefs lil_adds ==> rule : ldi_rules" lir_adds "rule : rulefs lir_adds ==> rule : ldi_rules" end