Cut Elimination Algorithm

%%% Classical Linear Logic
%%% Admissibility of Cut in the cut-free sequent calculus
%%% Author: Frank Pfenning

ct  : o -> type.
cut : {A:o} (pos A -o #) -o (neg A -o #) -o ct A.

ct! : o -> type.
cut!: {A:o} (pos A -o #) -> (neg! A -> #) -o ct! A.

ct? : o -> type.
cut?: {A:o} (pos? A -> #) -o (neg A -o #) -> ct? A.

ad : (ct A & #) -> type.
ad!: (ct! A & #) -> type.
ad?: (ct? A & #) -> type.

% Axiom conversions

ad_axiom_l : ad (cut A ([p^] axiom N p) E , (E N)).

ad_axiom_r : ad (cut A D ([n^] axiom n P) , (D P)).

% Essential conversions, multiplicative

ad_times : ad (cut (A times B) ([p^] timesr D1 D2 p) ([n^] timesl E1 n) , F)
	    <- ({n2:neg B} ad (cut A D1 ([n1^] E1 n1 n2) , (E1' n2)))
	    <- ad (cut B D2 E1' , F).

ad_one   : ad (cut (one) ([p^] oner p) ([n^] onel E1 n) , E1).

% Essential conversions, additive

ad_and1 : ad (cut (A and B) ([p^] andr (D1 , D2) p) ([n^] andl1 E1 n) , F)
	   <- ad (cut A D1 E1 , F).

ad_and2 : ad (cut (A and B) ([p^] andr (D1 , D2) p) ([n^] andl2 E2 n) , F)
	   <- ad (cut B D2 E2 , F).

% No essential conversion for additive unit

% Essentional conversion, involution

ad_perp : ad (cut (perp A) ([p^] perpr D1 p) ([n^] perpl E1 n) , F)
	   <- ad (cut A E1 D1 , F).

% Essential conversions, modal

ad_! : ad (cut (! A) ([p^] !r D1! p) ([n^] !l E1 n) , F)
	<- ad! (cut! A D1! E1 , F).

ad_? : ad (cut (? A) ([p^] ?r D1 p) ([n^] ?l E1! n) , F)
	<- ad? (cut? A D1 E1! , F).

% Structural conversions

ad!_d  : ad! (cut! A D! ([n!] !d (E1 n!) n!) , F)
	  <- ({n1:neg A} ad! (cut! A D! ([n!] E1 n! n1) , (E1' n1)))
	  <- ad (cut A D! E1' , F).

ad?_r  : ad? (cut? A ([p?] ?d (D1 p?) p?) E! , F)
	  <- ({p1:pos A} ad? (cut? A ([p?] D1 p? p1) E! , (D1' p1)))
	  <- ad (cut A D1' E! , F).

%% Non-modal right commutative conversions

% No commutative conversions crossing axioms

% Commutative conversions crossing multiplicatives

adr_timesr1 : ad (cut A D ([n^] timesr (E1 n) E2 P) , (timesr E1' E2 P))
	       <- ({p1:pos B1} ad (cut A D ([n^] E1 n p1) , (E1' p1))).

adr_timesr2 : ad (cut A D ([n^] timesr E1 (E2 n) P) , (timesr E1 E2' P))
	       <- ({p2:pos B2} ad (cut A D ([n^] E2 n p2) , (E2' p2))).

adr_timesl  : ad (cut A D ([n^] timesl (E1 n) N) , (timesl E1' N))
	       <- ({n1:neg B1} {n2:neg B2}
		     ad (cut A D ([n^] E1 n n1 n2) , (E1' n1 n2))).

% No case for oner

adr_onel    : ad (cut A D ([n^] onel (E1 n) N) , (onel E1' N))
	       <- ad (cut A D E1 , E1').

% Commutative conversions crossing additives

adr_andr : ad (cut A D ([n^] andr ((E1 n) , (E2 n)) P) , (andr (E1' , E2') P))
	    <- ({p1:pos B1} ad (cut A D ([n^] E1 n p1) , (E1' p1)))
	    <- ({p2:pos B2} ad (cut A D ([n^] E2 n p2) , (E2' p2))).

adr_andl1 : ad (cut A D ([n^] andl1 (E1 n) N) , (andl1 E1' N))
	     <- ({n1:neg B1} ad (cut A D ([n^] E1 n n1) , (E1' n1))).

adr_andl2 : ad (cut A D ([n^] andl2 (E2 n) N) , (andl2 E2' N))
	     <- ({n2:neg B2} ad (cut A D ([n^] E2 n n2) , (E2' n2))).

adr_topr  : ad (cut A D ([n^] topr () P) , (topr () P)).

% no topl rule

% Commutative conversions crossing involution

adr_perpr : ad (cut A D ([n^] perpr (E1 n) P) , (perpr E1' P))
	     <- ({n1:neg B1} ad (cut A D ([n^] E1 n n1) , (E1' n1))).

adr_perpl : ad (cut A D ([n^] perpl (E1 n) N) , (perpl E1' N))
	     <- ({p1:pos B1} ad (cut A D ([n^] E1 n p1) , (E1' p1))).

% Commutative conversion crossing modal

% no adr_!r since there are no non-modal side formulas

% Meta-level weakening is required in next case!
adr_!l : ad (cut A D ([n^] !l (E1 n) N) , (!l E1' N))
	  <- ({n1!:neg! B1} ad (cut A D ([n^] E1 n n1!) , (E1' n1!))).

adr_!d : ad (cut A D ([n^] !d (E1 n) N!) , (!d E1' N!))
	  <- ({n1:neg B1} ad (cut A D ([n^] E1 n n1) , (E1' n1))).

% Meta-level weakening is required in next case!
adr_?r : ad (cut A D ([n^] ?r (E1 n) P) , (?r E1' P))
	  <- ({p1?:pos? B1} ad (cut A D ([n^] E1 n p1?) , (E1' p1?))).

% no adr_?l since there are no non-modal side formulas

adr_?d : ad (cut A D ([n^] ?d (E1 n) P?) , (?d E1' P?))
	  <- ({p1:pos B1} ad (cut A D ([n^] E1 n p1) , (E1' p1))).

%% Non-modal left commutative conversions

% No commutative conversions crossing axioms

adl_timesr1 : ad (cut A ([p^] timesr (D1 p) D2 P) E , (timesr D1' D2 P))
	       <- ({p1:pos B1} ad (cut A ([p^] D1 p p1) E , (D1' p1))).

adl_timesr2 : ad (cut A ([p^] timesr D1 (D2 p) P) E , (timesr D1 D2' P))
	       <- ({p2:pos B2} ad (cut A ([p^] D2 p p2) E , (D2' p2))).

adl_timesl  : ad (cut A ([p^] timesl (D1 p) N) E , (timesl D1' N))
	       <- ({n1:neg B1} {n2:neg B2}
		     ad (cut A ([p^] D1 p n1 n2) E , (D1' n1 n2))).

% No case for oner

adl_onel    : ad (cut A ([p^] onel (D1 p) N) E , (onel D1' N))
	       <- ad (cut A D1 E , D1').

% Commutative conversions crossing additives

adl_andr  : ad (cut A ([p^] andr ((D1 p) , (D2 p)) P) E , (andr (D1' , D2') P))
	     <- ({p1:pos B1} ad (cut A ([p^] D1 p p1) E , (D1' p1)))
	     <- ({p2:pos B2} ad (cut A ([p^] D2 p p2) E , (D2' p2))).

adl_andl1 : ad (cut A ([p^] andl1 (D1 p) N) E , (andl1 D1' N))
	     <- ({n1:neg B1} ad (cut A ([p^] D1 p n1) E , (D1' n1))).

adl_andl2 : ad (cut A ([p^] andl2 (D2 p) N) E , (andl2 D2' N))
	     <- ({n2:neg B1} ad (cut A ([p^] D2 p n2) E , (D2' n2))).

adl_topr  : ad (cut A ([p^] topr () P) E , (topr () P)).

% no topl rule

% Commutative conversions crossing involution

adl_perpr : ad (cut A ([p^] perpr (D1 p) P) E , (perpr D1' P))
	     <- ({n1:neg B1} ad (cut A ([p^] D1 p n1) E , (D1' n1))).

adl_perpl : ad (cut A ([p^] perpl (D1 p) N) E , (perpl D1' N))
	     <- ({p1:pos B1} ad (cut A ([p^] D1 p p1) E , (D1' p1))).

% Commutative conversions crossing modal

% no adl_!r since there are no non-modal side formulas

adl_!l : ad (cut A ([p^] !l (D1 p) N) E , (!l D1' N))
	  <- ({n1!:neg! B1} ad (cut A ([p^] D1 p n1!) E , (D1' n1!))).

adl_!d : ad (cut A ([p^] !d (D1 p) N!) E , (!d D1' N!))
	  <- ({n1:neg B1} ad (cut A ([p^] D1 p n1) E , (D1' n1))).

adl_?r : ad (cut A ([p^] ?r (D1 p) P) E , (?r D1' P))
	  <- ({p1?:pos? B1} ad (cut A ([p^] D1 p p1?) E , (D1' p1?))).

% no adl_?l since there are no non-modal side formulas

adl_?d : ad (cut A ([p^] ?d (D1 p) P?) E , (?d D1' P?))
	  <- ({p1:pos B1} ad (cut A ([p^] D1 p p1) E , (D1' p1))).

%% Right commutative !-conversions

% Axiom

ad!r_axiom : ad! (cut! A D! ([n!] axiom N P) , (axiom N P)).

% Multiplicative

ad!r_timesr : ad! (cut! A D! ([n!] timesr (E1 n!) (E2 n!) P) ,
	       (timesr E1' E2' P))
	       <- ({p1:pos B1} ad! (cut! A D! ([n!] E1 n! p1) , (E1' p1)))
	       <- ({p2:pos B2} ad! (cut! A D! ([n!] E2 n! p2) , (E2' p2))).

ad!r_timesl : ad! (cut! A D! ([n!] timesl (E1 n!) N) , (timesl E1' N))
	       <- ({n1:neg B1} {n2:neg B2}
		     ad! (cut! A D! ([n!] E1 n! n1 n2) , (E1' n1 n2))).

ad!r_oner   : ad! (cut! A D! ([n!] oner P) , (oner P)).

ad!r_onel   : ad! (cut! A D! ([n!] onel (E1 n!) N) , (onel E1' N))
	       <- ad! (cut! A D! E1 , E1').

% Additive

ad!r_andr   : ad! (cut! A D! ([n!] andr ((E1 n!) , (E2 n!)) P) , (andr (E1' , E2') P))
	       <- ({p1:pos B1} ad! (cut! A D! ([n!] E1 n! p1) , (E1' p1)))
	       <- ({p2:pos B2} ad! (cut! A D! ([n!] E2 n! p2) , (E2' p2))).

ad!r_andl1  : ad! (cut! A D! ([n!] andl1 (E1 n!) N) , (andl1 E1' N))
	       <- ({n1:neg B1} ad! (cut! A D! ([n!] E1 n! n1) , (E1' n1))).

ad!r_andl2  : ad! (cut! A D! ([n!] andl2 (E2 n!) N) , (andl1 E2' N))
	       <- ({n2:neg B2} ad! (cut! A D! ([n!] E2 n! n2) , (E2' n2))).

ad!r_topr   : ad! (cut! A D! ([n!] topr () P) , (topr () P)).

% no topl rule

% Involutions

ad!r_perpr  : ad! (cut! A D! ([n!] perpr (E1 n!) P) , (perpr E1' P))
	       <- ({n1:neg B1} ad! (cut! A D! ([n!] E1 n! n1) , (E1' n1))).

ad!r_perpl  : ad! (cut! A D! ([n!] perpl (E1 n!) N) , (perpl E1' N))
	       <- ({p1:pos B1} ad! (cut! A D! ([n!] E1 n! p1) , (E1' p1))).

% Modals

ad!r_!r : ad! (cut! A D! ([n!] !r (E1! n!) P) , (!r E1!' P))
	   <- ({p1:pos B1} ad! (cut! A D! ([n!] E1! n! p1) , (E1!' p1))).

ad!r_!l : ad! (cut! A D! ([n!] !l (E1 n!) N) , (!l E1' N))
	   <- ({n1!:neg! B1} ad! (cut! A D! ([n!] E1 n! n1!) , (E1' n1!))).

ad!r_!d : ad! (cut! A D! ([n!] !d (E1 n!) N!) , (!d E1' N!))
	   <- ({n1:neg B1} ad! (cut! A D! ([n!] E1 n! n1) , (E1' n1))).

ad!r_?r : ad! (cut! A D! ([n!] ?r (E1 n!) P) , (?r E1' P))
	   <- ({p1?:pos? B1} ad! (cut! A D! ([n!] E1 n! p1?) , (E1' p1?))).

ad!r_?l : ad! (cut! A D! ([n!] ?l (E1! n!) N) , (?l E1!' N))
	   <- ({n1:neg B1} ad! (cut! A D! ([n!] E1! n! n1) , (E1!' n1))).

ad!r_?d : ad! (cut! A D! ([n!] ?d (E1 n!) P?) , (?d E1' P?))
	   <- ({p1:pos B1} ad! (cut! A D! ([n!] E1 n! p1) , (E1' p1))).

%% No left commutative !-conversions, since there are no side formulas
%% Note: right commutative conversions or structural
%% conversions will always be applicable for ad!

%% No right commutative ?-conversion for the same reason

%% Left commutative ?-conversions

% Axiom

ad?l_axiom : ad? (cut? A ([p?] axiom N P) E! , (axiom N P)).

% Multiplicative

ad?l_timesr : ad? (cut? A ([p?] timesr (D1 p?) (D2 p?) P) E! , (timesr D1' D2' P))
	       <- ({p1:pos B1} ad? (cut? A ([p?] D1 p? p1) E! , (D1' p1)))
	       <- ({p2:pos B2} ad? (cut? A ([p?] D2 p? p2) E! , (D2' p2))).

ad?l_timesl : ad? (cut? A ([p?] timesl (D1 p?) N) E! , (timesl D1' N))
	       <- ({n1:neg B1} {n2:neg B2}
		     ad? (cut? A ([p?] D1 p? n1 n2) E! , (D1' n1 n2))).

ad?l_oner   : ad? (cut? A ([p?] oner P) E! , (oner P)).

ad?l_onel   : ad? (cut? A ([p?] onel (D1 p?) N) E! , (onel D1' N))
	       <- ad? (cut? A D1 E! , D1').

% Additive

ad?l_andr  : ad? (cut? A ([p?] andr ((D1 p?) , (D2 p?)) P) E! , (andr (D1' , D2') P))
	      <- ({p1:pos B1} ad? (cut? A ([p?] D1 p? p1) E! , (D1' p1)))
	      <- ({p2:pos B2} ad? (cut? A ([p?] D2 p? p2) E! , (D2' p2))).

ad?l_andl1 : ad? (cut? A ([p?] andl1 (D1 p?) N) E! , (andl1 D1' N))
	      <- ({n1:neg B1} ad? (cut? A ([p?] D1 p? n1) E! , (D1' n1))).

ad?l_andl2 : ad? (cut? A ([p?] andl2 (D2 p?) N) E! , (andl2 D2' N))
	      <- ({n2:neg B2} ad? (cut? A ([p?] D2 p? n2) E! , (D2' n2))).

ad?l_topr  : ad? (cut? A ([p?] topr () P) E! , (topr () P)).

% no topl rule

% Involutions

ad?l_perpr : ad? (cut? A ([p?] perpr (D1 p?) P) E! , (perpr D1' P))
	      <- ({n1:neg B1} ad? (cut? A ([p?] D1 p? n1) E! , (D1' n1))).

ad?l_perpl : ad? (cut? A ([p?] perpl (D1 p?) N) E! , (perpl D1' N))
	      <- ({p1:pos B1} ad? (cut? A ([p?] D1 p? p1) E! , (D1' p1))).

% Modals

ad?l_!r : ad? (cut? A ([p?] !r (D1! p?) P) E! , (!r  D1!' P))
	   <- ({p1:pos B1} ad? (cut? A ([p?] D1! p? p1) E! , (D1!' p1))).

ad?l_!l : ad? (cut? A ([p?] !l (D1 p?) N) E! , (!l D1' N))
	   <- ({n1!:neg! B1} ad? (cut? A ([p?] D1 p? n1!) E! , (D1' n1!))).

ad?l_!d : ad? (cut? A ([p?] !d (D1 p?) N!) E! , (!d D1' N!))
	   <- ({n1:neg B1} ad? (cut? A ([p?] D1 p? n1) E! , (D1' n1))).

ad?l_?r : ad? (cut? A ([p?] ?r (D1 p?) P) E! , (?r D1' P))
	   <- ({p1?:pos? B1} ad? (cut? A ([p?] D1 p? p1?) E! , (D1' p1?))).

ad?l_?l : ad? (cut? A ([p?] ?l (D1! p?) N) E! , (?l D1!' N))
	   <- ({n1:neg B1} ad? (cut? A ([p?] D1! p? n1) E! , (D1!' n1))).

ad?l_?d : ad? (cut? A ([p?] ?d (D1 p?) P?) E! , (?d D1' P?))
	   <- ({p1:pos B1} ad? (cut? A ([p?] D1 p? p1) E! , (D1' p1))).

Frank Pfenning