=================================================
=================== LANG1 =======================
=================================================

define based on lang0

=================================================
================== SYNTAX =======================
=================================================

same b,t,p,g,v,h,l,e

k = type | res | cap | cap+
_t = all A:cap+<=c.t | all A:cap<=c0,c1,...,cn.t
c = A | {} | {A p} | c1+c2
d = . | d,A:k | d,A:cap+<=c | d,A:cap<=c0,c1,...,cn
_h = \A:cap+<=c.h | \A:cap<=c0,c1,...,cn.h

=================================================
================= SEMANTICS =====================
=================================================

d |- .

d |- d'
----------- (A not in Dom(d,d'))
d |- d',A:k

d |- d'
d,d' |- c:cap+
----------------- (A not in Dom(d,d'))
d |- d',A:cap+<=c

d |- d'
d,d' |- c0:cap
d,d' |- c1:cap+ ... d,d' |- cn:cap+
----------------------------------- (A not in Dom(d,d'))
d |- d',A:cap<=c0,c1,...,cn

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

drop rule: all A<=c.t:type
drop rules: d |- c:cap

...,A:cap+<=c,... |- A:cap+

...,(A:cap<=c0,c1,...,cn),... |- A:cap

d |- c:cap+
d,A:cap+<=c |- t:type
------------------------- (A not in Dom(d))
d |- all A:cap+<=c.t:type

d |- c0:cap
d |- c1:cap+ ... d |- cn:cap+
d,A:cap<=c0,c1,...,cn |- t:type
------------------------------- (A not in Dom(d))
d |- all A:cap<=c0,c1,...,cn.t:type

d |- c:cap+
-----------
d |- c:cap

d |- {}:cap+

d |- A:res
--------------
d |- {A+}:cap+

d |- A:res
-------------
d |- {A~}:cap

d |- c1:k
d |- c2:k
------------ where k = cap or k = cap+
d |- c1+c2:k

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

drop rule: d |- c1 = /c1'
drop rule: d |- /c = /c+/c
drop rule: d |- /{} = {}
drop rule: d |- /{A~} = {A+}
drop rule: d |- //c = /c
drop rule: d |- /(c1+c2) = /c1+/c2

modify rules: "where k = cap" --> "where k = cap or k = cap+"

d |- c1 = c2:cap+
-----------------
d |- c1 = c2:cap

d |- c:cap+
-----------------
d |- c = c+c:cap+

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

drop rule: d |- /c <= /c'
drop rule: d |- c <= /c
drop rule: ...,A<=c,... |- A<=c
modify rules: "where k = cap" --> "where k = cap or k = cap+"

...,(A:k<=...,c,...),... |- A<=c

d |- A:res
-----------------
d |- {A~} <= {A+}

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

drop rule: d |- all A<=c.t = all A<=c'.t':type

d |- c = c':cap+
d,A:cap+<=c |- t = t':type
--------------------------------------------- (A not in Dom(d))
d |- all A:cap+<=c.t = all A:cap+<=c'.t':type

d |- c0 = c0':cap
d |- c1 = c1':cap+ ... d |- cn = cn':cap+
d,A:cap<=c0,c1,...,cn |- t = t':type
------------------------------------------------------------------- (A not in Dom(d))
d |- all A:cap<=c0,c1,...,cn.t = all A:cap<=c0',c1',...,cn'.t':type

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

drop rule: d;g |- \A<=c.h: all A<=c.t

d |- all A:k<=c1,...,cn.t: type
d,(A:k<=c1,...,cn);g |- h:t
---------------------------------------------- (A not in Dom(d))
d;g |- \A:k<=c1,...,cn.h: all A:k<=c1,...,cn.t

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

drop rule: d;g |- v[c:cap]: [A<-c]t

d;g |- v: all A:k<=c1,...,cn.t
d |- c <= c1 ... d |- c <= cn
d |- c:k
--------------------------------- where k = cap or k = cap+
d;g |- v[c:k]: [A<-c]t

=================================================
========== LANG0->LANG1 TRANSLATION =============
=================================================

T(A) = A
T(A handle) = A handle
T(all A:type.t) = all A:type.T(t)
T(all A:res.t) = all A:res.T(t)
T(all A:cap.t) = all As:cap+. all A:cap<=As. T(t)
T(all A<=c.t) = all As:cap+<=S(c). all A:cap<=C(c),As. T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>

C(A) = A
C({}) = {}
C({A p}) = {A p}
C(c1+c2) = C(c1)+C(c2)
C(/c) = S(c)

S(A) = As
S({}) = {}
S({A p}) = {A+}
S(c1+c2) = S(c1)+S(c2)
S(/c) = S(c)

D(.) = .
D(A:type,d) = A:type, D(d)
D(A:res,d) = A:res, D(d)
D(A:cap,d) = As:cap+, A:cap<=As, D(d)
D(A<=c,d) = As:cap+<=S(c), (A:cap<=C(c),As), D(d)

G(.) = .
G(x:t,g) = x:T(t),G(g)

V(x) = x
V(v[t:type]) = V(v)[T(t):type]
V(v[A:res]) = V(v)[A:res]
V(v[c:cap]) = V(v)[S(c):cap+][C(c):cap]

H(\A:type.h) = \A:type.H(h)
H(\A:res.h) = \A:res.H(h)
H(\A:cap.h) = \As:cap+.\A:cap<=As.H(h)
H(\A<=c.h) = \As:cap+<=S(c).\A:cap<=C(c),As.H(h)
H(\(c,x:t).e) = \(C(c),x:T(t)).E(e)
H(<v1,v2>) = <V(v1),V(v2)>

L(x=v) = x=V(v)
L(x=h) = x=H(h)
L(x=v.n) = x=V(v).n
L(new A,x) = new A,x
L(free v) = free V(v)
L(use v) = use V(v)

E(let l in e) = let L(l) in E(e)
E(v1 v2) = V(v1) V(v2)
E(halt) = halt

=================================================
=================== LEMMAS ======================
=================================================

Language lemmas:
  - if |- d and d |- g and d;g |- v:t then d |- t:type
  - if |- d and d |- g and d;g |- h:t then d |- t:type

Translation lemmas:
 -- if d |- c:cap then D(d) |- S(c):cap+
 -- if d |- c:cap then D(d) |- C(c):cap
 -- if d |- t:type then D(d) |- T(t):type
 -- if d |- d' then D(d) |- D(d')
 -- if d |- c1=c2:cap then D(d) |- S(c1)=S(c2):cap+
 -- if d |- c1=c2:cap then D(d) |- C(c1)=C(c2):cap
 -- if d |- t1=t2:type then D(d) |- T(t1)=T(t2):type
 -- if d |- c:cap then D(d) |- C(c)<=S(c)
 -- if d |- c1<=c2 then D(d) |- S(c1)<=S(c2)
 -- if d |- c1<=c2 then D(d) |- C(c1)<=C(c2)
 -- if |- d and d |- A':cap and d |- c:cap then S([A'<-c']c) = [A'<-C(c'),As'<-S(c')]S(c)
 -- if |- d and d |- A':cap and d |- c:cap then C([A'<-c']c) = [A'<-C(c'),As'<-S(c')]C(c)
 -- if |- d and d |- A':cap and d |- t:type then T([A'<-c']t) = [A'<-C(c'),As'<-S(c')]T(t)
 -- if |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t)
 -- if |- d and d |- g then D(d) |- G(g)
 -- if |- d and d |- g then:
    - if d;g |- v:t then D(d);G(g) |- V(v):T(t)
    - if d;g |- h:t then D(d);G(g) |- H(h):T(t)
    - if d;g;c |- l==>d';g';c' then D(d);G(g);C(c) |- L(l)==>D(d');G(g');C(c')
    - if d;g;c |- e then D(d);G(g);C(c) |- E(e)

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

If d |- c:cap then D(d) |- S(c):cap+

CASE:

...,A:cap,... |- A:cap

S(A) = As
D(...,A:cap,...) = ..., As:cap+, A:cap<=As, ...


CASE:

...,A<=c,... |- A:cap

S(A) = As
D(...,A<=c,...) = ..., As:cap+<=S(c), (A:cap<=C(c),As), ...


CASE:

d |- {}:cap

  S({}) = {}
  D(d) |- {}:cap+


d |- A:res
--------------
d |- {A p}:cap

  S({A p}) = {A+}
  D(d) |- {A+}:cap+


EASY CASES:

d |- c1:cap
d |- c2:cap
--------------
d |- c1+c2:cap

d |- c:cap
-----------
d |- /c:cap

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

If d |- c:cap then D(d) |- C(c):cap

CASE:

...,A:cap,... |- A:cap

C(A) = A
D(...,A:cap,...) = ..., As:cap+, A:cap<=As, ...


CASE:

C(A) = A
...,A<=c,... |- A:cap


CASE:

d |- {}:cap

  C({}) = {}
  D(d) |- {}:cap+
  ---------------
  D(d) |- {}:cap


CASE:

d |- A:res
--------------
d |- {A+}:cap

  C({A+}) = {A+}
  D(d) |- {A+}:cap+
  -----------------
  D(d) |- {A+}:cap


CASE:

d |- A:res
--------------
d |- {A~}:cap

  C({A~}) = {A~}
  D(d) |- {A~}:cap


CASE:

d |- c1:cap
d |- c2:cap
--------------
d |- c1+c2:cap

C(c1+c2) = C(c1)+C(c2)
By induction, D(d) |- C(c1):cap
By induction, D(d) |- C(c2):cap
By rule, D(d) |- C(c1)+C(c2):cap


CASE:

d |- c:cap
-----------
d |- /c:cap

C(/c) = S(c)
By lemma, D(d) |- S(c):cap+
By rule, D(d) |- S(c):cap

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

If d |- t:type then D(d) |- T(t):type

EASY CASES:

...,A:type,... |- A:type

d |- A:res
------------------
d |- A handle:type

d |- t1:type
d |- t2:type
-----------------
d |- <t1,t2>:type

d,A:k |- t:type
------------------- (where k=type or k=res)
d |- all A:k.t:type


CASE:

d,A:cap |- t:type
--------------------- (A not in Dom(d))
d |- all A:cap.t:type

Induction: D(d,A:cap) |- T(t):type
                                         D(d),As:cap+ |- As:cap+
                                         -----------------------
  D(d),As:cap+,A:cap<=As |- T(t):type    D(d),As:cap+ |- As:cap
  -------------------------------------------------------------
  D(d),As:cap+ |- all A:cap<=As.T(t):type


CASE:

d |- c:cap
d,A<=c |- t:type
-------------------- (A not in Dom(d))
d |- all A<=c.t:type

Lemma: D(d) |- S(c):cap+
Lemma: D(d) |- C(c):cap
Induction: D(d,A<=c) |- T(t):type
           D(d), As:cap+<=S(c), (A:cap<=C(c),As) |- T(t):type


EASY CASE:

d |- t:type
d |- c:cap
------------------
d |- (c,t)->0:type

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

If d |- d' then D(d) |- D(d')

EASY CASE:

d |- .


CASE:

d |- d'
----------- (A not in Dom(d,d'), k=type or k=res)
d |- d',A:k

Induction: D(d) |- D(d')
A not in Dom(D(d),D(d'))
By rule: D(d) |- D(d'),A:k


CASE:

d |- d'
------------- (A not in Dom(d,d'))
d |- d',A:cap

Induction: D(d) |- D(d')
A,As not in Dom(D(d),D(d'))
By rule: D(d) |- D(d'),As:cap+
By rule: D(d) |- D(d'),As:cap+,A:cap<=As


CASE:

d |- d'
d,d' |- c:cap
------------- (A not in Dom(d,d'))
d |- d',A<=c

Induction: D(d) |- D(d')
Lemma: D(d,d') |- S(c):cap+
Lemma: D(d,d') |- C(c):cap
By rule: D(d) |- D(d'),As:cap+<=S(c)
By rule: D(d) |- D(d'),As:cap+<=S(c),(A:cap<=C(c),As)

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

If d |- c1=c2:cap then D(d) |- S(c1)=S(c2):cap+

Abbreviations: S1 = S(s1), D = D(d), etc.

CASE:

d |- c:cap
--------------
d |- c = c:cap

  By lemma, D |- S(c):cap+
  By rule, D |- S(c) = S(c):cap+


EASY CASES:

d |- c2 = c1:cap
----------------
d |- c1 = c2:cap

d |- c1 = c2:cap
d |- c2 = c3:cap
----------------
d |- c1 = c3:cap

d |- c1 = c1':k
d |- c2 = c2':k
---------------------- where k = cap
d |- c1+c2 = c1'+c2':k

d |- c:k
--------------- where k = cap
d |- {}+c = c:k

d |- c1:k
d |- c2:k
-------------------- where k = cap
d |- c1+c2 = c2+c1:k

d |- c1:k
d |- c2:k
d |- c3:k
------------------------------ where k = cap
d |- (c1+c2)+c3 = c1+(c2+c3):k


CASE:

d |- c1 = c2:cap
-------------------
d |- /c1 = /c2:cap

  By induction, D |- S(c1) = S(c2):cap+
  S(/c1) = S(c1)
  S(/c2) = S(c2)


CASE:

d |- c:cap
-------------------
d |- /c = /c+/c:cap

  By lemma, D |- S(c):cap+
  By rule, D |- S(c) = S(c)+S(c):cap+
  S(/c) = S(c)


CASE:

d |- /{} = {}:cap

  S(/{}) = S({})


CASE:

d |- A:res
---------------------
d |- /{A~} = {A+}:cap

  S(/{A~}) = S({A~}) = {A+}
  S({A+}) = {A+}


CASE:

d |- c:cap
-----------------
d |- //c = /c:cap

  S(//c) = S(/c)


CASE:

d |- c1:cap
d |- c2:cap
---------------------------
d |- /(c1+c2) = /c1+/c2:cap

  S(/(c1+c2)) = S(c1+c2) = S(c1)+S(c2)
  S(/c1+/c2) = S(/c1)+S(/c2) = S(c1)+S(c2)


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

If d |- c1=c2:cap then D(d) |- C(c1)=C(c2):cap

Abbreviations: C1 = C(c1), D = D(d), etc.

CASE:

d |- c:cap
--------------
d |- c = c:cap

  By lemma, D |- C(c):cap
  By rule, D |- C(c) = C(c):cap


EASY CASES:

d |- c2 = c1:cap
----------------
d |- c1 = c2:cap

d |- c1 = c2:cap
d |- c2 = c3:cap
----------------
d |- c1 = c3:cap

d |- c1 = c1':k
d |- c2 = c2':k
---------------------- where k = cap
d |- c1+c2 = c1'+c2':k

d |- c:k
--------------- where k = cap
d |- {}+c = c:k

d |- c1:k
d |- c2:k
-------------------- where k = cap
d |- c1+c2 = c2+c1:k

d |- c1:k
d |- c2:k
d |- c3:k
------------------------------ where k = cap
d |- (c1+c2)+c3 = c1+(c2+c3):k


CASE:

d |- c1 = c2:cap
-------------------
d |- /c1 = /c2:cap

  By lemma, D |- S(c1) = S(c2):cap+
  By rule, D |- S(c1) = S(c2):cap
  C(/c1) = S(c1)
  C(/c2) = S(c2)


CASE:

d |- c:cap
-------------------
d |- /c = /c+/c:cap

  By lemma, D |- S(c) = S(c)+S(c):cap+
  By rule, D |- S(c) = S(c)+S(c):cap
  S(/c) = S(c)


CASE:

d |- /{} = {}:cap

  C(/{}) = S({}) = {}
  C({}) = {}


CASE:

d |- A:res
---------------------
d |- /{A~} = {A+}:cap

  C(/{A~}) = S({A~}) = {A+}
  C({A+}) = {A+}


CASE:

d |- c:cap
-----------------
d |- //c = /c:cap

  C(//c) = S(/c) = S(c)
  C(/c) = S(c)


CASE:

d |- c1:cap
d |- c2:cap
---------------------------
d |- /(c1+c2) = /c1+/c2:cap

  C(/(c1+c2)) = S(c1+c2) = S(c1)+S(c2)
  C(/c1+/c2) = C(/c1)+C(/c2) = S(c1)+S(c2)


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

If d |- t1=t2:type then D(d) |- T(t1)=T(t2):type

EASY CASES:

d |- t:type
---------------
d |- t = t:type

d |- t2 = t1:type
-----------------
d |- t1 = t2:type

d |- t1 = t2:type
d |- t2 = t3:type
-----------------
d |- t1 = t3:type

d |- t1 = t1':type
d |- t2 = t2':type
-----------------------------
d |- <t1,t2> = <t1',t2'>:type

d,A:k |- t = t':type
-------------------------------- (A not in Dom(d))
d |- all A:k.t = all A:k.t':type


CASE:

d |- c = c':cap
d,A<=c |- t = t':type
----------------------------------- (A not in Dom(d))
d |- all A<=c.t = all A<=c'.t':type

Lemma: D(d) |- S(c) = S(c'):cap+
Lemma: D(d) |- C(c) = C(c'):cap
Induction: D(d,A<=c) |- T(t) = T(t'):type
           D(d),As:cap+<=S(c), (A:cap<=C(c),As) |- T(t) = T(t'):type


EASY CASE:

d |- t = t':type
d |- c = c':cap
-------------------------------
d |- (c,t)->0 = (c',t')->0:type

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

If d |- c:cap then D(d) |- C(c)<=S(c)

Abbreviations: C1 = C(c1), S1 = S(c1), D = D(d), etc.

CASE:

...,A:cap,... |- A:cap

  D(...,A:cap,...) = ...,As:cap+, A:cap<=As, ...
  C(A) = A
  S(A) = As
  ...,As:cap+, A:cap<=As, ... |- A<=As


CASE:

...,A<=c,... |- A:cap

  D(...,A<=c,...) = ...,As:cap+<=S(c), (A:cap<=C(c),As),...
  C(A) = A

  ...,As:cap+<=S(c), (A:cap<=C(c),As),... |- A<=As
  ...,As:cap+<=S(c), (A:cap<=C(c),As),... |- As<=S(c)
  ---------------------------------------------------
  ...,As:cap+<=S(c), (A:cap<=C(c),As),... |- A<=S(c)


CASE:

d |- {}:cap

  C({}) = {}
  S({}) = {}
  D |- {} <= {}


CASE:

d |- A:res
--------------
d |- {A~}:cap

  C({A~}) = {A~}
  S({A~}) = {A+}
  By, rule, D |- {A~}<={A+}


CASE:

d |- A:res
--------------
d |- {A+}:cap

  C({A+}) = {A+}
  S({A+}) = {A+}
  D |- {A+}<={A+}


CASE:

d |- c1:cap
d |- c2:cap
--------------
d |- c1+c2:cap

  By induction, D |- C1<=S1
  By induction, D |- C2<=S2
  C(c1+c2) = C1+C2
  S(c1+c2) = S1+S2
  By rule, D |- C1+C2<=S1+S2


CASE:

d |- c:cap
-----------
d |- /c:cap

  By lemma, D |- S(c):cap+
  C(/c) = S(c)
  S(/c) = S(c)
  D |- S(c)<=S(c)


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

If d |- c1<=c2 then D(d) |- S(c1)<=S(c2)

Abbreviations: C1 = C(c1), S1 = S(c1), D = D(d), etc.

EASY CASES:

d |- c1 = c2:k
-------------- where k = cap
d |- c1 <= c2

d |- c1 <= c2
d |- c2 <= c3
-------------
d |- c1 <= c3

d |- c1 <= c1'
d |- c2 <= c2'
---------------------
d |- c1+c2 <= c1'+c2'


CASE:

d |- c1 <= c2
---------------
d |- /c1 <= /c2

  S(/c1) = S(c1)
  S(/c2) = S(c2)
  By induction, D |- S(c1)<=S(c2)


CASE:

...,A<=c,... |- A<=c

  D(...,A<=c,...) = ...,As:cap+<=S(c), (A:cap<=C(c),As),...
  S(A) = As
  ...,As:cap+<=S(c), (A:cap<=C(c),As),... |- As<=S(c)


CASE:

d |- c:cap
------------
d |- c <= /c

  S(/c) = S(c)


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

If d |- c1<=c2 then D(d) |- C(c1)<=C(c2)

Abbreviations: C1 = C(c1), S1 = S(c1), D = D(d), etc.

EASY CASES:

d |- c1 = c2:k
-------------- where k = cap
d |- c1 <= c2

d |- c1 <= c2
d |- c2 <= c3
-------------
d |- c1 <= c3

d |- c1 <= c1'
d |- c2 <= c2'
---------------------
d |- c1+c2 <= c1'+c2'


CASE:

d |- c1 <= c2
---------------
d |- /c1 <= /c2

  C(/c1) = S(c1)
  C(/c2) = S(c2)
  By lemma, D |- S(c1)<=S(c2)


CASE:

...,A<=c,... |- A<=c

  D(...,A<=c,...) = ...,As:cap+<=S(c), (A:cap<=C(c),As),...
  C(A) = A
  ...,As:cap+<=S(c), (A:cap<=C(c),As),... |- A<=C(c)


CASE:

d |- c:cap
------------
d |- c <= /c

  C(/c) = S(c)
  By lemma, D |- C(c)<=S(c)


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

If |- d and d |- A':cap and d |- c:cap then S([A'<-c']c) = [A'<-C(c'),As'<-S(c')]S(c)

CASE

S(A') = As'

S([A'<-c']A') = S(c')
[A'<-C(c'),As'<-S(c')]S(A') = [A'<-C(c'),As'<-S(c')]As' = S(c')


CASE

S(A) = As

S([A'<-c']A) = As where A!=A'
[A'<-C(c'),As'<-S(c')]S(A) = [A'<-C(c'),As'<-S(c')]As = As
  (where As'!=As and A'!=As because A!=A')


CASE:

S({A' p}) = {A'+}

Impossible case: d |- A':cap and d |- A':res cannot both be true


EASY CASES:

S({}) = {}
S({A p}) = {A+}
S(c1+c2) = S(c1)+S(c2)
S(/c) = S(c)


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

If |- d and d |- A':cap and d |- c:cap then C([A'<-c']c) = [A'<-C(c'),As'<-S(c')]C(c)

CASE:

C(A') = A'

C([A'<-c']A') = C(c')
[A'<-C(c'),As'<-S(c')]C(A') = [A'<-C(c'),As'<-S(c')]A' = C(c')


EASY CASES:

C(A) = A
C({}) = {}
C({A p}) = {A p}
C({A' p}) = {A' p}
C(c1+c2) = C(c1)+C(c2)


CASE:

C(/c) = S(c)

C([A'<-c']/c) = C(/[A'<-c']/c) = S([A'<-c']c)
[A'<-C(c'),As'<-S(c')]C(/c) = [A'<-C(c'),As'<-S(c')]S(c)
By Lemma, S([A'<-c']c) = [A'<-C(c'),As'<-S(c')]S(c)

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

If |- d and d |- A':cap and d |- t:type then T([A'<-c']t) = [A'<-C(c'),As'<-S(c')]T(t)


CASE:

T(A') = A'
Impossible case: d |- A':cap and d |- A':type cannot both be true


EASY CASES:

T(A) = A
T(A handle) = A handle
T(A' handle) = A' handle
T(all A:type.t) = all A:type.T(t)
T(all A:res.t) = all A:res.T(t)
T(all A:cap.t) = all As:cap+. all A:cap<=As. T(t)
T(all A<=c.t) = all As:cap+<=S(c). all A:cap<=C(c),As. T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>


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

If |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t)

(easy supporting lemmas:
If |- d and d |- A':type and d |- c:cap then S([A'<-t']c) = [A'<-T(t')]S(c)
If |- d and d |- A':type and d |- c:cap then C([A'<-t']c) = [A'<-T(t')]C(c)
)


EASY CASES:

T(A') = A'
T(A) = A
T(A handle) = A handle
T(A' handle) = A' handle
T(all A:type.t) = all A:type.T(t)
T(all A:res.t) = all A:res.T(t)
T(all A:cap.t) = all As:cap+. all A:cap<=As. T(t)
T(all A<=c.t) = all As:cap+<=S(c). all A:cap<=C(c),As. T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>

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

If |- d and d |- g then D(d) |- G(g)

easy induction using lemma: if d |- t:type then D(d) |- T(t):type

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

If |- d and d |- g then:
  - if d;g |- v:t then D(d);G(g) |- V(v):T(t)
  - if d;g |- h:t then D(d);G(g) |- H(h):T(t)
  - if d;g;c |- l==>d';g';c' then D(d);G(g);C(c) |- L(l)==>D(d');G(g');C(c')
  - if d;g;c |- e then D(d);G(g);C(c) |- E(e)

V(v[t:type]) = V(v)[T(t):type]
V(v[A:res]) = V(v)[A:res]
V(v[c:cap]) = V(v)[S(c):cap+][C(c):cap]
H(\A:type.h) = \A:type.H(h)
H(\A:res.h) = \A:res.H(h)
H(\A:cap.h) = \As:cap+.\A:cap<=As.H(h)
H(\A<=c.h) = \As:cap+<=S(c).\A:cap<=C(c),As.H(h)
H(\(c,x:t).e) = \(C(c),x:T(t)).E(e)
H(<v1,v2>) = <V(v1),V(v2)>
L(x=v) = x=V(v)
L(x=h) = x=H(h)
L(x=v.n) = x=V(v).n
L(new A,x) = new A,x
L(free v) = free V(v)
L(use v) = use V(v)
E(let l in e) = let L(l) in E(e)
E(v1 v2) = V(v1) V(v2)
E(halt) = halt


EASY CASE:

d,A:k;g |- h:t
------------------------ (k=type or k=res) (A not in Dom(d))
d;g |- \A:k.h: all A:k.t


CASE:

d,A:cap;g |- h:t
---------------------------- (A not in Dom(d))
d;g |- \A:cap.h: all A:cap.t

D(d),As:cap+ |- As:cap+
-----------------------
D(d),As:cap+ |- As:cap

By lemma: d |- all A:cap.t:type
          d,A:cap |- t:type
By lemma: D(d,A:cap) |- T(t):type
          D(d),As:cap+,A:cap<=As |- T(t):type
          ---------------------------------------
          D(d),As:cap+ |- all A:cap<=As.T(t):type
          -------------------------------------------
          D(d) |- all As:cap+.all A:cap<=As.T(t):type

H(\A:cap.h) = \As:cap+.\A:cap<=As.H(h)
Induction: D(d,A:cap);G(g) |- H(h):T(t)
           D(d),As:cap+,A:cap<=As;G(g) |- H(h):T(t)    
           -------------------------------------------------------
           D(d),As:cap+;G(g) |- \A:cap<=As.H(h):all A:cap<=As.T(t)
           --------------------------------------------------------------------
           D(d);G(g) |- \As:cap+.\A:cap<=As.H(h):all As:cap+.all A:cap<=As.T(t)


CASE:

d |- c:cap
d,A<=c;g |- h:t
-------------------------- (A not in Dom(d))
d;g |- \A<=c.h: all A<=c.t

By lemma: d |- all A<=c.t:type
          d,A<=c |- t:type    d |- c:cap
By lemma: D(d) |- C(c):cap    D(d) |- S(c):cap+
By lemma: D(d,A<=c) |- T(t):type
          D(d),As:cap+<=S(c), (A:cap<=C(c),As) |- T(t):type
          ---------------------------------------------------
          D(d),As:cap+<=S(c) |- all A:cap<=C(c),As. T(t):type
          --------------------------------------------------------
          D(d) |- all As:cap+<=S(c). all A:cap<=C(c),As. T(t):type

T(all A<=c.t) = all As:cap+<=S(c). all A:cap<=C(c),As. T(t)
H(\A<=c.h) = \As:cap+<=S(c).\A:cap<=C(c),As.H(h)

Induction: D(d,A<=c);G(g) |- H(h):T(t)
           D(d),As:cap+<=S(c),(A:cap<=C(c),As);G(g) |- H(h):T(t)
           -------------------------------------------------------------------------
           D(d),As:cap+<=S(c);G(g) |- \A:cap<=C(c),As.H(h): all A:cap<=C(c),As. T(t)
           ---------------------------------------------------------------------------------------------
           D(d);G(g) |- \As:cap+<=S(c).\A:cap<=C(c),As.H(h): all As:cap+<=S(c). all A:cap<=C(c),As. T(t)


EASY CASES:

d |- c:cap
d |- t:type
d;g,x:t;c |- e
--------------------------- (x not in Dom(g))
d;g |- \(c,x:t).e: (c,t)->0

d;g |- v1: t1
d;g |- v2: t2
-----------------------
d;g |- <v1,v2>: <t1,t2>


CASE:

d;g |- h: t'
d |- t' = t:type
----------------
d;g |- h: t

Lemma: D(d) |- T(t')=T(t):type



CASE:

d;...,x:t,... |- x: t

V(x) = x
G(...,x:t,...) = ...,x:T(t),...


EASY CASE:

d;g |- v: all A:k.t
d |- b:k
---------------------- where k=type or k=cap
d;g |- v[b:k]: [A<-b]t


CASE:

d;g |- v: all A:cap.t
d |- c:cap
------------------------
d;g |- v[c:cap]: [A<-c]t

By lemma: d |- all A:cap.t
          d,A:cap |- t

V(v[c:cap]) = V(v)[S(c):cap+][C(c):cap]
T(all A:cap.t) = all As:cap+. all A:cap<=As. T(t)
By lemma: T([A<-c]t) = [A<-C(c),As<-S(c)]T(t)
By lemma: D(d) |- C(c)<=S(c)

Induction: D(d);G(g) |- V(v): T(all A:cap.t)
           D(d);G(g) |- V(v): all As:cap+. all A:cap<=As. T(t)
           ----------------------------------------------------------
           D(d);G(g) |- V(v)[S(c):cap+]: [As<-S(c)]all A:cap<=As. T(t)
           D(d);G(g) |- V(v)[S(c):cap+]: all A:cap<=S(c). [As<-S(c)]T(t)
           ---------------------------------------------------------------
           D(d);G(g) |- V(v)[S(c):cap+][C(c):cap]: [A<-C(c)][As<-S(c)]T(t)

[A<-C(c)][As<-S(c)] = [A<-C(c),As<-S(c)] because A is not in freevars(S(c))


CASE:

d;g |- v: all A<=c'.t
d |- c <= c'
------------------------
d;g |- v[c:cap]: [A<-c]t

V(v[c:cap]) = V(v)[S(c):cap+][C(c):cap]
T(all A<=c'.t) = all As:cap+<=S(c'). all A:cap<=C(c'),As. T(t)
By lemma: T([A<-c]t) = [A<-C(c),As<-S(c)]T(t)
By lemma: D(d) |- S(c)<=S(c')
By lemma: D(d) |- C(c)<=C(c')
By lemma: D(d) |- C(c)<=S(c)

Induction: D(d);G(g) |- V(v): T(all A<=c'.t)
           D(d);G(g) |- V(v): all As:cap+<=S(c'). all A:cap<=C(c'),As. T(t)
           -----------------------------------------------------------------
           D(d);G(g) |- V(v)[S(c):cap+]: [As<-S(c)]all A:cap<=C(c'),As. T(t)
           D(d);G(g) |- V(v)[S(c):cap+]: all A:cap<=C(c'),S(c). [As<-S(c)]T(t)
           -------------------------------------------------------------------
           D(d);G(g) |- V(v)[S(c):cap+][C(c):cap]: [A<-C(c)][As<-S(c)]T(t)

[A<-C(c)][As<-S(c)] = [A<-C(c),As<-S(c)] because A is not in freevars(S(c))


EASY CASES:

d;g |- v: t'
d |- t' = t:type
----------------
d;g |- v: t

d;g |- v:t
-------------------------- (x not in Dom(g))
d;g;c |- x=v ==> d;g,x:t;c

d;g |- h:t
-------------------------- (x not in Dom(g))
d;g;c |- x=h ==> d;g,x:t;c

d;g |- v:<t_1,t_2>
------------------------------ (x not in Dom(g) and 1<=n<=2)
d;g;c |- x=v.n ==> d;g,x:t_n;c


CASE:

d;g;c |- new A,x ==> d,A:res;g,x:A handle;c+{A~} (A not in Dom(d) and x not in Dom(g))

C(c+{A~}) = C(c)+{A~}


EASY CASE:

d;g |- v: A handle
d |- c = c'+{A~}:cap
--------------------------
d;g;c |- free v ==> d;g;c'


CASE:

d;g |- v: A handle
d |- c <= c'+{A+}
------------------------
d;g;c |- use v ==> d;g;c

Induction: D(d);G(g) |- V(v): A handle
Lemma: D(d) |- C(c) <= C(c'+{A+})
       D(d) |- C(c) <= C(C')+{A+}


EASY CASES:

d;g;c |- l ==> d';g';c'
d';g';c' |- e
-----------------------
d;g;c |- let l in e

d;g |- v1: (c',t)->0
d;g |- v2: t
d |- c <= c'
--------------------
d;g;c |- v1 v2

d |- c = {}:cap
---------------
d;g;c |- halt

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