calk = lkdt + cagen (* to deal with admissibility of cut *) (* (* inductive def'n of cases where cut-admissibility will be proved *) inductive "cap" intrs lrpI "[| (ps, {} |- {A}) : lkir ; (qs, {A} |- {}) : lkil ; pse = map (extend (X, Y)) ps ; qse = map (extend (X, Y)) qs ; (ALL p: set pse. (p, A, insert A X |- Y) : cap) ; (ALL q: set qse. (X |- insert A Y, A, q) : cap) ; (sfa, A) : ipsubfml ; (X |- insert sfa Y, sfa, insert sfa X |- Y) : cap |] ==> (X |- insert A Y, A, insert A X |- Y) : cap" lcI "[| (ps, U |- V) : lkne ; A ~: V ; pscmap fmls (ps, U |- V) = (pse, X |- insert A Y) ; ALL p: set pse. (p, A, insert A X |- Y) : cap |] ==> (X |- insert A Y, A, insert A X |- Y) : cap" rcI "[| (ps, U |- V) : lkne ; A ~: U ; pscmap fmls (ps, U |- V) = (pse, insert A X |- Y) ; ALL p: set pse. (X |- insert A Y, A, p) : cap |] ==> (X |- insert A Y, A, insert A X |- Y) : cap" axlI "A : X ==> (X |- insert A Y, A, insert A X |- Y) : cap" axrI "A : Y ==> (X |- insert A Y, A, insert A X |- Y) : cap" *)