kinds, integers, registers, variables:
        k = k->k | nat | reg | type
        n = 0 | s(n)
        r = r1 | ... | rn
        l = n | r
proof formulas:
        t = !t | t -o t | t*t
          | 0 | s(t) | elim t t t
          | A | all A:k.t | exists A:k.t | \A:k.t | t t
          | %t | rec t
          | r | Reg t t | Mem t t | Code t t
patterns:
        pat = x | !x | !(pat) | A,pat | pat,pat
proof terms:
        e = x | !e | let pat = e in e | \pat:t.e | e e | e,e
          | induction t t e e
          | \A:k.e | e t | pack t,e as t
          | %e | e %<< e
          | fact | code(n)[t...t]
        v = !v | \pat:t.e | v,v | \A:k.e | pack t,v as t | %e | fact | code(n)[t...t]
programming terms:
        c = e | #c
        ins = [c]
            | [c]mov r<-n
            | [c|c]mov r<-r
            | [c|c]add r<-r+n
            | [c|c|c]add r<-r+r
            | [c|c]load r<-[r+n]
            | [c|c|c]store [r+n]<-r
            | [c|c|x.c]ble r<=r n
        blk = let pat = ins in blk
            | [c]jmp n
            | [c|c]jmp r
        b = \A:k.b
          | \pat:t.blk
programs:
        prog = let pat = c in prog
             | B blk

static environments:
       non D = {...A->k...}
       lin G = {} | G,x->t | G,!x->t
       non P = {...n->t...} for Code
       lin L = {...l->n...} for Reg/Mem
dynamic environments:
       lin L = {...l->n...} for Reg/Mem
       non B = {...n->b...} for Code
(note: following tradition, sometimes A:k or x:t is written for A->k or x->t)

C = D;G;P;L
!C = D;!G;P;{}

!{} = {}
!(G,x->t) = !G
!(G,!x->t) = !G,!x->t
domain({}) = {}
domain(G,x->t) = {x} union domain(G)
domain(G,!x->t) = {x} union domain(G)

C=C1,C2 if C and C1 and C2 have identical nonlinear (non) assumptions
  and C's linear (lin) assumptions are divided between C1 and C2
D = D1 D2 if D = D1 union D2 and domain(D1) disjoint from domain(D2)
G = G1 G2 if G = G1 union G2 and domain(G1) disjoint from domain(G2)
D;G;P;L D';G' = D D';G G';P;L if D D' and G G' are well-formed
G=G1,x->t if G = G1 union {x->t} and x not in domain(G1)
G=G1,!x->t if G = G1 union {!x->t} and x not in domain(G1)
D=D1,A->k if D = D1 union {A->k} and A not in domain(D1)
(similar definitions for extending P,L,B)

