Linear logic

The fact that the LF type theory uses only unrestricted assumptions has led some to assume that it cannot encode substructural logics such as linear logic. In fact, LF admits a very elegant encoding of linear logic, given below. The key idea is a judgement used to enforce the linear use of each linear assumption.

The Encoding

Syntax

(options removed from twelftag: hidden=“true”)

%%%%%  Syntax  %%%%%
%%%  Types  %%%
%sort tp %.
%name tp %.
%scope tp %term o %pi tp %-> tp %-> tp %.
%prec %right 7 -o %.
%term * %pi tp %-> tp %-> tp %.
%prec %right 10 * %.
%term & %pi tp %-> tp %-> tp %.
%prec %right 9 & %.
%term + %pi tp %-> tp %-> tp %.
%prec %right 8 + %.
%term ! %pi tp %-> tp %.
%term zero tp %.
%term top tp %.
%% 1 need not be primitive.
%define one tp ! top %.
%%%  Terms  %%%
%sort term %.
%name term %.
%term lam %pi (%pi term %-> term) %-> term %.
%term app %pi term %-> term %-> term %.
%term tensor %pi term %-> term %-> term %.
%term lett %pi term %-> (%pi term %-> term %-> term) %-> term %.
%term pair %pi term %-> term %-> term %.
%term pi1 %pi term %-> term %.
%term pi2 %pi term %-> term %.
%term in1 %pi term %-> term %.
%term in2 %pi term %-> term %.
%term case %pi term %-> (%pi term %-> term) %-> (%pi term %-> term) %-> term %.
%term bang %pi term %-> term %.
%term letb %pi term %-> (%pi term %-> term) %-> term %.
%term any %pi term %-> term %.
%term unit term %.
%% derived syntax for 1
%define star term bang unit %.
%define leto (%pi term %-> term %-> term) [t1] [t2] letb t1 ([x] t2) %.

Linearity

Linearity is enforced by employing a linearity judgement for each linear assumption. The linearity judgement ensures that a variable is used linearly (roughly speaking, exactly once) within its scope. (For an example of its use, see the rule of/lam for linear lambda abstraction below, which ensures that its argument is used linearly within its body.)

(options removed from twelftag: hidden=“true”)

%%%%%  Linearity  %%%%%
%sort linear {_ %pi term %-> term} %.

For example, a variable is used linearly in a single occurrence of that variable:

%term linear/var linear ([x] x) %.

A variable is used linearly in a lambda abstraction if it is used linearly in the body. (The abstraction’s argument must also be used linearly in the body, but that is handled separately, by the abstraction’s typing rule.)

%term linear/lam %pi (linear ([x] lam (M x))) %<- ({y} linear ([x] M x y)) %.

A variable is used linearly in application, if it is used linearly in one of the two subterms and does not appear at all in the other:

%term linear/app1 %pi (linear ([x] app (M1 x) M2)) %<- (linear M1) %.
%term linear/app2 %pi (linear ([x] app M1 (M2 x))) %<- (linear M2) %.

The remaining constructs use the same technique. Note that there is no rule for bang; no linear variable may appear within a bang. Also note that a linear variable need not appear within an any (as with unit); however, if it does appear, it must be used linearly.

%term linear/tensor1 %pi (linear ([x] tensor (M1 x) M2)) %<- (linear M1) %.
%term linear/tensor2 %pi (linear ([x] tensor M1 (M2 x))) %<- (linear M2) %.
%term linear/lett1 %pi (linear ([x] lett (M1 x) M2)) %<- (linear M1) %.
%term linear/lett2 %pi (linear ([x] lett M1 (M2 x))) %<- ({y} {z} linear ([x] M2 x y z)) %.
%term linear/pair %pi (linear ([x] pair (M1 x) (M2 x))) %<- (linear M1) %<- (linear M2) %.
%term linear/pi1 %pi (linear ([x] pi1 (M x))) %<- (linear M) %.
%term linear/pi2 %pi (linear ([x] pi2 (M x))) %<- (linear M) %.
%term linear/in1 %pi (linear ([x] in1 (M x))) %<- (linear M) %.
%term linear/in2 %pi (linear ([x] in2 (M x))) %<- (linear M) %.
%term linear/case1 %pi (linear ([x] case (M x) M1 M2)) %<- (linear M) %.
%term linear/case2
  %pi (linear ([x] case M (M1 x) (M2 x)))
  %<- ({y} linear ([x] M1 x y))
  %<- ({y} linear ([x] M2 x y)) %.
%term linear/letb1 %pi (linear ([x] letb (M1 x) M2)) %<- (linear M1) %.
%term linear/letb2 %pi (linear ([x] letb M1 (M2 x))) %<- ({y} linear ([x] M2 x y)) %.
%term linear/any1 %pi (linear ([x] any (M x))) %<- (linear M) %.
%term linear/any2 linear ([x] any M) %.
%term linear/unit linear ([x] unit) %.
%% derived rules for 1
%define linear/leto1 (%pi (linear ([x] leto (M1 x) M2)) %<- (linear M1)) [d] linear/letb1 d %.
%define linear/leto2 (%pi (linear ([x] leto M1 (M2 x))) %<- (linear M2)) [d] linear/letb2 ([y] d) %.

Typing rules

The typing rules are standard for linear logic, except that they must check that the linearity invariants are maintained. Thus, the typing rule for any construct that binds a linear variable (lam, for example) has a premise (or premises) ensuring that such variable(s) are used linearly in their scope. However, letb, which binds an unrestricted variable, does not check for linear usage of that variable.

(options removed from twelftag: hidden=“true”)

%%%%%  Typing Rules  %%%%%
%sort of {_ term} {_ tp} %.
%term of/lam
  %pi (of (lam M) (T1 -o T2))
  %<- ({x} %pi (of x T1) %-> (of (M x) T2))
  %<- (linear M) %.
%term of/app %pi (of (app M1 M2) T2) %<- (of M1 (T1 -o T2)) %<- (of M2 T1) %.
%term of/tensor %pi (of (tensor M1 M2) (T1 * T2)) %<- (of M1 T1) %<- (of M2 T2) %.
%term of/lett
  %pi (of (lett M1 M2) T)
  %<- (of M1 (T1 * T2))
  %<- ({x} %pi (of x T1) %-> ({y} %pi (of y T2) %-> (of (M2 x y) T)))
  %<- ({y} linear ([x] M2 x y))
  %<- ({x} linear ([y] M2 x y)) %.
%term of/pair %pi (of (pair M1 M2) (T1 & T2)) %<- (of M1 T1) %<- (of M2 T2) %.
%term of/pi1 %pi (of (pi1 M) T1) %<- (of M (T1 & T2)) %.
%term of/pi2 %pi (of (pi2 M) T2) %<- (of M (T1 & T2)) %.
%term of/in1 %pi (of (in1 M) (T1 + T2)) %<- (of M T1) %.
%term of/in2 %pi (of (in2 M) (T1 + T2)) %<- (of M T2) %.
%term of/case
  %pi (of (case M M1 M2) T)
  %<- (of M (T1 + T2))
  %<- ({x} %pi (of x T1) %-> (of (M1 x) T))
  %<- ({x} %pi (of x T2) %-> (of (M2 x) T))
  %<- (linear M1)
  %<- (linear M2) %.
%term of/bang %pi (of (bang M) (! T)) %<- (of M T) %.
%term of/letb
  %pi (of (letb M1 M2) T2)
  %<- (of M1 (! T1))
  %<- ({x} %pi (of x T1) %-> (of (M2 x) T2)) %.
%term of/any %pi (of (any M) T) %<- (of M zero) %.
%term of/unit of unit top %.
%% derived rules for 1
%define of/star (of star one) of/bang of/unit %.
%define of/leto (%pi (of (leto M1 M2) T) %<- (of M1 one) %<- (of M2 T)) [d2] [d1] of/letb ([x] [d] d2) d1 %.

Subject Reduction

As a metatheoretic example, we may prove the subject reduction property using this encoding. First we define the relevant worlds:

(options removed from twelftag: hidden=“true”)

%%%%%  Worlds  %%%%%
%block block {x term}%.
%block bind [t tp] {x term} {d of x t}%.

Next we define reduction:

(options removed from twelftag: hidden=“true”)

