%%% Classical Sequent Calculus with Cut.
%%% Author: Frank Pfenning

@ : type.        % Token (for contradiction)
%name @ D*.

cut^   : (pos A -> @)
	  -> (neg A -> @)
	  -> @.

axiom^ : (neg A -> pos A -> @).

andr^  : (pos A -> @)
	  -> (pos B -> @)
	  -> (pos (A and B) -> @).

andl1^ : (neg A -> @)
	  -> (neg (A and B) -> @).

andl2^ : (neg B -> @)
	  -> (neg (A and B) -> @).

impr^  : (neg A -> pos B -> @)
	  -> (pos (A imp B) -> @).

impl^  : (pos A -> @)
	  -> (neg B -> @)
	  -> (neg (A imp B) -> @).

orr1^  : (pos A -> @)
	 -> (pos (A or B) -> @).

orr2^  : (pos B -> @)
	  -> (pos (A or B) -> @).

orl^   : (neg A -> @)
	 -> (neg B -> @)
	 -> (neg (A or B) -> @).

notr^  : (neg A -> @)
	  -> (pos (not A) -> @).

notl^  : (pos A -> @)
	  -> (neg (not A) -> @).

truer^ : (pos (true) -> @).

falsel^ : (neg (false) -> @).

forallr^ : ({a:i} pos (A a) -> @)
	    -> (pos (forall A) -> @). 

foralll^ : {T:i} (neg (A T) -> @)
	    -> (neg (forall A) -> @).

existsr^ : {T:i} (pos (A T) -> @)
	    -> (pos (exists A) -> @).

existsl^ : ({a:i} neg (A a) -> @)
	    -> (neg (exists A) -> @).