Cut Admissibility

seq.elf

term : type.
and : term -> term -> term.
or  : term -> term -> term.
imp : term -> term -> term.
top : term.

hyp : term -> type.

true : term -> type.
init : true A
        <- hyp A.

topR : true top.

andR : true A -> true B -> true (and A B).
andL : hyp (and A B) -> (hyp A -> hyp B -> true C) -> true C.

orR1 : true A -> true (or A B).
orR2 : true B -> true (or A B).
orL  : hyp (or A B)
        -> (hyp A -> true C)
        -> (hyp B -> true C)
        -> true C.

impR : true (imp A B)
        <- (hyp A -> true B).
impL : true C
        <- (hyp B -> true C)
        <- true A
        <- hyp (imp A B).

cut : {A} true A -> (hyp A -> true B) -> true B -> type.
%mode cut +T +A +B -C.
- : cut A DA init DA.
- : cut A (init HA) E (E HA).
- : cut A DA ([hA] Closed) Closed.
- : cut (and A B) (andR DA DB) ([hAB : hyp (and A B)] andL hAB ([hA : hyp A][hB : hyp B] F0 hAB hA hB)) F
     <- ({hA}{hB} cut (and A B) (andR DA DB) ([hAB] F0 hAB hA hB) (F1 hA hB))
     <- ({hB} cut A DA ([hA] F1 hA hB) (F2 hB))
     <- cut B DB ([hB] F2 hB) F.
- : cut (imp A B) (impR ([hA : hyp A] AtoB hA)) ([hAB : hyp (imp A B)] impL hAB (G hAB) ([hB : hyp B] F1 hAB hB)) F
     <- cut (imp A B) (impR ([hA] AtoB hA)) ([hAB] G hAB) DA
     <- cut A DA ([hA] AtoB hA) DB
     <- ({hB} cut (imp A B) (impR AtoB) ([hAB] F1 hAB hB) (F2 hB))
     <- cut B DB ([hB] F2 hB) F.
- : cut (or A B) (orR1 DA) ([hAB] orL hAB (L1 hAB) (R hAB)) L
     <- ({hA} cut (or A B) (orR1 DA) ([hAB] L1 hAB hA) (L2 hA))
     <- cut A DA L2 L.
- : cut (or A B) (orR2 DB) ([hAB] orL hAB (L hAB) (R1 hAB)) R
     <- ({hB} cut (or A B) (orR2 DB) ([hAB] R1 hAB hB) (R2 hB))
     <- cut B DB R2 R.
- : cut C (andL DAB ([hA][hB] D hA hB)) E (andL DAB ([hA][hB] F hA hB))
     <- ({hA}{hB} cut C (D hA hB) E (F hA hB)).
- : cut C (impL DA Hab ([hB] D hB)) E (impL DA Hab ([hB] F hB))
     <- ({hB} cut C (D hB) E (F hB)).
- : cut C (orL HAB DA DB) E (orL HAB EA EB)
   <- ({hA} cut C (DA hA) E (EA hA))
   <- ({hB} cut C (DB hB) E (EB hB)).
- : cut A DA ([hA] andR (F1 hA) (G1 hA)) (andR F G)
     <- cut A DA F1 F
     <- cut A DA G1 G.
- : cut A DA ([hA] impR ([hB] F1 hA hB)) (impR G)
     <- ({hB} cut A DA ([hA] F1 hA hB) (G hB)).
- : cut A DA ([hA] orR1 (DBC1 hA)) (orR1 DBC)
     <- cut A DA DBC1 DBC.
- : cut A DA ([hA] orR2 (DBC1 hA)) (orR2 DBC)
     <- cut A DA DBC1 DBC.
- : cut A DA ([hA] andL HBC ([hB][hC] F1 hA hB hC)) (andL HBC F)
     <- ({hB}{hC} cut A DA ([hA] F1 hA hB hC) (F hB hC)).
- : cut A DA ([hA] impL HBC (G1 hA) ([hC] F1 hA hC)) (impL HBC G F)
     <- cut A DA G1 G
     <- ({hC} cut A DA ([hA] F1 hA hC) (F hC)).
- : cut A DA ([hA] orL HBC (DB1 hA) (DC1 hA)) (orL HBC DB DC)
   <- ({hB} cut A DA ([hA] DB1 hA hB) (DB hB))
   <- ({hC} cut A DA ([hA] DC1 hA hC) (DC hC)).

%block always-has-hyp : some {A : term} block {H : hyp A}.
%worlds (always-has-hyp) (cut _ _ _ _).
%total {A [D E]} (cut A D E _).