% Linear Logic

%hlf.

o : type. %name o A.

% Additive connectives
% and    : o -> o -> o.  %infix right 11 and.
triv    : o -> o.  

% top    : o.

conc : o -> @type. %name conc CONC.
hyp : o -> @type. %name hyp HYP.

%% Inference Rules

trivl : (hyp (triv A) -o conc C) o- (hyp A -o conc C).
% trivr : conc (triv A) o- conc A.

% andl1 : (hyp (A and B) -o conc C)
%         o- (hyp A -o conc C).
% andl2 : (hyp (A and B) -o conc C)
%        o- (hyp B -o conc C).
% andr : {a : w} 
% 	conc (A and B) @ a
% 	<- conc B @ a
% 	<- conc A @ a.

% topr : {a : w} conc top @ a.

% axiom : hyp A -o conc A.

%%% Cut admissibility

ca : {A : o}
      conc A @ AA
      -> (hyp A -o conc C) @ BB
      -> conc C @ (AA * BB)
      -> type.

%% Principal Cuts

% ca_triv : ca (triv A) (trivr ^ D) 
%	   ([h:^ (hyp (triv A))] trivl ^ E ^ h) F
%	   <- ca A D E F.

% ca_and1 : ca (A1 and A2) (andr ^ D1 D2) 
% 	   ([h:^ (hyp (A1 and A2))] andl1 ^ E ^ h) F
% 	   <- ca A1 D1 E F.


% ca_and2 : ca (A1 and A2) (andr ^ D1 D2) 
% 	   ([h :^ (hyp (A1 and A2))] andl2 ^ E ^ h) F
% 	   <- ca A2 D2 E F.

% %% D-commutative left

cad_trivl  : ca A (trivl ^ D1 ^ H) E (trivl ^ D1' ^ H)
	      <- {a : w} {h1: hyp B1 @ a} ca A (D1 ^ h1) E (D1' ^ h1).

% cad_andl1  : ca A (andl1 ^ D1 ^ H) E (andl1 ^ D1' ^ H)
% 	      <- {a : w} {h1: hyp B1 @ a} ca A (D1 ^ h1) E (D1' ^ h1).


% cad_andl2  : ca A (andl2 ^ D2 ^ H) E (andl2 ^ D2' ^ H)
% 	      <- {a : w} {h2:hyp B2 @ a} ca A (D2 ^ h2) E (D2' ^ h2).

% %% E-commutative right

% cae_trivr : ca A D ([h:^ (hyp A)] trivr ^ (E ^ h)) (trivr ^ E')
%	    <- ca A D E E'.


% cae_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'.

% cae_topr : {D:conc A @ P} ca A D ([a:w][h: (hyp A) @ a] topr (Q * a)) (topr (Q * P)).

%% E-commutative left

cae_trivl: ca A D ([a] [x:hyp A @ a] trivl ^ ([b] [y:hyp B @ b] E a x b y) ^ H) (trivl ^ F' ^ H)
	    <- ({b} {y:hyp B @ b} ca A D ([x:^ (hyp A)] E ^ x ^ y) (F' ^ y)).

% cae_andl1: ca A D ([a] [x:hyp A @ a] andl1 ^ ([b] [y:hyp B @ b] E a x b y) ^ H) (andl1 ^ F' ^ H)
% 	    <- ({b} {y:hyp B @ b} ca A D ([x:^ (hyp A)] E ^ x ^ y) (F' ^ y)).

% cae_andl2: ca A D ([a] [x:hyp A @ a] andl2 ^ ([b] [y:hyp B @ b] E a x b y) ^ H) (andl2 ^ F' ^ H)
% 	    <- ({b} {y:hyp B @ b} ca A D ([x:^ (hyp A)] E ^ x ^ y) (F' ^ y)).


%% Axiom cases

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

% ca_axiom_r : ca A D axiom D.

%block b : some {A : o} block {a : w} {x : hyp A a}.

%mode (ca +A +D +E -F).
%worlds (b) (ca _ _ _ _).
%total {A [D E]} (ca A D E _).