%%% Completeness of sequent calculus
%%% Author: Frank Pfenning

cp : nd A -> right A -> type.

%%% Multiplicatives

% A -o B
lolliICP : cp (lolliI ^ D1) (lolliR ^ R1)
	    o- ({x:nd A} {l:left A}
		  cp x (init ^ l) -o cp (D1 ^ x) (R1 ^ l)).

lolliECP : cp (lolliE ^ D1 ^ D2) 
	    (cut ^ R2
	       ^ ([l^left A] cut ^ R1
		    ^ ([k^left (lolli A B)]
			 lolliL ^ (init ^ l) ^ ([r^left B] init ^ r) ^ k)))
	    o- cp D1 R1
	    o- cp D2 R2.

% A * B
tensorICP : cp (tensorI ^ D1 ^ D2) (tensorR ^ R1 ^ R2)
	     o- cp D1 R1
	     o- cp D2 R2.

tensorECP : cp (tensorE ^ D1 ^ D2)
	     (cut ^ R1
		^ [l^left (tensor A B)] tensorL ^ R2 ^ l)
	     o- cp D1 R1
	     o- ({x:nd A} {l:left A} {y:nd B} {k:left B}
		   cp x (init ^ l)
		   -o cp y (init ^ k)
		   -o cp (D2 ^ x ^ y) (R2 ^ l ^ k)).
% 1
oneICP : cp (oneI) (oneR).

oneECP : cp (oneE ^ D1 ^ D2) (cut ^ R1 ^ ([l^left (one)] oneL ^ R2 ^ l))
	  o- cp D1 R1
	  o- cp D2 R2.

%%% Additives

% A & B

withICP : cp (withI ^ (D1, D2)) (withR ^ (R1, R2))
	   o- cp D1 R1 & cp D2 R2.

withE1CP : cp (withE1 ^ D1)
	    (cut ^ R1
	       ^ ([l^left (with A B)] withL1 ^ ([k^left A] init ^ k) ^ l))
	    o- cp D1 R1.

withE2CP : cp (withE2 ^ D1)
	    (cut ^ R1
	       ^ ([l^left (with A B)] withL2 ^ ([k^left B] init ^ k) ^ l))
	    o- cp D1 R1.

% T
topICP : cp (topI ^ ()) (topR ^ ())
	  o- <T>.

% no topE

% A + B
plusI1CP : cp (plusI1 ^ D1) (plusR1 ^ R1)
	    o- cp D1 R1.

plusI2CP : cp (plusI2 ^ D2) (plusR2 ^ R2)
	    o- cp D2 R2.

plusECP : cp (plusE ^ D1 ^ (D2 , D3))
	   (cut ^ R1
	      ^ ([l^left (plus A B)] plusL ^ (R2, R3) ^ l))
	   o- cp D1 R1
	   o- ({x:nd A} {l:left A}
		 cp x (init ^ l)
		 -o cp (D2 ^ x) (R2 ^ l))
	      & ({y:nd B} {k:left B}
		   cp y (init ^ k)
		   -o cp (D3 ^ y) (R3 ^ k)).

% 0
% no zeroI
zeroECP : cp (zeroE ^ D1 ^ ())
	   (cut ^ R1 ^ ([l^left (zero)] zeroL ^ () ^ l))
	   o- cp D1 R1
	   o- <T>.

%%% Exponentials

% A -> B
impICP : cp (impI ^ D1) (impR ^ R1)
	  o- ({u:nd A} {l:left A}
		cp u (init ^ l) -> cp (D1 u) (R1 l)).

impECP : cp (impE ^ D1 D2)
	  (cut! R2
	     ^ ([l:left A] cut ^ R1
		  ^ ([k^left (imp A B)]
		       impL (init ^ l) ^ ([r:left B] init ^ r) ^ k)))
	  o- cp D1 R1
	  <- cp D2 R2.

% ! A
bangICP : cp (bangI D1) (bangR R1)
	   <- cp D1 R1.

bangECP : cp (bangE ^ D1 ^ D2)
	   (cut ^ R1 ^ ([l^left (bang A)] bangL ^ R2 ^ l))
	   o- cp D1 R1
	   o- ({u:nd A} {l:left A}
		 cp u (init ^ l) -o cp (D2 u) (R2 l)).