%%%%%  Reduction  %%%%%
%sort reduce {_ term} {_ term} %.
%term red/refl reduce M M %.
%term red/trans %pi (reduce M1 M3) %<- (reduce M1 M2) %<- (reduce M2 M3) %.
%% beta rules
%term red/beta reduce (app (lam M1) M2) (M1 M2) %.
%term red/beta* reduce (lett (tensor M1 M2) M) (M M1 M2) %.
%term red/beta&1 reduce (pi1 (pair M1 M2)) M1 %.
%term red/beta&2 reduce (pi2 (pair M1 M2)) M2 %.
%term red/beta+1 reduce (case (in1 M) M1 M2) (M1 M) %.
%term red/beta+2 reduce (case (in2 M) M1 M2) (M2 M) %.
%term red/beta! reduce (letb (bang M1) M2) (M2 M1) %.
%% compatibility
%term red/lam %pi (reduce (lam M) (lam M')) %<- ({x} reduce (M x) (M' x)) %.
%term red/app %pi (reduce (app M1 M2) (app M1' M2')) %<- (reduce M1 M1') %<- (reduce M2 M2') %.
%term red/tensor
  %pi (reduce (tensor M1 M2) (tensor M1' M2'))
  %<- (reduce M1 M1')
  %<- (reduce M2 M2') %.
%term red/lett
  %pi (reduce (lett M1 M2) (lett M1' M2'))
  %<- (reduce M1 M1')
  %<- ({x} {y} reduce (M2 x y) (M2' x y)) %.
%term red/pair %pi (reduce (pair M1 M2) (pair M1' M2')) %<- (reduce M1 M1') %<- (reduce M2 M2') %.
%term red/pi1 %pi (reduce (pi1 M) (pi1 M')) %<- (reduce M M') %.
%term red/pi2 %pi (reduce (pi2 M) (pi2 M')) %<- (reduce M M') %.
%term red/in1 %pi (reduce (in1 M) (in1 M')) %<- (reduce M M') %.
%term red/in2 %pi (reduce (in2 M) (in2 M')) %<- (reduce M M') %.
%term red/case
  %pi (reduce (case M M1 M2) (case M' M1' M2'))
  %<- (reduce M M')
  %<- ({x} reduce (M1 x) (M1' x))
  %<- ({x} reduce (M2 x) (M2' x)) %.
%term red/bang %pi (reduce (bang M) (bang M')) %<- (reduce M M') %.
%term red/letb
  %pi (reduce (letb M1 M2) (letb M1' M2'))
  %<- (reduce M1 M1')
  %<- ({x} reduce (M2 x) (M2' x)) %.
%term red/any %pi (reduce (any M) (any M')) %<- (reduce M M') %.
%% commuting conversions
%term red/app/lett reduce (app (lett M1 M2) M3) (lett M1 ([x] [y] app (M2 x y) M3)) %.
%term red/app/case reduce (app (case M1 M2a M2b) M3) (case M1 ([x] app (M2a x) M3) ([x] app (M2b x) M3)) %.
%term red/app/letb reduce (app (letb M1 M2) M3) (letb M1 ([x] app (M2 x) M3)) %.
%term red/app/any reduce (app (any M1) M2) (any M1) %.
%term red/pi1/lett reduce (pi1 (lett M1 M2)) (lett M1 ([x] [y] pi1 (M2 x y))) %.
%term red/pi1/case reduce (pi1 (case M1 M2a M2b)) (case M1 ([x] pi1 (M2a x)) ([x] pi1 (M2b x))) %.
%term red/pi1/letb reduce (pi1 (letb M1 M2)) (letb M1 ([x] pi1 (M2 x))) %.
%term red/pi1/any reduce (pi1 (any M)) (any M) %.
%term red/pi2/lett reduce (pi2 (lett M1 M2)) (lett M1 ([x] [y] pi2 (M2 x y))) %.
%term red/pi2/case reduce (pi2 (case M1 M2a M2b)) (case M1 ([x] pi2 (M2a x)) ([x] pi2 (M2b x))) %.
%term red/pi2/letb reduce (pi2 (letb M1 M2)) (letb M1 ([x] pi2 (M2 x))) %.
%term red/pi2/any reduce (pi2 (any M)) (any M) %.
%term red/lett/lett reduce (lett (lett M1 M2) M3) (lett M1 ([x] [y] lett (M2 x y) M3)) %.
%term red/lett/case reduce (lett (case M1 M2a M2b) M3) (case M1 ([x] lett (M2a x) M3) ([x] lett (M2b x) M3)) %.
%term red/lett/letb reduce (lett (letb M1 M2) M3) (letb M1 ([x] lett (M2 x) M3)) %.
%term red/lett/any reduce (lett (any M1) M2) (any M1) %.
%term red/case/lett reduce (case (lett M1 M2) M3a M3b) (lett M1 ([x] [y] case (M2 x y) M3a M3b)) %.
%term red/case/case reduce (case (case M1 M2a M2b) M3a M3b) (case M1 ([x] case (M2a x) M3a M3b) ([x] case (M2b x) M3a M3b)) %.
%term red/case/letb reduce (case (letb M1 M2) M3a M3b) (letb M1 ([x] case (M2 x) M3a M3b)) %.
%term red/case/any reduce (case (any M1) M2a M2b) (any M1) %.
%term red/letb/lett reduce (letb (lett M1 M2) M3) (lett M1 ([x] [y] letb (M2 x y) M3)) %.
%term red/letb/case reduce (letb (case M1 M2a M2b) M3) (case M1 ([x] letb (M2a x) M3) ([x] letb (M2b x) M3)) %.
%term red/letb/letb reduce (letb (letb M1 M2) M3) (letb M1 ([x] letb (M2 x) M3)) %.
%term red/letb/any reduce (letb (any M1) M2) (any M1) %.
%term red/any/lett reduce (any (lett M1 M2)) (lett M1 ([x] [y] any (M2 x y))) %.
%term red/any/case reduce (any (case M1 M2a M2b)) (case M1 ([x] any (M2a x)) ([x] any (M2b x))) %.
%term red/any/letb reduce (any (letb M1 M2)) (letb M1 ([x] any (M2 x))) %.
%term red/any/any reduce (any (any M)) (any M) %.

Next we define syntactic equality and establish some uninteresting properties about it.

(options removed from twelftag: hidden=“true”)

%%%%%  Equality  %%%%%
%sort tp-eq {_ tp} {_ tp} %.
%term tp-eq/i tp-eq T T %.
%sort term-eq {_ term} {_ term} %.
%term term-eq/i term-eq M M %.

(options removed from twelftag: hidden=“true”)

%%%%%  Cons Lemmas  %%%%%
%sort any-resp {_ term-eq M M'} {_ term-eq (any M) (any M')} %.
%mode any-resp %in %out %.
%term _ any-resp term-eq/i term-eq/i %.
%worlds (block bind) (any-resp _ _) %.
%total {} (any-resp _ _) %.
%sort app-resp {_ term-eq M1 M1'} {_ term-eq M2 M2'} {_ term-eq (app M1 M2) (app M1' M2')} %.
%mode app-resp %in %in %out %.
%term _ app-resp term-eq/i term-eq/i term-eq/i %.
%worlds (block bind) (app-resp _ _ _) %.
%total {} (app-resp _ _ _) %.
%sort bang-resp {_ term-eq M M'} {_ term-eq (bang M) (bang M')} %.
%mode bang-resp %in %out %.
%term _ bang-resp term-eq/i term-eq/i %.
%worlds (block bind) (bang-resp _ _) %.
%total {} (bang-resp _ _) %.
%sort case-resp {_ term-eq M1 M1'} {_ {x} term-eq (M2 x) (M2' x)} {_ {x} term-eq (M3 x) (M3' x)} {_ term-eq (case M1 M2 M3) (case M1' M2' M3')} %.
%mode case-resp %in %in %in %out %.
%term _ case-resp term-eq/i ([_] term-eq/i) ([_] term-eq/i) term-eq/i %.
%worlds (block bind) (case-resp _ _ _ _) %.
%total {} (case-resp _ _ _ _) %.
%sort in1-resp {_ term-eq M M'} {_ term-eq (in1 M) (in1 M')} %.
%mode in1-resp %in %out %.
%term _ in1-resp term-eq/i term-eq/i %.
%worlds (block bind) (in1-resp _ _) %.
%total {} (in1-resp _ _) %.
%sort in2-resp {_ term-eq M M'} {_ term-eq (in2 M) (in2 M')} %.
%mode in2-resp %in %out %.
%term _ in2-resp term-eq/i term-eq/i %.
%worlds (block bind) (in2-resp _ _) %.
%total {} (in2-resp _ _) %.
%sort lam-resp {_ {x} term-eq (M x) (M' x)} {_ term-eq (lam M) (lam M')} %.
%mode lam-resp %in %out %.
%term _ lam-resp ([x] term-eq/i) term-eq/i %.
%worlds (block bind) (lam-resp _ _) %.
%total {} (lam-resp _ _) %.
%sort letb-resp {_ term-eq M1 M1'} {_ {x} term-eq (M2 x) (M2' x)} {_ term-eq (letb M1 M2) (letb M1' M2')} %.
%mode letb-resp %in %in %out %.
%term _ letb-resp term-eq/i ([x] term-eq/i) term-eq/i %.
%worlds (block bind) (letb-resp _ _ _) %.
%total {} (letb-resp _ _ _) %.
%sort lett-resp {_ term-eq M1 M1'} {_ {x} {y} term-eq (M2 x y) (M2' x y)} {_ term-eq (lett M1 M2) (lett M1' M2')} %.
%mode lett-resp %in %in %out %.
%term _ lett-resp term-eq/i ([x] [y] term-eq/i) term-eq/i %.
%worlds (block bind) (lett-resp _ _ _) %.
%total {} (lett-resp _ _ _) %.
%sort pair-resp {_ term-eq M1 M1'} {_ term-eq M2 M2'} {_ term-eq (pair M1 M2) (pair M1' M2')} %.
%mode pair-resp %in %in %out %.
%term _ pair-resp term-eq/i term-eq/i term-eq/i %.
%worlds (block bind) (pair-resp _ _ _) %.
%total {} (pair-resp _ _ _) %.
%sort pi1-resp {_ term-eq M M'} {_ term-eq (pi1 M) (pi1 M')} %.
%mode pi1-resp %in %out %.
%term _ pi1-resp term-eq/i term-eq/i %.
%worlds (block bind) (pi1-resp _ _) %.
%total {} (pi1-resp _ _) %.
%sort pi2-resp {_ term-eq M M'} {_ term-eq (pi2 M) (pi2 M')} %.
%mode pi2-resp %in %out %.
%term _ pi2-resp term-eq/i term-eq/i %.
%worlds (block bind) (pi2-resp _ _) %.
%total {} (pi2-resp _ _) %.
%sort tensor-resp {_ term-eq M1 M1'} {_ term-eq M2 M2'} {_ term-eq (tensor M1 M2) (tensor M1' M2')} %.
%mode tensor-resp %in %in %out %.
%term _ tensor-resp term-eq/i term-eq/i term-eq/i %.
%worlds (block bind) (tensor-resp _ _ _) %.
%total {} (tensor-resp _ _ _) %.
%%%%%  Respects Lemmas  %%%%%
%sort linear-resp {_ {x} term-eq (M1 x) (M2 x)} {_ linear M1} {_ linear M2} %.
%mode linear-resp %in %in %out %.
%term _ linear-resp ([x] term-eq/i) D D %.
%worlds (block bind) (linear-resp _ _ _) %.
%total {} (linear-resp _ _ _) %.
%sort reduce-resp {_ term-eq M1 M1'} {_ term-eq M2 M2'} {_ reduce M1 M2} {_ reduce M1' M2'} %.
%mode reduce-resp %in %in %in %out %.
%term _ reduce-resp term-eq/i term-eq/i D D %.
%worlds (block bind) (reduce-resp _ _ _ _) %.
%total {} (reduce-resp _ _ _ _) %.
%reduces <= D1 D2 (reduce-resp _ _ D2 D1) %.
%%%%%  Down to Business  %%%%%

Next we prove an important lemma: when a variable x is used linearly in a term M1, and M1 is substituted for a linear variable in a term M2 that does not mention x, than x is used linearly in the result.

%sort compose-linear {_ linear M1} {_ linear M2} {_ linear ([x] M1 (M2 x))} %.
%mode compose-linear %in %in %out %.

(options removed from twelftag: hidden=“true”)

%term _ compose-linear linear/var D D %.
%term _
  %pi (compose-linear (linear/lam D1) D2 (linear/lam D))
  %<- ({y} compose-linear (D1 y) D2 (D y)) %.
%term _
  %pi (compose-linear (linear/app1 D1) D2 (linear/app1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/app2 D1) D2 (linear/app2 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/tensor1 D1) D2 (linear/tensor1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/tensor2 D1) D2 (linear/tensor2 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/lett1 D1) D2 (linear/lett1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/lett2 D1) D2 (linear/lett2 D))
  %<- ({y} {z} compose-linear (D1 y z) D2 (D y z)) %.
%term _
  %pi (compose-linear (linear/pair D1b D1a) D2 (linear/pair Db Da))
  %<- (compose-linear D1a D2 Da)
  %<- (compose-linear D1b D2 Db) %.
%term _
  %pi (compose-linear (linear/pi1 D1) D2 (linear/pi1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/pi2 D1) D2 (linear/pi2 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/in1 D1) D2 (linear/in1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/in2 D1) D2 (linear/in2 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/case1 D1) D2 (linear/case1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/case2 D1b D1a) D2 (linear/case2 Db Da))
  %<- ({y} compose-linear (D1a y) D2 (Da y))
  %<- ({y} compose-linear (D1b y) D2 (Db y)) %.
%term _
  %pi (compose-linear (linear/letb1 D1) D2 (linear/letb1 D))
  %<- (compose-linear D1 D2 D) %.
%term _
  %pi (compose-linear (linear/letb2 D1) D2 (linear/letb2 D))
  %<- ({y} compose-linear (D1 y) D2 (D y)) %.
%term _
  %pi (compose-linear (linear/any1 D1) D2 (linear/any1 D))
  %<- (compose-linear D1 D2 D) %.
%term _ compose-linear linear/any2 _ linear/any2 %.
%term _ compose-linear linear/unit _ linear/unit %.
%worlds (block bind) (compose-linear _ _ _) %.
%total D (compose-linear D _ _) %.

Next we prove a technical lemma. It states that if x does not appear in M1, and M1 reduces to M2, then x does not appear in M2.

%sort reduce-closed {_ {x term} reduce M1 (M2 x)} {_ {x term} term-eq M2' (M2 x)} %.
%mode reduce-closed %in %out %.

(options removed from twelftag: hidden=“true”)

%term _ reduce-closed ([x] red/refl) ([x] term-eq/i) %.
%sort reduce-closed!trans {_ {x term} term-eq M1' (M1 x)} {_ {x term} reduce (M1 x) (M2 x)} {_ {x term} term-eq M2' (M2 x)} %.
%mode reduce-closed!trans %in %in %out %.
%term _
  %pi (reduce-closed ([x] red/trans (D2 x) (D1 x)) Deq2)
  %<- (reduce-closed D1 Deq1)
  %<- (reduce-closed!trans Deq1 D2 Deq2) %.
%term _ %pi (reduce-closed!trans ([x] term-eq/i) D Deq) %<- (reduce-closed D Deq) %.
%term _ reduce-closed ([x] red/beta) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta*) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta&1) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta&2) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta+1) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta+2) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/beta!) ([x] term-eq/i) %.
%term _
  %pi (reduce-closed ([x] red/lam (Dred x)) Deq')
  %<- ({y} reduce-closed ([x] Dred x y) ([x] Deq x y))
  %<- ({x} lam-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/app (Dred2 x) (Dred1 x)) Deq)
  %<- (reduce-closed Dred1 Deq1)
  %<- (reduce-closed Dred2 Deq2)
  %<- ({x} app-resp (Deq1 x) (Deq2 x) (Deq x)) %.
%term _
  %pi (reduce-closed ([x] red/tensor (Dred2 x) (Dred1 x)) Deq)
  %<- (reduce-closed Dred1 Deq1)
  %<- (reduce-closed Dred2 Deq2)
  %<- ({x} tensor-resp (Deq1 x) (Deq2 x) (Deq x)) %.
%term _
  %pi (reduce-closed ([x] red/lett (Dred2 x) (Dred1 x)) Deq)
  %<- (reduce-closed Dred1 Deq1)
  %<- ({y} {z} reduce-closed ([x] Dred2 x y z) ([x] Deq2 x y z))
  %<- ({x} lett-resp (Deq1 x) (Deq2 x) (Deq x)) %.
%term _
  %pi (reduce-closed ([x] red/pair (Dred2 x) (Dred1 x)) Deq)
  %<- (reduce-closed Dred1 Deq1)
  %<- (reduce-closed Dred2 Deq2)
  %<- ({x} pair-resp (Deq1 x) (Deq2 x) (Deq x)) %.
%term _
  %pi (reduce-closed ([x] red/pi1 (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} pi1-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/pi2 (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} pi2-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/in1 (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} in1-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/in2 (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} in2-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/case (Dred3 x) (Dred2 x) (Dred1 x)) Deq')
  %<- (reduce-closed Dred1 Deq1)
  %<- ({y} reduce-closed ([x] Dred2 x y) ([x] Deq2 x y))
  %<- ({y} reduce-closed ([x] Dred3 x y) ([x] Deq3 x y))
  %<- ({x} case-resp (Deq1 x) (Deq2 x) (Deq3 x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/bang (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} bang-resp (Deq x) (Deq' x)) %.
%term _
  %pi (reduce-closed ([x] red/letb (Dred2 x) (Dred1 x)) Deq)
  %<- (reduce-closed Dred1 Deq1)
  %<- ({y} reduce-closed ([x] Dred2 x y) ([x] Deq2 x y))
  %<- ({x} letb-resp (Deq1 x) (Deq2 x) (Deq x)) %.
%term _
  %pi (reduce-closed ([x] red/any (Dred x)) Deq')
  %<- (reduce-closed Dred Deq)
  %<- ({x} any-resp (Deq x) (Deq' x)) %.
%term _ reduce-closed ([x] red/app/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/app/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/app/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/app/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi1/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi1/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi1/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi1/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi2/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi2/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi2/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/pi2/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/lett/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/lett/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/lett/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/lett/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/case/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/case/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/case/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/case/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/letb/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/letb/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/letb/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/letb/any) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/any/lett) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/any/case) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/any/letb) ([x] term-eq/i) %.
%term _ reduce-closed ([x] red/any/any) ([x] term-eq/i) %.
%worlds (block bind) (reduce-closed _ _) (reduce-closed!trans _ _ _) %.
%total (D1 D2) (reduce-closed D1 _) (reduce-closed!trans _ D2 _) %.

With these lemmas in hand, we can prove the subject reduction theorem. In fact, there are two theorems to be proved simultaneously. One (sr) states that types are preserved by reduction, and the other (srl) states that linearity is preserved by reduction.

%sort srl {_ {x} reduce (M x) (M' x)} {_ {x} %pi (of x T) %-> (of (M x) T')} {_ linear M} {_ linear M'} %.
%sort sr {_ reduce M M'} {_ of M T} {_ of M' T} %.
%mode srl %in %in %in %out %.
%mode sr %in %in %out %.

(options removed from twelftag: hidden=“true”)

%scope sr %term refl srl ([x] red/refl) _ D D %.
%term trans
  %pi (srl ([x] red/trans (Dred23 x) (Dred12 x)) Dof1 Dlin1 Dlin3)
  %<- (srl Dred12 Dof1 Dlin1 Dlin2)
  %<- ({x} {d} sr (Dred12 x) (Dof1 x d) (Dof2 x d))
  %<- (srl Dred23 Dof2 Dlin2 Dlin3) %.
%scope sr %term beta1 srl ([x] %the (reduce (app (lam (M1 x)) M2) _) red/beta) ([x] [d] of/app (%the (of _ T2) (Dof2 x d)) (of/lam (Dlin1 x) (Dof1 x d))) (linear/app1 (linear/lam Dlin)) (Dlin M2) %.
%term beta2
  %pi (srl ([x] %the (reduce (app (lam M1) (M2 x)) _) red/beta) ([x] [d] of/app (%the (of _ T2) (Dof2 x d)) (of/lam (Dlin1 x) (Dof1 x d))) (linear/app2 Dlin) Dlin')
  %<- (compose-linear (Dlin1 unit) Dlin Dlin') %.
%scope sr %term bet*11
  %pi (srl ([x] %the (reduce (lett (tensor (M1 x) M2) M) _) red/beta*) ([x] [d] of/lett (Dlin2 x) (Dlin1 x) (Dof2 x d) (%the (of _ (T1 * T2)) (Dof1 x d))) (linear/lett1 (linear/tensor1 Dlin)) Dlin')
  %<- (compose-linear (Dlin1 unit M2) Dlin Dlin') %.
%term bet*12
  %pi (srl ([x] %the (reduce (lett (tensor M1 (M2 x)) M) _) red/beta*) ([x] [d] of/lett (Dlin2 x) (Dlin1 x) (Dof2 x d) (%the (of _ (T1 * T2)) (Dof1 x d))) (linear/lett1 (linear/tensor2 Dlin)) Dlin')
  %<- (compose-linear (Dlin2 unit M1) Dlin Dlin') %.
%scope sr %term bet*2 srl ([x] %the (reduce (lett (tensor M1 M2) (M x)) _) red/beta*) ([x] [d] of/lett (Dlin2 x) (Dlin1 x) (Dof2 x d) (%the (of _ (T1 * T2)) (Dof1 x d))) (linear/lett2 Dlin) (Dlin M1 M2) %.
%term beta&1 srl ([x] %the (reduce (pi1 (pair (M1 x) (M2 x))) _) red/beta&1) ([x] [d] of/pi1 (of/pair (%the (of _ T1) (Dof2 x d)) (%the (of _ T2) (Dof1 x d)))) (linear/pi1 (linear/pair Dlin2 Dlin1)) Dlin1 %.
%scope sr %term beta&2 srl ([x] %the (reduce (pi2 (pair (M1 x) (M2 x))) _) red/beta&2) ([x] [d] of/pi2 (of/pair (%the (of _ T1) (Dof2 x d)) (%the (of _ T2) (Dof1 x d)))) (linear/pi2 (linear/pair Dlin2 Dlin1)) Dlin2 %.
%term bt+1-1
  %pi (srl ([x] %the (reduce (case (in1 (M x)) M1 M2) _) red/beta+1) ([x] [d] of/case (Dlin2 x) (Dlin1 x) _ _ (%the (of _ (T1 + T2)) _)) (linear/case1 (linear/in1 Dlin)) Dlin')
  %<- (compose-linear (Dlin1 unit) Dlin Dlin') %.
%scope sr %term bt+1-2 srl ([x] %the (reduce (case (in1 M) (M1 x) (M2 x)) _) red/beta+1) ([x] [d] of/case (Dlin2 x) (Dlin1 x) _ _ (%the (of _ (T1 + T2)) _)) (linear/case2 Dlin2' Dlin1') (Dlin1' M) %.
%term bt+2-1
  %pi (srl ([x] %the (reduce (case (in2 (M x)) M1 M2) _) red/beta+2) ([x] [d] of/case (Dlin2 x) (Dlin1 x) _ _ (%the (of _ (T1 + T2)) _)) (linear/case1 (linear/in2 Dlin)) Dlin')
  %<- (compose-linear (Dlin2 unit) Dlin Dlin') %.
%scope sr %term bt+2-2 srl ([x] %the (reduce (case (in2 M) (M1 x) (M2 x)) _) red/beta+2) ([x] [d] of/case (Dlin2 x) (Dlin1 x) _ _ (%the (of _ (T1 + T2)) _)) (linear/case2 Dlin2' Dlin1') (Dlin2' M) %.
%term beta! srl ([x] %the (reduce (letb (bang M1) (M2 x)) _) red/beta!) ([x] [d] of/letb (Dof2 x d) (of/bang (%the (of _ T) (Dof1 x d)))) (linear/letb2 Dlin) (Dlin M1) %.
%scope sr %term lam
  %pi (srl ([x] red/lam (Dred x)) ([x] [d] of/lam (Dlin1 x) (Dof x d)) (linear/lam Dlin) (linear/lam Dlin'))
  %<- ({y} {e} srl ([x] Dred x y) ([x] [d] Dof x d y e) (Dlin y) (Dlin' y)) %.
%term app1
  %pi (srl ([x] red/app (Dred2 x) (Dred1 x)) ([x] [d] of/app (Dof2 x d) (Dof1 x d)) (linear/app1 Dlin) Dlin'')
  %<- (srl Dred1 Dof1 Dlin Dlin')
  %<- (reduce-closed Dred2 Deq)
  %<- ({x} app-resp term-eq/i (Deq x) (Deq' x))
  %<- (linear-resp Deq' (linear/app1 Dlin') Dlin'') %.
%scope sr %term app2
  %pi (srl ([x] red/app (Dred2 x) (Dred1 x)) ([x] [d] of/app (Dof2 x d) (Dof1 x d)) (linear/app2 Dlin) Dlin'')
  %<- (srl Dred2 Dof2 Dlin Dlin')
  %<- (reduce-closed Dred1 Deq)
  %<- ({x} app-resp (Deq x) term-eq/i (Deq' x))
  %<- (linear-resp Deq' (linear/app2 Dlin') Dlin'') %.
%term tens1
  %pi (srl ([x] red/tensor (Dred2 x) (Dred1 x)) ([x] [d] of/tensor (Dof2 x d) (Dof1 x d)) (linear/tensor1 Dlin) Dlin'')
  %<- (srl Dred1 Dof1 Dlin Dlin')
  %<- (reduce-closed Dred2 Deq)
  %<- ({x} tensor-resp term-eq/i (Deq x) (Deq' x))
  %<- (linear-resp Deq' (linear/tensor1 Dlin') Dlin'') %.
%scope sr %term tens2
  %pi (srl ([x] red/tensor (Dred2 x) (Dred1 x)) ([x] [d] of/tensor (Dof2 x d) (Dof1 x d)) (linear/tensor2 Dlin) Dlin'')
  %<- (srl Dred2 Dof2 Dlin Dlin')
  %<- (reduce-closed Dred1 Deq)
  %<- ({x} tensor-resp (Deq x) term-eq/i (Deq' x))
  %<- (linear-resp Deq' (linear/tensor2 Dlin') Dlin'') %.
%term lett1
  %pi (srl ([x] red/lett (Dred2 x) (Dred1 x)) ([x] [d] of/lett (Dlin2 x) (Dlin1 x) (Dof2 x d) (Dof1 x d)) (linear/lett1 Dlin) Dlin'')
  %<- (srl Dred1 Dof1 Dlin Dlin')
  %<- ({y} {z} reduce-closed ([x] Dred2 x y z) ([x] Deq x y z))
  %<- ({x} lett-resp term-eq/i (Deq x) (Deq' x))
  %<- (linear-resp Deq' (linear/lett1 Dlin') Dlin'') %.
%scope sr %term lett2
  %pi (srl ([x] red/lett (Dred2 x) (Dred1 x)) ([x] [d] of/lett (Dlin2 x) (Dlin1 x) (Dof2 x d) (Dof1 x d)) (linear/lett2 Dlin) Dlin'')
  %<- ({y} {e of y T1} {z} {f of z T2} srl ([x] Dred2 x y z) ([x] [d] Dof2 x d y e z f) (Dlin y z) (Dlin' y z))
  %<- (reduce-closed Dred1 Deq)
  %<- ({x} lett-resp (Deq x) ([_] [_] term-eq/i) (Deq' x))
  %<- (linear-resp Deq' (linear/lett2 Dlin') Dlin'') %.
%term pair
  %pi (srl ([x] red/pair (Dred2 x) (Dred1 x)) ([x] [d] of/pair (Dof2 x d) (Dof1 x d)) (linear/pair Dlin2 Dlin1) (linear/pair Dlin2' Dlin1'))
  %<- (srl Dred1 Dof1 Dlin1 Dlin1')
  %<- (srl Dred2 Dof2 Dlin2 Dlin2') %.
%scope sr %term pi1
  %pi (srl ([x] red/pi1 (Dred x)) ([x] [d] of/pi1 (Dof x d)) (linear/pi1 Dlin) (linear/pi1 Dlin'))
  %<- (srl Dred Dof Dlin Dlin') %.
%term pi2
  %pi (srl ([x] red/pi2 (Dred x)) ([x] [d] of/pi2 (Dof x d)) (linear/pi2 Dlin) (linear/pi2 Dlin'))
  %<- (srl Dred Dof Dlin Dlin') %.
%scope sr %term in1
  %pi (srl ([x] red/in1 (Dred x)) ([x] [d] of/in1 (Dof x d)) (linear/in1 Dlin) (linear/in1 Dlin'))
  %<- (srl Dred Dof Dlin Dlin') %.
%term in2
  %pi (srl ([x] red/in2 (Dred x)) ([x] [d] of/in2 (Dof x d)) (linear/in2 Dlin) (linear/in2 Dlin'))
  %<- (srl Dred Dof Dlin Dlin') %.
%scope sr %term case1
  %pi (srl ([x] red/case (Dred3 x) (Dred2 x) (Dred1 x)) ([x] [d] of/case (Dlin3 x) (Dlin2 x) (Dof3 x d) (Dof2 x d) (Dof1 x d)) (linear/case1 Dlin) Dlin'')
  %<- (srl Dred1 Dof1 Dlin Dlin')
  %<- ({y} reduce-closed ([x] Dred2 x y) ([x] Deq2 x y))
  %<- ({y} reduce-closed ([x] Dred3 x y) ([x] Deq3 x y))
  %<- ({x} case-resp term-eq/i (Deq2 x) (Deq3 x) (Deq' x))
  %<- (linear-resp Deq' (linear/case1 Dlin') Dlin'') %.
%term case2
  %pi (srl ([x] red/case (Dred3 x) (Dred2 x) (Dred1 x)) ([x] [d] of/case (Dlin3 x) (Dlin2 x) (Dof3 x d) (Dof2 x d) (Dof1 x d)) (linear/case2 Dlin3' Dlin2') Dlin'')
  %<- ({x'} {d'} srl ([x] Dred2 x x') ([x] [d] Dof2 x d x' d') (Dlin2' x') (Dlin2'' x'))
  %<- ({x'} {d'} srl ([x] Dred3 x x') ([x] [d] Dof3 x d x' d') (Dlin3' x') (Dlin3'' x'))
  %<- (reduce-closed Dred1 Deq)
  %<- ({x} case-resp (Deq x) ([y] term-eq/i) ([y] term-eq/i) (Deq' x))
  %<- (linear-resp Deq' (linear/case2 Dlin3'' Dlin2'') Dlin'') %.
%scope sr %term letb1
  %pi (srl ([x] red/letb (Dred2 x) (Dred1 x)) ([x] [d] of/letb (Dof2 x d) (Dof1 x d)) (linear/letb1 Dlin) Dlin'')
  %<- (srl Dred1 Dof1 Dlin Dlin')
  %<- ({y} reduce-closed ([x] Dred2 x y) ([x] Deq x y))
  %<- ({x} letb-resp term-eq/i (Deq x) (Deq' x))
  %<- (linear-resp Deq' (linear/letb1 Dlin') Dlin'') %.
%term letb1
  %pi (srl ([x] red/letb (Dred2 x) (Dred1 x)) ([x] [d] of/letb (Dof2 x d) (Dof1 x d)) (linear/letb2 Dlin) Dlin'')
  %<- ({x'} {d'} srl ([x] Dred2 x x') ([x] [d] Dof2 x d x' d') (Dlin x') (Dlin' x'))
  %<- (reduce-closed Dred1 Deq)
  %<- ({x} letb-resp (Deq x) ([y] term-eq/i) (Deq' x))
  %<- (linear-resp Deq' (linear/letb2 Dlin') Dlin'') %.
%scope sr %term any1
  %pi (srl ([x] red/any (Dred x)) ([x] [d] of/any (Dof x d)) (linear/any1 Dlin) (linear/any1 Dlin'))
  %<- (srl Dred Dof Dlin Dlin') %.
%term any2
  %pi (srl ([x] red/any (Dred x)) ([x] [d] of/any (Dof x d)) linear/any2 Dlin)
  %<- (reduce-closed Dred Deq)
  %<- ({x} any-resp (Deq x) (Deq' x))
  %<- (linear-resp Deq' linear/any2 Dlin) %.
%scope sr %term Cl*11 srl ([x] %the (reduce (app (lett (M1 x) M2) M3) _) red/app/lett) _ (linear/app1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term Cl*12 srl ([x] %the (reduce (app (lett M1 (M2 x)) M3) _) red/app/lett) _ (linear/app1 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/app1 (Dlin x y))) %.
%scope sr %term Cl*2 srl ([x] %the (reduce (app (lett M1 M2) (M3 x)) _) red/app/lett) _ (linear/app2 Dlin) (linear/lett2 ([x] [y] linear/app2 Dlin)) %.
%term Cl+11 srl ([x] %the (reduce (app (case (M1 x) M2a M2b) M3) _) red/app/case) _ (linear/app1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%scope sr %term Cl+12 srl ([x] %the (reduce (app (case M1 (M2a x) (M2b x)) M3) _) red/app/case) _ (linear/app1 (linear/case2 DlinB DlinA)) (linear/case2 ([y] linear/app1 (DlinB y)) ([y] linear/app1 (DlinA y))) %.
%term Cl+2 srl ([x] %the (reduce (app (case M1 M2a M2b) (M3 x)) _) red/app/case) _ (linear/app2 Dlin) (linear/case2 ([y] linear/app2 Dlin) ([y] linear/app2 Dlin)) %.
%scope sr %term Cl!11 srl ([x] %the (reduce (app (letb (M1 x) M2) M3) _) red/app/letb) _ (linear/app1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term Cl!12 srl ([x] %the (reduce (app (letb M1 (M2 x)) M3) _) red/app/letb) _ (linear/app1 (linear/letb2 Dlin)) (linear/letb2 ([y] linear/app1 (Dlin y))) %.
%scope sr %term Cl!2 srl ([x] %the (reduce (app (letb M1 M2) (M3 x)) _) red/app/letb) _ (linear/app2 Dlin) (linear/letb2 ([y] linear/app2 Dlin)) %.
%term Cl011 srl ([x] %the (reduce (app (any (M1 x)) M2) _) red/app/any) _ (linear/app1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%scope sr %term Cl012 srl ([x] %the (reduce (app (any M1) M2) _) red/app/any) _ (linear/app1 linear/any2) linear/any2 %.
%term Cl02 srl ([x] %the (reduce (app (any M1) (M2 x)) _) red/app/any) _ (linear/app2 _) linear/any2 %.
%scope sr %term C&1*1 srl ([x] %the (reduce (pi1 (lett (M1 x) M2)) _) red/pi1/lett) _ (linear/pi1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C&1*2 srl ([x] %the (reduce (pi1 (lett M1 (M2 x))) _) red/pi1/lett) _ (linear/pi1 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/pi1 (Dlin x y))) %.
%scope sr %term C&1+1 srl ([x] %the (reduce (pi1 (case (M1 x) M2a M2b)) _) red/pi1/case) _ (linear/pi1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%term C&1+2 srl ([x] %the (reduce (pi1 (case M1 (M2a x) (M2b x))) _) red/pi1/case) _ (linear/pi1 (linear/case2 DlinB DlinA)) (linear/case2 ([x] linear/pi1 (DlinB x)) ([x] linear/pi1 (DlinA x))) %.
%scope sr %term C&1!1 srl ([x] %the (reduce (pi1 (letb (M1 x) M2)) _) red/pi1/letb) _ (linear/pi1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C&1!2 srl ([x] %the (reduce (pi1 (letb M1 (M2 x))) _) red/pi1/letb) _ (linear/pi1 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/pi1 (Dlin x))) %.
%scope sr %term C&101 srl ([x] %the (reduce (pi1 (any (M x))) _) red/pi1/any) _ (linear/pi1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%term C&102 srl ([x] %the (reduce (pi1 (any M)) _) red/pi1/any) _ (linear/pi1 linear/any2) linear/any2 %.
%scope sr %term C&2*1 srl ([x] %the (reduce (pi2 (lett (M1 x) M2)) _) red/pi2/lett) _ (linear/pi2 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C&2*2 srl ([x] %the (reduce (pi2 (lett M1 (M2 x))) _) red/pi2/lett) _ (linear/pi2 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/pi2 (Dlin x y))) %.
%scope sr %term C&2+1 srl ([x] %the (reduce (pi2 (case (M1 x) M2a M2b)) _) red/pi2/case) _ (linear/pi2 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%term C&2+2 srl ([x] %the (reduce (pi2 (case M1 (M2a x) (M2b x))) _) red/pi2/case) _ (linear/pi2 (linear/case2 DlinB DlinA)) (linear/case2 ([x] linear/pi2 (DlinB x)) ([x] linear/pi2 (DlinA x))) %.
%scope sr %term C&2!1 srl ([x] %the (reduce (pi2 (letb (M1 x) M2)) _) red/pi2/letb) _ (linear/pi2 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C&2!2 srl ([x] %the (reduce (pi2 (letb M1 (M2 x))) _) red/pi2/letb) _ (linear/pi2 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/pi2 (Dlin x))) %.
%scope sr %term C&201 srl ([x] %the (reduce (pi2 (any (M x))) _) red/pi2/any) _ (linear/pi2 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%term C&202 srl ([x] %the (reduce (pi2 (any M)) _) red/pi2/any) _ (linear/pi2 linear/any2) linear/any2 %.
%scope sr %term C**11 srl ([x] %the (reduce (lett (lett (M1 x) M2) M3) _) red/lett/lett) _ (linear/lett1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C**12 srl ([x] %the (reduce (lett (lett M1 (M2 x)) M3) _) red/lett/lett) _ (linear/lett1 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/lett1 (Dlin x y))) %.
%scope sr %term C**2 srl ([x] %the (reduce (lett (lett M1 M2) (M3 x)) _) red/lett/lett) _ (linear/lett2 Dlin) (linear/lett2 ([x] [y] linear/lett2 Dlin)) %.
%term C*+11 srl ([x] %the (reduce (lett (case (M1 x) M2a M2b) M3) _) red/lett/case) _ (linear/lett1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%scope sr %term C*+12 srl ([x] %the (reduce (lett (case M1 (M2a x) (M2b x)) M3) _) red/lett/case) _ (linear/lett1 (linear/case2 DlinB DlinA)) (linear/case2 ([y] linear/lett1 (DlinB y)) ([y] linear/lett1 (DlinA y))) %.
%term C*+2 srl ([x] %the (reduce (lett (case M1 M2a M2b) (M3 x)) _) red/lett/case) _ (linear/lett2 Dlin) (linear/case2 ([y] linear/lett2 Dlin) ([y] linear/lett2 Dlin)) %.
%scope sr %term C*!11 srl ([x] %the (reduce (lett (letb (M1 x) M2) M3) _) red/lett/letb) _ (linear/lett1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C*!12 srl ([x] %the (reduce (lett (letb M1 (M2 x)) M3) _) red/lett/letb) _ (linear/lett1 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/lett1 (Dlin x))) %.
%scope sr %term C*!2 srl ([x] %the (reduce (lett (letb M1 M2) (M3 x)) _) red/lett/letb) _ (linear/lett2 Dlin) (linear/letb2 ([x] linear/lett2 Dlin)) %.
%term C*011 srl ([x] %the (reduce (lett (any (M1 x)) M2) _) red/lett/any) _ (linear/lett1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%scope sr %term C*012 srl ([x] %the (reduce (lett (any M1) M2) _) red/lett/any) _ (linear/lett1 linear/any2) linear/any2 %.
%term C*02 srl ([x] %the (reduce (lett (any M1) (M2 x)) _) red/lett/any) _ (linear/lett2 Dlin) linear/any2 %.
%scope sr %term C+*11 srl ([x] %the (reduce (case (lett (M1 x) M2) M3a M3b) _) red/case/lett) _ (linear/case1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C+*12 srl ([x] %the (reduce (case (lett M1 (M2 x)) M3a M3b) _) red/case/lett) _ (linear/case1 (linear/lett2 Dlin)) (linear/lett2 ([y] [z] linear/case1 (Dlin y z))) %.
%scope sr %term C+*2 srl ([x] %the (reduce (case (lett M1 M2) (M3a x) (M3b x)) _) red/case/lett) _ (linear/case2 DlinB DlinA) (linear/lett2 ([y] [z] linear/case2 DlinB DlinA)) %.
%term C++11 srl ([x] %the (reduce (case (case (M1 x) M2a M2b) M3a M3b) _) red/case/case) _ (linear/case1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%scope sr %term C++12 srl ([x] %the (reduce (case (case M1 (M2a x) (M2b x)) M3a M3b) _) red/case/case) _ (linear/case1 (linear/case2 DlinB DlinA)) (linear/case2 ([y] linear/case1 (DlinB y)) ([y] linear/case1 (DlinA y))) %.
%term C++2 srl ([x] %the (reduce (case (case M1 M2a M2b) (M3a x) (M3b x)) _) red/case/case) _ (linear/case2 DlinB DlinA) (linear/case2 ([y] linear/case2 DlinB DlinA) ([y] linear/case2 DlinB DlinA)) %.
%scope sr %term C+!11 srl ([x] %the (reduce (case (letb (M1 x) M2) M3a M3b) _) red/case/letb) _ (linear/case1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C+!12 srl ([x] %the (reduce (case (letb M1 (M2 x)) M3a M3b) _) red/case/letb) _ (linear/case1 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/case1 (Dlin x))) %.
%scope sr %term C+!2 srl ([x] %the (reduce (case (letb M1 M2) (M3a x) (M3b x)) _) red/case/letb) _ (linear/case2 DlinB DlinA) (linear/letb2 ([x] linear/case2 DlinB DlinA)) %.
%term C+011 srl ([x] %the (reduce (case (any (M1 x)) M2a M2b) _) red/case/any) _ (linear/case1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%scope sr %term C+012 srl ([x] %the (reduce (case (any M1) M2a M2b) _) red/case/any) _ (linear/case1 linear/any2) linear/any2 %.
%term C+02 srl ([x] %the (reduce (case (any M1) (M2a x) (M2b x)) _) red/case/any) _ (linear/case2 DlinB DlinA) linear/any2 %.
%scope sr %term C!*11 srl ([x] %the (reduce (letb (lett (M1 x) M2) M3) _) red/letb/lett) _ (linear/letb1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C!*12 srl ([x] %the (reduce (letb (lett M1 (M2 x)) M3) _) red/letb/lett) _ (linear/letb1 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/letb1 (Dlin x y))) %.
%scope sr %term C!*2 srl ([x] %the (reduce (letb (lett M1 M2) (M3 x)) _) red/letb/lett) _ (linear/letb2 Dlin) (linear/lett2 ([x] [y] linear/letb2 Dlin)) %.
%term C!+11 srl ([x] %the (reduce (letb (case (M1 x) M2a M2b) M3) _) red/letb/case) _ (linear/letb1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%scope sr %term C!+12 srl ([x] %the (reduce (letb (case M1 (M2a x) (M2b x)) M3) _) red/letb/case) _ (linear/letb1 (linear/case2 DlinB DlinA)) (linear/case2 ([x] linear/letb1 (DlinB x)) ([x] linear/letb1 (DlinA x))) %.
%term C!+2 srl ([x] %the (reduce (letb (case M1 M2a M2b) (M3 x)) _) red/letb/case) _ (linear/letb2 Dlin) (linear/case2 ([x] linear/letb2 Dlin) ([x] linear/letb2 Dlin)) %.
%scope sr %term C!!11 srl ([x] %the (reduce (letb (letb (M1 x) M2) M3) _) red/letb/letb) _ (linear/letb1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C!!12 srl ([x] %the (reduce (letb (letb M1 (M2 x)) M3) _) red/letb/letb) _ (linear/letb1 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/letb1 (Dlin x))) %.
%scope sr %term C!!2 srl ([x] %the (reduce (letb (letb M1 M2) (M3 x)) _) red/letb/letb) _ (linear/letb2 Dlin) (linear/letb2 ([x] linear/letb2 Dlin)) %.
%term C!011 srl ([x] %the (reduce (letb (any (M1 x)) M2) _) red/letb/any) _ (linear/letb1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%scope sr %term C!012 srl ([x] %the (reduce (letb (any M1) M2) _) red/letb/any) _ (linear/letb1 linear/any2) linear/any2 %.
%term C!02 srl ([x] %the (reduce (letb (any M1) (M2 x)) _) red/letb/any) _ (linear/letb2 Dlin) linear/any2 %.
%scope sr %term C0*11 srl ([x] %the (reduce (any (lett (M1 x) M2)) _) red/any/lett) _ (linear/any1 (linear/lett1 Dlin)) (linear/lett1 Dlin) %.
%term C0*12 srl ([x] %the (reduce (any (lett M1 (M2 x))) _) red/any/lett) _ (linear/any1 (linear/lett2 Dlin)) (linear/lett2 ([x] [y] linear/any1 (Dlin x y))) %.
%scope sr %term C0*2 srl ([x] %the (reduce (any (lett M1 M2)) _) red/any/lett) _ linear/any2 (linear/lett2 ([x] [y] linear/any2)) %.
%term C0+11 srl ([x] %the (reduce (any (case (M1 x) M2a M2b)) _) red/any/case) _ (linear/any1 (linear/case1 Dlin)) (linear/case1 Dlin) %.
%scope sr %term C0+12 srl ([x] %the (reduce (any (case M1 (M2a x) (M2b x))) _) red/any/case) _ (linear/any1 (linear/case2 DlinB DlinA)) (linear/case2 ([x] linear/any1 (DlinB x)) ([x] linear/any1 (DlinA x))) %.
%term C0+2 srl ([x] %the (reduce (any (case M1 M2a M2b)) _) red/any/case) _ linear/any2 (linear/case2 ([x] linear/any2) ([x] linear/any2)) %.
%scope sr %term C0!11 srl ([x] %the (reduce (any (letb (M1 x) M2)) _) red/any/letb) _ (linear/any1 (linear/letb1 Dlin)) (linear/letb1 Dlin) %.
%term C0!12 srl ([x] %the (reduce (any (letb M1 (M2 x))) _) red/any/letb) _ (linear/any1 (linear/letb2 Dlin)) (linear/letb2 ([x] linear/any1 (Dlin x))) %.
%scope sr %term C0!2 srl ([x] %the (reduce (any (letb M1 M2)) _) red/any/letb) _ linear/any2 (linear/letb2 ([x] linear/any2)) %.
%term C0011 srl ([x] %the (reduce (any (any (M x))) _) red/any/any) _ (linear/any1 (linear/any1 Dlin)) (linear/any1 Dlin) %.
%scope sr %term C0012 srl ([x] %the (reduce (any (any M)) _) red/any/any) _ (linear/any1 linear/any2) linear/any2 %.
%term C002 srl ([x] %the (reduce (any (any M)) _) red/any/any) _ linear/any2 linear/any2 %.
%scope sr %term refl sr red/refl D D %.
%term trans
  %pi (sr (red/trans Dred23 Dred12) D1 D3)
  %<- (sr Dred12 D1 D2)
  %<- (sr Dred23 D2 D3) %.
%scope sr %term beta sr red/beta (of/app Dof2 (of/lam _ Dof1)) (Dof1 _ Dof2) %.
%term beta* sr red/beta* (of/lett Dlin2 Dlin1 Dof (of/tensor Dof2 Dof1)) (Dof _ Dof1 _ Dof2) %.
%scope sr %term beta&1 sr red/beta&1 (of/pi1 (of/pair Dof2 Dof1)) Dof1 %.
%term beta&2 sr red/beta&2 (of/pi2 (of/pair Dof2 Dof1)) Dof2 %.
%scope sr %term beta+1 sr red/beta+1 (of/case _ _ Dof2 Dof1 (of/in1 Dof)) (Dof1 _ Dof) %.
%term beta+2 sr red/beta+2 (of/case _ _ Dof2 Dof1 (of/in2 Dof)) (Dof2 _ Dof) %.
%scope sr %term beta! sr red/beta! (of/letb Dof2 (of/bang Dof1)) (Dof2 _ Dof1) %.
%term lam
  %pi (sr (red/lam Dred) (of/lam Dlin Dof) (of/lam Dlin' Dof'))
  %<- ({x} {d} sr (Dred x) (Dof x d) (Dof' x d))
  %<- (srl Dred Dof Dlin Dlin') %.
%scope sr %term app
  %pi (sr (red/app Dred2 Dred1) (of/app Dof2 Dof1) (of/app Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- (sr Dred2 Dof2 Dof2') %.
%term tensor
  %pi (sr (red/tensor Dred2 Dred1) (of/tensor Dof2 Dof1) (of/tensor Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- (sr Dred2 Dof2 Dof2') %.
%scope sr %term lett
  %pi (sr (red/lett Dred2 Dred1) (of/lett Dlin2 Dlin1 Dof2 Dof1) (of/lett Dlin2' Dlin1' Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- ({x} {d of x T1} {y} {e of y T2} sr (Dred2 x y) (Dof2 x d y e) (Dof2' x d y e))
  %<- ({y} {e of y T2} srl ([x] Dred2 x y) ([x] [d] Dof2 x d y e) (Dlin1 y) (Dlin1' y))
  %<- ({x} {d of x T1} srl ([y] Dred2 x y) ([y] [e] Dof2 x d y e) (Dlin2 x) (Dlin2' x)) %.
%term pair
  %pi (sr (red/pair Dred2 Dred1) (of/pair Dof2 Dof1) (of/pair Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- (sr Dred2 Dof2 Dof2') %.
%scope sr %term pi1 %pi (sr (red/pi1 Dred) (of/pi1 Dof) (of/pi1 Dof')) %<- (sr Dred Dof Dof') %.
%term pi2 %pi (sr (red/pi2 Dred) (of/pi2 Dof) (of/pi2 Dof')) %<- (sr Dred Dof Dof') %.
%scope sr %term in1 %pi (sr (red/in1 Dred) (of/in1 Dof) (of/in1 Dof')) %<- (sr Dred Dof Dof') %.
%term in2 %pi (sr (red/in2 Dred) (of/in2 Dof) (of/in2 Dof')) %<- (sr Dred Dof Dof') %.
%scope sr %term case
  %pi (sr (red/case Dred3 Dred2 Dred1) (of/case Dlin3 Dlin2 Dof3 Dof2 Dof1) (of/case Dlin3' Dlin2' Dof3' Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- ({x} {d} sr (Dred2 x) (Dof2 x d) (Dof2' x d))
  %<- ({x} {d} sr (Dred3 x) (Dof3 x d) (Dof3' x d))
  %<- (srl Dred2 Dof2 Dlin2 Dlin2')
  %<- (srl Dred3 Dof3 Dlin3 Dlin3') %.
%term letb
  %pi (sr (red/letb Dred2 Dred1) (of/letb Dof2 Dof1) (of/letb Dof2' Dof1'))
  %<- (sr Dred1 Dof1 Dof1')
  %<- ({x} {d} sr (Dred2 x) (Dof2 x d) (Dof2' x d)) %.
%scope sr %term bang %pi (sr (red/bang Dred) (of/bang Dof) (of/bang Dof')) %<- (sr Dred Dof Dof') %.
%term any %pi (sr (red/any Dred) (of/any Dof) (of/any Dof')) %<- (sr Dred Dof Dof') %.
%scope sr %term Cl* sr red/app/lett (of/app Dof3 (of/lett Dlin2 Dlin1 Dof2 Dof1)) (of/lett ([x] linear/app1 (Dlin2 x)) ([x] linear/app1 (Dlin1 x)) ([x1] [d1] [x2] [d2] of/app Dof3 (Dof2 x1 d1 x2 d2)) Dof1) %.
%term Cl+ sr red/app/case (of/app Dof3 (of/case DlinB DlinA Dof2b Dof2a Dof1)) (of/case (linear/app1 DlinB) (linear/app1 DlinA) ([x] [d] of/app Dof3 (Dof2b x d)) ([x] [d] of/app Dof3 (Dof2a x d)) Dof1) %.
%scope sr %term Cl! sr red/app/letb (of/app Dof3 (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/app Dof3 (Dof2 x d)) Dof1) %.
%term Cl0 sr red/app/any (of/app _ (of/any Dof)) (of/any Dof) %.
%scope sr %term C&1* sr red/pi1/lett (of/pi1 (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/pi1 (Dlin2' x)) ([x] linear/pi1 (Dlin2 x)) ([x1] [d1] [x2] [d2] of/pi1 (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C&1+ sr red/pi1/case (of/pi1 (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/pi1 Dlin2b) (linear/pi1 Dlin2a) ([x] [d] of/pi1 (Dof2b x d)) ([x] [d] of/pi1 (Dof2a x d)) Dof1) %.
%scope sr %term C&1! sr red/pi1/letb (of/pi1 (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/pi1 (Dof2 x d)) Dof1) %.
%term C&10 sr red/pi1/any (of/pi1 (of/any Dof)) (of/any Dof) %.
%scope sr %term C&2* sr red/pi2/lett (of/pi2 (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/pi2 (Dlin2' x)) ([x] linear/pi2 (Dlin2 x)) ([x1] [d1] [x2] [d2] of/pi2 (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C&2+ sr red/pi2/case (of/pi2 (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/pi2 Dlin2b) (linear/pi2 Dlin2a) ([x] [d] of/pi2 (Dof2b x d)) ([x] [d] of/pi2 (Dof2a x d)) Dof1) %.
%scope sr %term C&2! sr red/pi2/letb (of/pi2 (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/pi2 (Dof2 x d)) Dof1) %.
%term C&20 sr red/pi2/any (of/pi2 (of/any Dof)) (of/any Dof) %.
%scope sr %term C** sr red/lett/lett (of/lett Dlin3' Dlin3 Dof3 (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/lett1 (Dlin2' x)) ([x] linear/lett1 (Dlin2 x)) ([x1] [d1] [x2] [d2] of/lett Dlin3' Dlin3 Dof3 (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C*+ sr red/lett/case (of/lett Dlin3' Dlin3 Dof3 (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/lett1 Dlin2b) (linear/lett1 Dlin2a) ([x] [d] of/lett Dlin3' Dlin3 Dof3 (Dof2b x d)) ([x] [d] of/lett Dlin3' Dlin3 Dof3 (Dof2a x d)) Dof1) %.
%scope sr %term C*! sr red/lett/letb (of/lett Dlin3' Dlin3 Dof3 (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/lett Dlin3' Dlin3 Dof3 (Dof2 x d)) Dof1) %.
%term C*0 sr red/lett/any (of/lett _ _ _ (of/any Dof)) (of/any Dof) %.
%scope sr %term C+* sr red/case/lett (of/case Dlin3b Dlin3a Dof3b Dof3a (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/case1 (Dlin2' x)) ([y] linear/case1 (Dlin2 y)) ([x1] [d1] [x2] [d2] of/case Dlin3b Dlin3a Dof3b Dof3a (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C++ sr red/case/case (of/case Dlin3b Dlin3a Dof3b Dof3a (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/case1 Dlin2b) (linear/case1 Dlin2a) ([x] [d] of/case Dlin3b Dlin3a Dof3b Dof3a (Dof2b x d)) ([x] [d] of/case Dlin3b Dlin3a Dof3b Dof3a (Dof2a x d)) Dof1) %.
%scope sr %term C+! sr red/case/letb (of/case Dlin3b Dlin3a Dof3b Dof3a (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/case Dlin3b Dlin3a Dof3b Dof3a (Dof2 x d)) Dof1) %.
%term C+0 sr red/case/any (of/case _ _ _ _ (of/any Dof)) (of/any Dof) %.
%scope sr %term C!* sr red/letb/lett (of/letb Dof3 (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/letb1 (Dlin2' x)) ([x] linear/letb1 (Dlin2 x)) ([x1] [d1] [x2] [d2] of/letb Dof3 (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C!+ sr red/letb/case (of/letb Dof3 (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/letb1 Dlin2b) (linear/letb1 Dlin2a) ([x] [d] of/letb Dof3 (Dof2b x d)) ([x] [d] of/letb Dof3 (Dof2a x d)) Dof1) %.
%scope sr %term C!! sr red/letb/letb (of/letb Dof3 (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/letb Dof3 (Dof2 x d)) Dof1) %.
%term C!0 sr red/letb/any (of/letb _ (of/any Dof)) (of/any Dof) %.
%scope sr %term C0* sr red/any/lett (of/any (of/lett Dlin2' Dlin2 Dof2 Dof1)) (of/lett ([x] linear/any1 (Dlin2' x)) ([x] linear/any1 (Dlin2 x)) ([x1] [d1] [x2] [d2] of/any (Dof2 x1 d1 x2 d2)) Dof1) %.
%term C0+ sr red/any/case (of/any (of/case Dlin2b Dlin2a Dof2b Dof2a Dof1)) (of/case (linear/any1 Dlin2b) (linear/any1 Dlin2a) ([x] [d] of/any (Dof2b x d)) ([x] [d] of/any (Dof2a x d)) Dof1) %.
%scope sr %term C0! sr red/any/letb (of/any (of/letb Dof2 Dof1)) (of/letb ([x] [d] of/any (Dof2 x d)) Dof1) %.
%term C00 sr red/any/any (of/any (of/any Dof)) (of/any Dof) %.
%worlds (bind) (srl _ _ _ _) (sr _ _ _) %.
%total (D1 D2) (srl D1 _ _ _) (sr D2 _ _) %.

> Show complete code.

check="true"> Show STELF output.