%%% Admissibility of Cut in Classical Sequent Calculus
%%% Author: Frank Pfenning

ca' : {A:o} (pos A -> #) -> (neg A -> #) -> # -> type.
%mode ca' +A +D +E -F.

%%% Essential Conversions

ca_axiom'l : ca' A ([p] axiom' N p) E (E N).

ca_axiom'r : ca' A D ([n] axiom' n P) (D P).

ca_and1' :
  ca' (A and B) ([p] andr' (D1 p) (D2 p) p) ([n] andl1' ([n1] E1 n n1) n) F
     <- ({p1:pos A} ca' (A and B) ([p] D1 p p1) ([n] andl1' ([n1] E1 n n1) n) (D1' p1))
     <- ({n1:neg A}
	   ca' (A and B) ([p] andr' (D1 p) (D2 p) p)
	   ([n] E1 n n1) (E1' n1))
     <- ca' A ([p1] D1' p1) ([n1] E1' n1) F.

ca_and2' :
  ca' (A and B) ([p] andr' (D1 p) (D2 p) p) ([n] andl2' (E2 n) n) F
     <- ({p2:pos B} ca' (A and B) ([p] D2 p p2) ([n] andl2' (E2 n) n) (D2' p2))
     <- ({n2:neg B}
	   ca' (A and B) ([p] andr' (D1 p) (D2 p) p)
	   ([n] E2 n n2) (E2' n2))
     <- ca' B ([p2] D2' p2) ([n2] E2' n2) F.

ca_imp' :
  ca' (A imp B) ([p] impr' (D1 p) p) ([n] impl' (E1 n) (E2 n) n) F
     <- ({p1:pos A} ca' (A imp B) ([p] impr' (D1 p) p) ([n] E1 n p1) (E1' p1))
     <- ({n2:neg B} ca' (A imp B) ([p] impr' (D1 p) p) ([n] E2 n n2) (E2' n2))
     <- ({n1:neg A} {p2:pos B}
	   ca' (A imp B) ([p] D1 p n1 p2) ([n] impl' (E1 n) (E2 n) n)
	   (D1' n1 p2))
     <- ({p2:pos B} ca' A ([p1] E1' p1) ([n1] D1' n1 p2) (F2 p2))
     <- ca' B ([p2] F2 p2) ([n2] E2' n2) F.

ca_or1' :
  ca' (A or B) ([p] orr1' (D1 p) p) ([n] orl' (E1 n) (E2 n) n) F
     <- ({n1:neg A} ca' (A or B) ([p] orr1' (D1 p) p) ([n] E1 n n1) (E1' n1))
     <- ({p1:pos A} ca' (A or B) ([p] D1 p p1) ([n] orl' (E1 n) (E2 n) n)
	   (D1' p1))
     <- ca' A D1' E1' F.

ca_or2' :
  ca' (A or B) ([p] orr2' (D2 p) p) ([n] orl' (E1 n) (E2 n) n) F
     <- ({n2:neg B} ca' (A or B) ([p] orr2' (D2 p) p) ([n] E2 n n2) (E2' n2))
     <- ({p2:pos B} ca' (A or B) ([p] D2 p p2) ([n] orl' (E1 n) (E2 n) n)
	   (D2' p2))
     <- ca' B D2' E2' F.

ca_not' :
  ca' (not A) ([p] notr' (D1 p) p) ([n] notl' (E1 n) n) F
     <- ({p1:pos A} ca' (not A) ([p] notr' (D1 p) p) ([n] E1 n p1) (E1' p1))
     <- ({n1:neg A} ca' (not A) ([p] D1 p n1) ([n] notl' (E1 n) n) (D1' n1))
     <- ca' A E1' D1' F.

ca_forall' :
  ca' (forall A) ([p] forallr' (D1 p) p) ([n] foralll' T (E1 n) n) F
     <- ({n1} ca' (forall A) ([p] forallr' (D1 p) p) ([n] E1 n n1) (E1' n1))
     <- ({p1} ca' (forall A) ([p] D1 p T p1) ([n] foralll' T (E1 n) n) (D1' p1))
     <- ca' (A T) D1' E1' F.

ca_exists' :
  ca' (exists A) ([p] existsr' T (D1 p) p) ([n] existsl' (E1 n) n) F
     <- ({n1} ca' (exists A) ([p] existsr' T (D1 p) p) ([n] E1 n T n1) (E1' n1))
     <- ({p1} ca' (exists A) ([p] D1 p p1) ([n] existsl' (E1 n) n) (D1' p1))
     <- ca' (A T) D1' E1' F.

%%% Right Commutative Conversions

car_axiom' : ca' A D ([n] axiom' N P) (axiom' N P).

car_andr' :
  ca' A D ([n] andr' (E1 n) (E2 n) P) (andr' F1 F2 P)
     <- ({p1:pos B1} ca' A D ([n] E1 n p1) (F1 p1))
     <- ({p2:pos B2} ca' A D ([n] E2 n p2) (F2 p2)).

car_andl1' :
  ca' A D ([n] andl1' (E1 n) N) (andl1' F1 N)
     <- ({n1:neg B1} ca' A D ([n] E1 n n1) (F1 n1)).

car_andl2' :
  ca' A D ([n] andl2' (E2 n) N) (andl2' F2 N)
     <- ({n2:neg B2} ca' A D ([n] E2 n n2) (F2 n2)).

car_impr' :
  ca' A D ([n] impr' (E1 n) P) (impr' F1 P)
     <- ({n1:neg B1} {p2:pos B2}
	   ca' A D ([n] E1 n n1 p2) (F1 n1 p2)).

car_impl' :
  ca' A D ([n] impl' (E1 n) (E2 n) N) (impl' F1 F2 N)
     <- ({p1:pos B1} ca' A D ([n] E1 n p1) (F1 p1))
     <- ({n2:neg B2} ca' A D ([n] E2 n n2) (F2 n2)).


car_orr1' :
  ca' A D ([n] orr1' (E1 n) P) (orr1' F1 P)
     <- ({p1:pos B1} ca' A D ([n] E1 n p1) (F1 p1)).

car_orr2' :
  ca' A D ([n] orr2' (E2 n) P) (orr2' F2 P)
     <- ({p2:pos B2} ca' A D ([n] E2 n p2) (F2 p2)).

car_orl' :
  ca' A D ([n] orl' (E1 n) (E2 n) N) (orl' F1 F2 N)
     <- ({n1:neg B1} ca' A D ([n] E1 n n1) (F1 n1))
     <- ({n2:neg B2} ca' A D ([n] E2 n n2) (F2 n2)).

car_notr' :
  ca' A D ([n] notr' (E1 n) P) (notr' F1 P)
     <- ({n1:neg B1} ca' A D ([n] E1 n n1) (F1 n1)).

car_notl' :
  ca' A D ([n] notl' (E1 n) N) (notl' F1 N)
     <- ({p1:pos B1} ca' A D ([n] E1 n p1) (F1 p1)).

car_truer' :
  ca' A D ([n] truer' P) (truer' P).

car_falsel' :
  ca' A D ([n] falsel' N) (falsel' N).

car_forallr' :
  ca' A D ([n] forallr' (E1 n) P) (forallr' F1 P)
     <- ({a:i} {p1:pos (B1 a)}
	   ca' A D ([n] E1 n a p1) (F1 a p1)).

car_foralll' :
  ca' A D ([n] foralll' T (E1 n) N) (foralll' T F1 N)
     <- ({n1} ca' A D ([n] E1 n n1) (F1 n1)).

car_existsr' :
  ca' A D ([n] existsr' T (E1 n) P) (existsr' T F1 P)
     <- ({p1} ca' A D ([n] E1 n p1) (F1 p1)).

car_existsl' :
  ca' A D ([n] existsl' (E1 n) N) (existsl' F1 N)
     <- ({a:i} {n1:neg (B1 a)}
	   ca' A D ([n] E1 n a n1) (F1 a n1)).

%%% Left Commutative Conversions

cal_axiom' : ca' A ([p] axiom' N P) E (axiom' N P).

cal_andr' :
  ca' A ([p] andr' (D1 p) (D2 p) P) E (andr' F1 F2 P)
     <- ({p1:pos B1} ca' A ([p] D1 p p1) E (F1 p1))
     <- ({p2:pos B2} ca' A ([p] D2 p p2) E (F2 p2)).

cal_andl1' :
  ca' A ([p] andl1' (D1 p) N) E (andl1' F1 N)
     <- ({n1:neg B1} ca' A ([p] D1 p n1) E (F1 n1)).

cal_andl2' :
  ca' A ([p] andl2' (D2 p) N) E (andl2' F2 N)
     <- ({n2:neg B2} ca' A ([p] D2 p n2) E (F2 n2)).

cal_impr' :
  ca' A ([p] impr' (D1 p) P) E (impr' F1 P)
     <- ({n1:neg B1} {p2:pos B2}
	   ca' A ([p] D1 p n1 p2) E (F1 n1 p2)).

cal_impl' :
  ca' A ([p] impl' (D1 p) (D2 p) N) E (impl' F1 F2 N)
     <- ({p1:pos B1} ca' A ([p] D1 p p1) E (F1 p1))
     <- ({n2:neg B2} ca' A ([p] D2 p n2) E (F2 n2)).

cal_orr1' :
  ca' A ([p] orr1' (D1 p) P) E (orr1' F1 P)
     <- ({p1:pos B1} ca' A ([p] D1 p p1) E (F1 p1)).

cal_orr2' :
  ca' A ([p] orr2' (D2 p) P) E (orr2' F2 P)
     <- ({p2:pos B2} ca' A ([p] D2 p p2) E (F2 p2)).

cal_orl' :
  ca' A ([p] orl' (D1 p) (D2 p) N) E (orl' F1 F2 N)
     <- ({n1:neg B1} ca' A ([p] D1 p n1) E (F1 n1))
     <- ({n2:neg B2} ca' A ([p] D2 p n2) E (F2 n2)).

cal_notr' :
  ca' A ([p] notr' (D1 p) P) E (notr' F1 P)
     <- ({n1:neg B1} ca' A ([p] D1 p n1) E (F1 n1)).

cal_notl' :
  ca' A ([p] notl' (D1 p) N) E (notl' F1 N)
     <- ({p1:pos B1} ca' A ([p] D1 p p1) E (F1 p1)).

cal_truer' :
  ca' A ([p] truer' P) E (truer' P).

cal_falsel' :
  ca' A ([p] falsel' N) E (falsel' N).

cal_forallr' :
  ca' A ([p] forallr' (D1 p) P) E (forallr' F1 P)
     <- ({a:i} {p1:pos (B1 a)}
	   ca' A ([p] D1 p a p1) E (F1 a p1)).

cal_foralll' :
  ca' A ([p] foralll' T (D1 p) N) E (foralll' T F1 N)
     <- ({n1} ca' A ([p] D1 p n1) E (F1 n1)).

cal_existsr' :
  ca' A ([p] existsr' T (D1 p) P) E (existsr' T F1 P)
     <- ({p1} ca' A ([p] D1 p p1) E (F1 p1)).

cal_existsl' :
  ca' A ([p] existsl' (D1 p) N) E (existsl' F1 N)
     <- ({a:i} {n1:neg (B1 a)}
	   ca' A ([p] D1 p a n1) E (F1 a n1)).

%block lp : some {A:o} block {p:pos A}.
%block ln : some {A:o} block {n:neg A}.
%block li : block {a:i}.
%block lo : block {p:o}.
%worlds (lp | ln | li | lo) (ca' A D E F).
%covers ca' +A +D +E *F.
%terminates {A [D E]} (ca' A D E _).
%total {A [D E]} (ca' A D E _).