(* stuff that was in gcmctree, but depends on using sequents,
involved cut, multicut, contraction *)
(* will use concrete derivation trees for proving cut, rather than multicut,
admissibility, where there are explicity contraction rules *)
theory gcmctree imports cagen gentree begin
consts
masdt :: "'a sequent psc set => 'a =>
('a sequent dertree * 'a sequent dertree) set"
casdt :: "'a sequent psc set => 'a =>
('a sequent dertree * 'a sequent dertree) set"
inductive "masdt rls A"
intros
I : "valid rls dtl & valid rls dtr -->
(conclDT dtl, conclDT dtr) : mar rls A ==>
(dtl, dtr) : masdt rls A"
inductive "casdt rls A"
intros
I : "valid rls dtl & valid rls dtr -->
(conclDT dtl, conclDT dtr) : car rls A ==>
(dtl, dtr) : casdt rls A"
end