Typing judgments:
D |- t:k
|- t1=t2
|- pat:t => D;G
C |- e:t
C |- c:t
(C);(C') |- ins:t
C |- blk
!C |- n->b:t
D;G;{};L |- prog

abbreviations:
  D;G;P;L |- t:k means D |- t:k
  D;G;P;L |- t1=t2 means |- t1=t2
  LE = \A:nat.\B:nat.all F:nat->type.!(all N:nat.F N -o F s(N)) -o F A -o F B
  ADD = \A:nat.\B:nat.elim B A (\M:nat.\C:nat.s(C))

[s] = [] | [A<-t][s] | [x<-e][s]

Evaluation/reduction judgments:
pat<-e => [s]
e-->e'
c-->c'
(L;ins) --> (L;ins')
(L;ins) --> (L';v)
B |- (L;blk) --> (L';blk')
(L;prog) --> (L';prog')

====================================================================

D |- t:type
----------
D |- !t:type

D |- t1:type
D |- t2:type
----------------
D |- t1 -o t2:type

D |- t1:type
D |- t2:type
-------------
D |- t1*t2:type

D |- 0:nat

D |- t:nat
-------------
D |- s(t):nat

D |- tn:nat
D |- tz:k
D |- ts:nat->k->k
--------------------
D |- elim tn tz ts:k

D,A:k |- A:k

D,A:k |- t:type
-------------------
D |- all A:k.t : type

D,A:k |- t:type
----------------------
D |- exists A:k.t : type

D,A:ka |- t:kb
---------------------
D |- \A:ka.t : ka->kb

D |- tf:ka->kb
D |- ta:ka
--------------
D |- tf ta:kb

D |- t:k
---------
D |- %t:k

D |- t:k->k
------------
D |- rec t:k

D |- r:reg

D |- tr:reg
D |- tn:nat
-------------------
D |- Reg tr tn:type

D |- tm:nat
D |- tn:nat
-------------------
D |- Mem tm tn:type

D |- tm:nat
D |- t:type
-------------------
D |- Code tm t:type

====================================================================

|- t = t

|- t1 = t2
----------
|- t2 = t1

|- t1 = t2
|- t2 = t3
----------
|- t1 = t3

|- (\A:k.tb) ta = [A<-ta]tb

|- elim 0 tz ts = tz

|- elim s(tm) tz ts = ts tm (elim tm tz ts)

|- rec t = %(t (rec t))

|- (%t1) t2 = %(t1 t2)

|- t1 = t1'
-----------------
|- T[t1] = T[t1']

|- t1 = t1'
|- t2 = t2'
------------------------
|- T[t1,t2] = T[t1',t2']

|- t1 = t1'
|- t2 = t2'
|- t3 = t3'
-------------------------------
|- T[t1,t2,t3] = T[t1',t2',t3']

T[t1] = !t1 | s(t1) | all A:k.t1 | exists A:k.t1 | \A:k.t1 | %t1 | rec t1
T[t1,t2] = t1 -o t2 | t1*t2 | t1 t2 | Reg t1 t2 | Mem t1 t2 | Code t1 t2
T[t1,t2,t3] = elim t1 t2 t3

====================================================================

(single-step version of = for use in proofs)

|- t => t
|- (\A:k.tb) ta => [A<-ta]tb
|- elim 0 tz ts => tz
|- elim s(tm) tz ts => ts tm (elim tm tz ts)
|- rec t => %(t (rec t))
|- (%t1) t2 => %(t1 t2)

|- t1 => t1'
------------------
|- T[t1] => T[t1']

|- t1 => t1'
|- t2 => t2'
-------------------------
|- T[t1,t2] => T[t1',t2']

|- t1 => t1'
|- t2 => t2'
|- t3 => t3'
--------------------------------
|- T[t1,t2,t3] => T[t1',t2',t3']

====================================================================

|- x:t => {};{x:t}

|- !x:!t => {};{!x:t}

|- pat:t => D;G
-------------------
|- !(pat):!t => D;G

|- pat:t => D;G
--------------------------------
|- A,pat:exists A:k.t => D,A:k;G

|- pat1:t1 => D1;G1
|- pat2:t2 => D2;G2
---------------------------------
|- pat1,pat2:t1*t2 => D1 D2;G1 G2

!C,!x:t |- x:t

!C,x:t |- x:t

!C |- e:t
-----------
!C |- !e:!t

C1 |- e1:t1
|- pat:t1 => D;G
C2 D;G |- e2:t2
C1,C2 |- t2:type
------------------------------
C1,C2 |- let pat = e1 in e2:t2

|- pat:ta => D;G
C D;G |- e:tb
C |- ta -o tb : type
-------------------------
C |- \pat:ta.e : ta -o tb

C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb

C1 |- e1:t1
C2 |- e2:t2
--------------------
C1,C2 |- e1,e2:t1*t2

C1,!C2 |- tn:nat
C1,!C2 |- tF:nat->type
C1 |- e0:tF 0
!C2 |- es:!all A:nat.tF A -o tF s(A)
-------------------------------------
C1,!C2 |- induction tn tF e0 es: tF A

C,A:k |- e:t
-----------------------
C |- \A:k.e : all A:k.t

C |- e : all A:k.t'
C |- t:k
-------------------
C |- e t : [A<-t]t'

C |- t1:k
C |- e:[A<-t1]t2
-----------------------------------------------
C |- pack t1,e as exists A:k.t2 : exists A:k.t2

C |- e:t
----------
C |- %e:%t

C1 |- e1:%(ta -o tb)
C2 |- e2:%ta
------------------------
C1,C2 |- e1 %<< e2 : %tb

D;!G;P;{r->n} |- fact:Reg r n

D;!G;P;{n->n'} |- fact:Mem n n'

t = all A1:k1...all An:kn.Code n t'
D |- t1:k1
...
D |- tn:kn
---------------------------------------------------------------
D;!G;P,n->t;{} |- code(n)[t1...tn]:Code n [An<-tn]...[A1<-t1]t'

C |- e:t
C |- t = t'
-----------
C |- e:t'

C |- c:%t
---------
C |- #c:t

(note: no rule is necessary for C |- c:t,C |- t = t' ==> C |- c:t')

Cr |- c:t
-----------------
(C);(Cr) |- [c]:t

Cr |- cr:Reg r t
------------------------------------
(C);(Cr) |- [cr]mov r<-n' : Reg r n'

abbreviation: C |-* c:t means C' |- c:t where C=C',C''

C |-* c':Reg r' t'
Cr |- cr:Reg r t
---------------------------------------
(C);(Cr) |- [cr|c']mov r<-r' : Reg r t'

C |-* c':Reg r' t'
Cr |- cr:Reg r t
-------------------------------------------------
(C);(Cr) |- [cr|c']add r<-r'+n'' : Reg r (t'+n'')

C |-* c':Reg r' t'
C |-* c'':Reg r'' t''
Cr |- cr:Reg r t
---------------------------------------------------------
(C);(Cr) |- [cr|c'|c'']add r<-r'+r'' : Reg r (ADD t' t'')

C |-* c':Reg r' t' * Mem (t'+n'') t''
Cr |- cr:Reg r t
-----------------------------------------------
(C);(Cr) |- [cr|c']load r<-[r'+n''] : Reg r t''

C |-* c':Reg r' t'
C |-* c'':Reg r'' t''
Cr |- cr:Mem (t''+n'') t'''
-------------------------------------------------------------
(C);(Cr) |- [cr|c'|c'']store [r''+n'']<-r' : Mem (t''+n'') t'

C |-* c':Reg r' t'
C |-* c'':Reg r'' t''
C,!x:(LE t' t'') |- c:(Code n t) * t
------------------------------------------------------
(C);(!Cr) |- [c'|c''|x.c]ble r'<=r'' n:!(LE s(t'') t')

(Ca,Cr);(Cr) |- ins:t
|- pat:t => D;G
Ca D;G |- blk
-----------------------------
Ca,Cr |- let pat = ins in blk

C |- c:(Code n t) * t
----------------------
C |- [c]jmp n

C |-* c:Reg r tr
C |- c:(Code tr t) * t
-----------------------
C |- [c|c]jmp r

!C,A:k |- n->b:t
---------------------------
!C |- n->\A:k.b : all A:k.t

|- pat:t => D;G
!C D;G |- blk
!C |- t:type
------------------------------
!C |- n->\pat:t.blk : Code n t

!C |- n->b:t
!C |- t = t'
-------------
!C |- n->b:t'

C |- c:t
C |- pat:t => D;G
C D;G |- prog
------------------------
C |- let pat = c in prog

C = D;G;{n1->t1,...,nn->tn);L
!C |- n1->b1:t1
...
!C |- nn->bn:tn
C |- blk
-----------------------------------
D;G;{};L |- {n1->b1,...,nn->bn} blk

forall n->t in P, |- t:type
forall x->t and !x->t in G, D |- t:type
---------------------------------------
|- D;G;P;L

====================================================================

x<-e => [x<-e]

!x<-!e => [x<-e]

pat<-e => [s]
-----------------
!(pat)<-!e => [s]

pat<-e => [s]
---------------------------------
A,pat<-pack t,e as t' => [s][A<-t]

pat1<-e1 => [s1]
pat2<-e2 => [s2]
---------------------------
pat1,pat2<-e1,e2 => [s2][s1]

pat<-ea => [s]
----------------------------
let pat = ea in eb --> [s]eb

pat<-ea => [s]
------------------------
(\pat:t.eb) ea --> [s]eb

|- tn = 0
----------------------------
induction tn tf e0 es --> e0

|- tn = s(tm)
---------------------------------------------------------
induction tn tf e0 !es --> es tm (induction tm tf e0 !es)

(\A:k.e) t --> [A<-t]e

%ef %<< %ea --> %(ef ea)

E[e1] = !e1 | \pat:t.e1 | \A:k.e1 | e1 t | pack t1,e1 as t2
      | let pat = e1 in e | e1 e | e1,e | induction t t e1 e
      | let pat = e in e1 | e e1 | e,e1 | induction t t e e1
      | e1 %<< e | e %<< e1
(note: no congruence rule for %e)

e-->e'
------------
E[e]-->E[e']

c --> c'
----------
#c --> #c'

#%e --> e

I[c1] = [c1]
      | [c1]mov r<-n
      | [c1|c]mov r<-r
      | [c|c1]mov r<-r
      | [c1|c]add r<-r+n
      | [c|c1]add r<-r+n
      | [c1|c|c]add r<-r+r
      | [c|c1|c]add r<-r+r
      | [c|c|c1]add r<-r+r
      | [c1|c]load r<-[r+n]
      | [c|c1]load r<-[r+n]
      | [c1|c|c]store [r+n]<-r
      | [c|c1|c]store [r+n]<-r
      | [c|c|c1]store [r+n]<-r
      | [c1|c|x.c]ble r<=r n
      | [c|c1|x.c]ble r<=r n

c --> c'
------------------
L;I[c] --> L;I[c']

L;[v] --> L;v
L0,r->n;[fact]mov r<-n' --> L0,r->n';fact
L;[fact|fact]mov r1<-r2 --> L0,r1->L(r2);fact   where L=L0,r1->n
L;[fact|fact]add r1<-r2+n3 --> L0,r1->L(r2)+n3;fact   where L=L0,r1->n
L;[fact|fact|fact]add r1<-r2+r3 --> L0,r1->L(r2)+L(r3);fact   where L=L0,r1->n
L;[fact|fact,fact]load r1<-[r2+n3] --> L0,r1->L(L(r2)+n3);fact   where L=L0,r1->n
L;[fact|fact|fact]store [r1+n1]<-r2 --> L0,L(L(r1)+n1)->L(r2);fact   where L=L0,(L0(r1)+n1)->n

L(r1) > L(r2)
--------------------------------------
L;[fact|fact|x.c]ble r<=r n --> L;fact

L(r1) <= L(r2)
---------------------------------------------------------------------------------------
B |- L;let pat = [fact|fact|x.c3]ble r1<=r2 n in blk --> L;[[x<-le L(r1) L(r2)]c3]jmp n

L;ins --> L;ins'
-----------------------------------------------------------------
B |- L;let pat = ins in blk --> L;let pat = ins' in blk

L;ins --> L';v
-----------------------------------------------------
B |- L;let pat = ins in blk --> L';let pat = v in blk

pat<-v => [s]
--------------------------------------
B |- L;let pat = v in blk --> L;[s]blk

c --> c'
--------------------------------
B |- L;[c]jmp n --> L;[c']jmp n

c --> c'
-------------------------------------
B |- L;[c0;c]jmp r --> L;[c0;c']jmp r

c --> c'
-------------------------------------
B |- L;[c;c0]jmp r --> L;[c';c0]jmp r

pat<-v => [s]
----------------------------------------------------------------------------------------------
B,n->\A1:k1...\An:kj.\pat:t.blk |- L;[code(n)[t1...tj],v]jmp n --> L;[s][Aj<-tj]...[A1<-t1]blk

pat<-v => [s]
----------------------------------------------------------------------------------------------------
B,L(r)->\A1:k1...\Aj:kj.\pat:t.blk |- L;[code(L(r))[t1...tj],v]jmp r --> L;[s][Aj<-tj]...[A1<-t1]blk

c --> c'
----------------------------------------------------
(L;let pat = c in prog) --> (L;let pat = c' in prog)

pat<-e => [s]
-----------------------------------------------
(L;let pat = e in prog) --> (L;[s]prog)

B |- (L;blk) --> (L';blk')
--------------------------
(L;B blk) --> (L';B blk')

====================================================================