Sequent Derivations to Annotated Natural Deductions

%%% Translating Sequent Derivations to Annotated
%%% Natural Deductions in Minimal Linear Logic.

lv2i : (pos A -o #) -> intro A -> type.
lv2e : neg A -> elim A -> type.
lv2e! : neg! A -> elim A -> type.

%% Axioms and Cut

lv2i_axiom : lv2i ([p^pos A] axiom N p) (e2i E)
	      o- lv2e N E.

lv2i_cut : lv2i ([p^pos C] cut Q1 (Q2 p)) (I2 (i2e I1))
	    o- lv2i Q1 I1
	    o- ({n1:neg A} {u1:elim A}
		  lv2e n1 u1
		  -o lv2i ([p^pos C] Q2 p n1) (I2 u1)).

lv2i_cut! : lv2i ([p^pos C] cut! Q1 (Q2 p)) (!e' I2 (i2e (!i' I1)))
	     <- lv2i Q1 (I1:intro A)
	     o- ({n1!:neg! A} {u1!:elim A}
		   lv2e! n1! u1!
		   -> lv2i ([p^pos C] Q2 p n1!) (I2 u1!)).

%% Multiplicative Connectives

lv2i_impr : lv2i (impr Q1) (impi' I1)
	     o- ({n1:neg A} {u1:elim A}
		   lv2e n1 u1
		   -o lv2i (Q1 n1) (I1 u1)).

lv2i_impe : lv2i ([p^pos C] impl Q1 (Q2 p) N) (I2 (impe' I1 E))
	     o- lv2e N E
	     o- lv2i Q1 I1
	     o- ({n2:neg B} {u2:elim B}
		   lv2e n2 u2
		   -o lv2i ([p^pos C] Q2 p n2) (I2 u2)).

lv2i_timesr : lv2i (timesr Q1 Q2) (timesi' I1 I2)
	       o- lv2i Q1 I1
	       o- lv2i Q2 I2.

lv2i_timesl : lv2i ([p^pos C] timesl (Q1 p) N) (timese' I1 E)
	       o- lv2e N E
	       o- ({n1:neg A} {u1:elim A}
		     {n2:neg B} {u2:elim B}
		     lv2e n1 u1
		     -o lv2e n2 u2
		     -o lv2i ([p^pos C] Q1 p n1 n2) (I1 u1 u2)).

lv2i_oner : lv2i (oner) (onei').

lv2i_onee : lv2i ([p^pos C] onel (Q1 p) N) (onee' I1 E)
	     o- lv2e N E
	     o- lv2i Q1 I1.

%% Additive Connectives

lv2i_withr : lv2i (withr (Q1 , Q2)) (withi' (I1 , I2))
	      o- (lv2i Q1 I1
		    & lv2i Q2 I2).

lv2i_withl1 : lv2i ([p^pos C] withl1 (Q1 p) N) (I1 (withe1' E))
	       o- lv2e N E
	       o- ({n1:neg A} {u1:elim A}
		     lv2e n1 u1
		     -o lv2i ([p^pos C] Q1 p n1) (I1 u1)).

lv2i_withl2 : lv2i ([p^pos C] withl2 (Q2 p) N) (I2 (withe2' E))
	       o- lv2e N E
	       o- ({n2:neg B} {u2:elim B}
		     lv2e n2 u2
		     -o lv2i ([p^pos C] Q2 p n2) (I2 u2)).

lv2i_topr   : lv2i (topr ()) (topi' ())
	       o- <T>.

% no topl

lv2i_plusr1 : lv2i (plusr1 Q1) (plusi1' I1)
	      o- lv2i Q1 I1.

lv2i_plusr2 : lv2i (plusr2 Q2) (plusi2' I2)
	       o- lv2i Q2 I2.

lv2i_plusl : lv2i ([p^pos C] plusl (Q1 p , Q2 p) N) (pluse' (I1 , I2) E)
	      o- lv2e N E
	      o- ({n1:neg A} {u1:elim A}
		    lv2e n1 u1
		    -o lv2i ([p^pos C] Q1 p n1) (I1 u1))
		 & ({n2:neg B} {u2:elim B}
		      lv2e n2 u2
		      -o lv2i ([p^pos C] Q2 p n2) (I2 u2)).

% no zeroi

lv2i_zerol : lv2i ([p^pos C] zerol () N) (zeroe' () E)
	      o- lv2e N E
	      o- <T>.

%% Quantifiers

lv2i_forallr : lv2i (forallr Q1) (foralli' I1)
		o- ({a:i} lv2i (Q1 a) (I1 a)).

lv2i_foralll : lv2i ([p^pos C] foralll T (Q1 p) N)  (I1 (foralle' T E))
		o- lv2e N E
		o- ({n1} {u1}
		      lv2e n1 u1
		      -o lv2i ([p^pos C] Q1 p n1) (I1 u1)).

lv2i_existsr : lv2i (existsr T Q1) (existsi' T I1)
		o- lv2i Q1 I1.

lv2i_existsl : lv2i ([p^pos C] existsl (Q1 p) N) (existse' I1 E)
		o- lv2e N E
		o- ({a:i}
		      {n1:neg (A a)} {u1:elim (A a)}
		      lv2e n1 u1
		      -o lv2i ([p^pos C] Q1 p a n1) (I1 a u1)).

%% Exponentials

lv2i_!r : lv2i (!r Q1) (!i' I1)
	   <- lv2i Q1 I1.

lv2i_!l : lv2i ([p^pos C] !l (Q1 p) N) (!e' I1 E)
	   o- lv2e N E
	   o- ({n1!:neg! A} {u1!:elim A}
		 lv2e! n1! u1!
		 -> lv2i ([p^pos C] Q1 p n1!) (I1 u1!)).

lv2i_!d : lv2i ([p^pos C] !d (Q1 p) N!) (I1 U!)
	   o- lv2e! N! U!
	   o- ({n1:neg A} {u1:elim A}
		 lv2e n1 u1
		 -o lv2i ([p^pos C] Q1 p n1) (I1 u1)).

Frank Pfenning