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

ca : {A:o} conc A -> (hyp A -> conc C) -> conc C -> type.
%mode ca +A +D +E -F.

%% Axiom Conversions

ca_axiom_l : ca A (axiom H) E (E H).

ca_axiom_r : ca A D ([h:hyp A] axiom h) D.

%% Essential Conversions

ca_and1 : ca (A1 and A2) (andr D1 D2)
	   ([h:hyp (A1 and A2)] andl1 (E1 h) h) F
	   <- ({h1:hyp A1}
		 ca (A1 and A2) (andr D1 D2)
		 ([h:hyp (A1 and A2)] E1 h h1) (E1' h1))
	   <- ca A1 D1 E1' F.

ca_and2 : ca (A1 and A2) (andr D1 D2)
	   ([h:hyp (A1 and A2)] andl2 (E2 h) h) F
	   <- ({h2:hyp A2}
		 ca (A1 and A2) (andr D1 D2)
		 ([h:hyp (A1 and A2)] E2 h h2) (E2' h2))
	   <- ca A2 D2 E2' F.

ca_imp  : ca (A1 imp A2) (impr D2)
	   ([h:hyp (A1 imp A2)] impl (E1 h) (E2 h) h) F
	   <- ca (A1 imp A2) (impr D2) E1 E1'
	   <- ({h2:hyp A2}
		 ca (A1 imp A2) (impr D2)
		 ([h:hyp (A1 imp A2)] E2 h h2) (E2' h2))
	   <- ca A1 E1' D2 D2'
	   <- ca A2 D2' E2' F.

ca_or1  : ca (A1 or A2) (orr1 D1)
	   ([h:hyp (A1 or A2)] orl (E1 h) (E2 h) h) F
	   <- ({h1:hyp A1}
		 ca (A1 or A2) (orr1 D1)
		 ([h:hyp (A1 or A2)] E1 h h1) (E1' h1))
	   <- ca A1 D1 E1' F.

ca_or2  : ca (A1 or A2) (orr2 D2)
	   ([h:hyp (A1 or A2)] orl (E1 h) (E2 h) h) F
	   <- ({h2:hyp A2}
		 ca (A1 or A2) (orr2 D2)
		 ([h:hyp (A1 or A2)] E2 h h2) (E2' h2))
	   <- ca A2 D2 E2' F.

ca_not  : ca (not A1) (notr D1)
	   ([h:hyp (not A1)] notl (E1 h) h) (F2 C)
	   <- ca (not A1) (notr D1) E1 F1
	   <- ({p:o} ca A1 F1 ([h1:hyp A1] D1 p h1) (F2 p)).

ca_forall : ca (forall A1) (forallr D1)
	     ([h:hyp (forall A1)] foralll T (E1 h) h) F
	     <- ({h2:hyp (A1 T)}
		   ca (forall A1) (forallr D1)
		   ([h:hyp (forall A1)] E1 h h2) (E1' h2))
	     <- ca (A1 T) (D1 T) E1' F.

ca_exists : ca (exists A1) (existsr T D1)
	     ([h:hyp (exists A1)] existsl (E1 h) h) F
	     <- ({a:i} {h1:hyp (A1 a)}
		   ca (exists A1) (existsr T D1)
		   ([h:hyp (exists A1)] E1 h a h1) (E1' a h1))
	     <- ca (A1 T) D1 (E1' T) F.

%% Left Commutative Conversions

cal_andl1  : ca A (andl1 D1 H) E (andl1 D1' H)
	      <- {h1:hyp B1} ca A (D1 h1) E (D1' h1).

cal_andl2  : ca A (andl2 D2 H) E (andl2 D2' H)
	      <- {h2:hyp B2} ca A (D2 h2) E (D2' h2).

cal_impl   : ca A (impl D1 D2 H) E (impl D1 D2' H)
	      <- ({h2:hyp B2} ca A (D2 h2) E (D2' h2)).

cal_orl    : ca A (orl D1 D2 H) E (orl D1' D2' H)
	      <- ({h1:hyp B1} ca A (D1 h1) E (D1' h1))
	      <- ({h2:hyp B2} ca A (D2 h2) E (D2' h2)).

cal_notl   : ca A (notl D1 H) E (notl D1 H).

cal_falsel  : ca A (falsel H) E (falsel H).

cal_foralll : ca A (foralll T D1 H) E (foralll T D1' H)
	       <- ({h} ca A (D1 h) E (D1' h)).

cal_existsl : ca A (existsl D1 H) E (existsl D1' H)
	       <- ({a:i} {h:hyp (B1 a)}
		     ca A (D1 a h) E (D1' a h)).

%% Right Commutative Conversions

car_axiom : ca A D ([h:hyp A] axiom H1) (axiom H1).

car_andr : ca A D ([h:hyp A] andr (E1 h) (E2 h)) (andr E1' E2')
	    <- ca A D E1 E1'
	    <- ca A D E2 E2'.

car_andl1: ca A D ([h:hyp A] andl1 (E1 h) H) (andl1 E1' H)
	    <- ({h1:hyp B1} ca A D ([h:hyp A] E1 h h1) (E1' h1)).

car_andl2: ca A D ([h:hyp A] andl2 (E2 h) H) (andl2 E2' H)
	    <- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).

car_impr : ca A D ([h:hyp A] impr (E2 h)) (impr E2')
	    <- ({h1:hyp B1} ca A D ([h:hyp A] E2 h h1) (E2' h1)).

car_impl : ca A D ([h:hyp A] impl (E1 h) (E2 h) H) (impl E1' E2' H)
	    <- ca A D E1 E1'
	    <- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).

car_orr1 : ca A D ([h:hyp A] orr1 (E1 h)) (orr1 E1')
	    <- ca A D E1 E1'.

car_orr2 : ca A D ([h:hyp A] orr2 (E2 h)) (orr2 E2')
	    <- ca A D E2 E2'.

car_orl  : ca A D ([h:hyp A] orl (E1 h) (E2 h) H) (orl E1' E2' H)
	    <- ({h1:hyp B1} ca A D ([h:hyp A] E1 h h1) (E1' h1))
	    <- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).

car_notr : ca A D ([h:hyp A] notr (E1 h)) (notr E1')
	    <- ({p:o} {h1:hyp B1} ca A D ([h:hyp A] E1 h p h1) (E1' p h1)).

car_notl : ca A D ([h:hyp A] notl (E1 h) H) (notl E1' H)
	    <- ca A D E1 E1'.

car_truer: ca A D ([h:hyp A] truer) (truer).

car_falsel : ca A D ([h:hyp A] falsel H) (falsel H).

car_forallr : ca A D ([h:hyp A] forallr (E1 h)) (forallr E1')
	       <- ({a:i} ca A D ([h:hyp A] E1 h a) (E1' a)).

car_foralll: ca A D ([h:hyp A] foralll T (E1 h) H) (foralll T E1' H)
	      <- ({h1} ca A D ([h:hyp A] E1 h h1) (E1' h1)).

car_existsr : ca A D ([h:hyp A] existsr T (E1 h)) (existsr T E1')
	       <- ca A D E1 E1'.

car_existsl : ca A D ([h:hyp A] existsl (E1 h) H) (existsl E1' H)
	       <- ({a:i} {h1:hyp (B1 a)}
		     ca A D ([h:hyp A] E1 h a h1) (E1' a h1)).