%%% Cut Elimination in Intuitionistic Sequent Calculus
%%% Author: Frank Pfenning

ce : conc* C -> conc C -> type.
%mode ce +D* -D.

ce_cut   : ce (cut* A D1* D2*) D
	    <- ce D1* D1
	    <- ({h1:hyp A} ce (D2* h1) (D2 h1))
	    <- ca A D1 D2 D.

ce_axiom : ce (axiom* H) (axiom H).

ce_andr  : ce (andr* D1* D2*) (andr D1 D2)
	    <- ce D1* D1
	    <- ce D2* D2.

ce_andl1 : ce (andl1* D1* H) (andl1 D1 H)
	    <- ({h1:hyp A} ce (D1* h1) (D1 h1)).

ce_andl2 : ce (andl2* D2* H) (andl2 D2 H)
	    <- ({h2:hyp B} ce (D2* h2) (D2 h2)).

ce_impr  : ce (impr* D1*) (impr D1)
	    <- ({h1:hyp A} ce (D1* h1) (D1 h1)).

ce_impl  : ce (impl* D1* D2* H) (impl D1 D2 H)
	    <- ce D1* D1
	    <- ({h2:hyp B} ce (D2* h2) (D2 h2)).

ce_orr1  : ce (orr1* D1*) (orr1 D1)
	    <- ce D1* D1.

ce_orr2  : ce (orr2* D2*) (orr2 D2)
	    <- ce D2* D2.

ce_orl   : ce (orl* D1* D2* H) (orl D1 D2 H)
	    <- ({h1:hyp A} ce (D1* h1) (D1 h1))
	    <- ({h2:hyp B} ce (D2* h2) (D2 h2)).

ce_notr  : ce (notr* D1*) (notr D1)
	    <- ({p:o} {h1:hyp A} ce (D1* p h1) (D1 p h1)).

ce_notl  : ce (notl* D1* H) (notl D1 H)
	    <- ce D1* D1.

ce_truer : ce (truer*) (truer).

ce_falsel : ce (falsel* H) (falsel H).

ce_forallr : ce (forallr* D1*) (forallr D1)
	      <- {a:i} ce (D1* a) (D1 a).

ce_foralll : ce (foralll* T D1* H) (foralll T D1 H)
	      <- ({h1} ce (D1* h1) (D1 h1)).

ce_existsr : ce (existsr* T D1*) (existsr T D1)
	      <- ce D1* D1.

ce_existsl : ce (existsl* D1* H) (existsl D1 H)
	      <- ({a:i} {h1:hyp (A1 a)} ce (D1* a h1) (D1 a h1)).
		    
%worlds (l1 | l2 | l3) (ce D* D).
%covers ce +D *D*.
%terminates D (ce D _).
%total D (ce D _).