=================================================
=================== LANG2 =======================
=================================================

define based on lang0

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

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

k = type | res | cap p
b = A | t | q
_t = all A:cap+ where u1#A<=a1,...,un#A<=an.t
q,u,a = A | {} | {A p} | q1+q2
c = u#a
d = . | d,A:k | d,A:cap+ where u1#A<=a1,...,un#A<=an
_h = \A:cap+ where u1#A<=a1,...,un#A<=an.h

by convention:
  u:cap~
  a:cap+

Let d |- u#a:cap mean d |- u:cap~ and d |- a:cap+
Let d |- u#a=u'#a':cap mean d |- u=u':cap~ and d |- a=a':cap+

[Question: can {A p} be written as just {A}?]

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

d |- .

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

d |- d'
d,d' |- u1:cap~ ... d,d' |- un:cap~
d,d' |- a1:cap+ ... d,d' |- an:cap+
------------------------------------------ (A not in Dom(d,d'))
d |- d',A:cap+ where u1#A<=a1,...,un#A<=an

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

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

...,A:cap+ where u1#A<=a1,...,un#A<=an,... |- A:cap+

d |- u1:cap~ ... d |- un:cap~
d |- a1:cap+ ... d |- an:cap+
d,A:cap+ where u1#A<=a1,...,un#A<=an |- t:type
-------------------------------------------------- (A not in Dom(d))
d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t:type

d |- {}:cap p

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

d |- q1:cap p
d |- q2:cap p
----------------
d |- q1+q2:cap p

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

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 p"
modify rules: c,c1,c1',c2,c2',c3 --> q,q1,q1',q2,q2',q3

d |- a:cap+
-----------------
d |- a = a+a:cap+

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

drop rules: d |- c1 <= c2

...,(A:cap+ where ...,u#A<=a,...),... |- u#A<=a

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

d |- a1 = a2:cap+
-----------------
d |- {}#a1 <= a2

d |- u1#a1 <= a2
d |- u2#a2 <= a3
-------------------
d |- u1+u2#a1 <= a3

d |- u1#a1 <= a1'
d |- u2#a2 <= a2'
---------------------------
d |- u1+u2#a1+a2 <= a1'+a2'

d |- u:cap~
d |- a:cap+
-------------- (optional)
d |- u#a <= {}

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

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

d |- u1 = u1':cap~ ... d |- un = un':cap~
d |- a1 = a1':cap+ ... d |- an = an':cap+
d,A:cap+ where u1#A<=a1,...,un#A<=an |- t = t':type
-------------------------------------------------------------------------------------------------- (A not in Dom(d))
d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t = all A:cap+ where u1'#A<=a1',...,un'#A<=an'.t':type

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

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

d |- all A:cap+ where u1#A<=a1,...,un#A<=an.t: type
d,(A:cap+ where u1#A<=a1,...,un#A<=an);g |- h:t
--------------------------------------------------- (A not in Dom(d))
d;g |- \A:cap+ where u1#A<=a1,...,un#A<=an.h:
         all A:cap+ where u1#A<=a1,...,un#A<=an.t

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

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



d;g |- v: all A:cap+ where u1#A<=a1,...,un#A<=an.t
d |- u1#a <= a1 ... d |- un#a <= an
d;g |- a:cap+
--------------------------------------------------
d;g |- v[a:cap+]: [A<-a]t

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

drop rule: d;g |- new A,x
drop rule: d;g |- free v
drop rule: d;g |- use v

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

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

d;g |- v: A handle
//d;g |- c <= {A+} (optional)
c = u#a
d |- u = u1+u2:cap~
d |- u1#a <= a'+{A+}
------------------------
d;g;c |- use v ==> d;g;c

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

drop rule: d;g;c |- v1 v2
drop rule: d;g;c |- halt

d;g |- v1: (u'#a',t)->0
d;g |- v2: t
d |- u = ub+u':cap~
d |- ub#a <= a'
-----------------------
d;g;u#a |- v1 v2

d |- u = {}:cap~
d |- a = {}:cap+
----------------
d;g;u#a |- halt

=================================================
========== LANG1->LANG2 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 Aa:cap+. all Au:cap~. T(t)
T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t)
T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t)
T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>

U(A) = Au
U({}) = {}
U({A~}) = {A~}
U({A+}) = {}
U(c1+c2) = U(c1)+U(c2)

A(A) = Aa
A({}) = {}
A({A~}) = {}
A({A+}) = {A+}
A(c1+c2) = A(c1)+A(c2)

C(c) = U(c)#A(c)

D(.) = .
D(A:type,d) = A:type, D(d)
D(A:res,d) = A:res, D(d)
D(A:cap,d) = Aa:cap+, Au:cap~, D(d)
D(A:cap+,d) = Aa:cap+. [Au<-{}]D(d)
D(A:cap+<=c,d) = Aa:cap+ where {}#Aa<=A(c), [Au<-{}]D(d)
D(A:cap<=c0,c1,...,cn,d) = Ab:cap~, Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), [Au<-Ab+U(c0)]D(d)

[.] = []
[A:type,d] = [d]
[A:res,d] = [d]
[A:cap,d] = [d]
[A:cap+,d] = [Au<-{}][d]
[A:cap+<=c,d] = [Au<-{}][d]
[A:cap<=c0,c1,...,cn,d] = [Au<-Ab+U(c0)][d]

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

d;g |- v:t ~~> v'
d;g |- h:t ~~> h'
d;g;c |- l ==> d';g';c' ~~> l'
d;g;c |- e ~~> e'
(ugly, but probably relegated to the appendix or TR anyway)

V(x) = x
V(v[t:type]) = V(v)[T(t):type]
V(v[A:res]) = V(v)[A:res]

d;g |- v: all A:cap.t ~~> v'
d |- c:cap
-----------------------------------------------------
d;g |- v[c:cap]: [A<-c]t ~~> v'[A(c):cap+][U(c):cap~]

d;g |- v: all A:cap+.t ~~> v'
d |- c:cap+
-------------------------------------------
d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+]

d;g |- v: all A:cap+<=c0.t ~~> v'
d |- c <= c0
d |- c:cap+
-------------------------------------------
d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+]

d;g |- v: all A:cap<=c0,...,cn.t ~~> v'
d |- c <= c0 ~~> ub
d |- c <= c1 ... d |- c <= cn
d |- c:cap
---------------------------------------------------
d;g |- v[c:cap]: [A<-c]t ~~> v'[ub:cap~][A(c):cap+]

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

H(\A:type.h) = \A:type.H(h)
H(\A:res.h) = \A:res.H(h)
H(\A:cap.h) = \Aa:cap+.\Au:cap~.H(h)
H(\A:cap+.h) = \Aa:cap+.[Au<-{}]H(h)
H(\A:cap+<=c.h) = \Aa:cap+ where {}#Aa<=A(c).[Au<-{}]H(h)
H(\A:cap<=c0,c1,...,cn.h) =  \Ab:cap~. \Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]H(h)
H(\(c,x:t).e) = \(C(c),x:T(t)).E(e)
H(<v1,v2>) = <V(v1),V(v2)>

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

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

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

d |- c1 = c2:k
-------------------- where k = cap or k = cap+
d |- c1 <= c2 ~~> {}

d |- c1 <= c2 ~~> u
d |- c2 <= c3 ~~> u'
----------------------
d |- c1 <= c3 ~~> u+u'

d |- c1 <= c1' ~~> u1
d |- c2 <= c2' ~~> u2
-------------------------------
d |- c1+c2 <= c1'+c2' ~~> u1+u2

...,(A:cap+<=c),... |- A<=c ~~> {}

...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab

...,(A:cap<=c0,...,ck,...),... |- A<=ck ~~> Ab+U(c0)

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

// (optional)
//d |- c:cap
//---------------------
//d |- c <= {} ~~> U(c)

=================================================
=================== 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
  - if |- d and d |- [A<-c1]t:type and d |- c1=c2:cap~ then d |- [A<-c1]t=[A<-c2]t:type

Translation lemmas:
 -- if |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]U(c):cap~
 -- if |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]A(c):cap+
 -- if |- d and d |- c1<=c2~~>u then D(d) |- [d]u:cap~
 -- if d |- d' then D(d) |- [d]D(d')
 -- if |- d and d |- t:type then D(d) |- [d]T(t):type
 -- if |- d and d |- c:cap+ then D(d) |- [d]U(c)={}:cap~
 -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]U(c1)=[d]U(c2):cap~
 -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]A(c1)=[d]A(c2):cap+
 -- if |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type
 -- if |- d and d |- c1<=c2~~>u then D(d) |- [d]U(c1)=[d]u+[d]U(c2):cap~ and D(d) |- [d]u#[d]A(c1)<=[d]A(c2)
      corollary: if |- d and d |- c1<=c2 and d |- c2:cap+ then D(d) |- [d]U(c1)#[d]A(c1)<=[d]A(c2)
 -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then A([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]A(c)
 -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then U([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]U(c)
 -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- t:type then T([A'<-c']t) = [Au'<-U(c'),Aa'<-A(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) |- [d]G(g)
 -- if |- d and d |- g then:
    - if d;g |- v:t ~~> v' then D(d);[d]G(g) |- [d]v':[d]T(t)
    - if d;g |- h:t ~~> h' then D(d);[d]G(g) |- [d]h':[d]T(t)
    - if d;g;c |- l==>d';g';c' ~~> l' then D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c') and [d]=[d']
    - if d;g;c |- e ~~> e' then D(d);[d]G(g);[d]C(c) |- [d]e'

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

If |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]U(c):cap~

By induction on d, then by induction on derivation of d |- c:k

CASE:

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

[...,A:cap,...]U(A) = [...,A:cap,...]Au = Au
D(...,A:cap,...) = ...,Aa:cap+,Au:cap~,...


CASE:

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

[...,A:cap+,...]U(A) = [...,A:cap+,...]Au = {}


CASE:

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

[...,A:cap+<=c,...]U(A) = [...,A:cap+<=c,...]Au = {}


CASE:

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

d = d1,(A:cap<=c0,c1,...,cn),d2
|- d1,(A:cap<=c0,c1,...,cn),d2 implies d1 |- c0:cap
By induction, D(d1) |- [d1]U(c0):cap~
[d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1
By weakening, D(d) |- [d]U(c0):cap~

[...,(A:cap<=c0,c1,...,cn),...]U(A) = [...,(A:cap<=c0,c1,...,cn),...]Au = Ab+U(c0)
D(...,(A:cap<=c0,c1,...,cn),...) = Ab:cap~, Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)]D(d)


EASY CASES:

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

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

If |- d and d |- c:k and k=cap or k=cap+ then D(d) |- [d]A(c):cap+


CASE:

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

[...,A:cap,...]A(A) = [...,A:cap,...]Aa = Aa
D(...,A:cap,...) = ...,Aa:cap+,Au:cap~,...


CASE:

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

[...,A:cap+,...]A(A) = [...,A:cap+,...]Aa = Aa
D(...,A:cap+,...) = ...,Aa:cap+,...


CASE:

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

[...,A:cap+<=c,...]A(A) = [...,A:cap+<=c,...]Aa = Aa
D(...,A:cap+<=c,...) = ...,Aa:cap+ where {}#Aa<=A(c),...


CASE:

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

[...,(A:cap<=c0,c1,...,cn),...]A(A) = [...,(A:cap<=c0,c1,...,cn),...]Aa = Aa
D(...,(A:cap<=c0,c1,...,cn),...) = Ab:cap~, Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)]D(d)


EASY CASES:

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

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

If |- d and d |- c1<=c2~~>u then D(d) |- [d]u:cap~

EASY CASES:

d |- c1 = c2:k
-------------------- where k = cap or k = cap+
d |- c1 <= c2 ~~> {}

d |- c1 <= c2 ~~> u
d |- c2 <= c3 ~~> u'
----------------------
d |- c1 <= c3 ~~> u+u'

d |- c1 <= c1' ~~> u1
d |- c2 <= c2' ~~> u2
-------------------------------
d |- c1+c2 <= c1'+c2' ~~> u1+u2

...,(A:cap+<=c),... |- A<=c ~~> {}


CASE:

...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab

D(...,(A:cap<=c0,...),...) = ..., Ab:cap~, Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), ...


CASE:

d1,(A:cap<=c0,...,ck,...),d2 |- A<=c ~~> Ab+U(c0)
d = d1,(A:cap<=c0,...,ck,...),d2

|- d1,(A:cap<=c0,...,ck,...),d2 implies that d1 |- c0:cap
By weakening, d |- c0:cap
By lemma, D(d) |- [d]U(c0):cap~

D(d) = ..., Ab:cap~, Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn), ...
[d] = [d1][Au<-Ab+U(c0)][d2]


EASY CASE:

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


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

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

(Note: D(d,d') = D(d),[d]D(d'))

EASY CASES:

d |- .

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


CASE:

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

Induction: D(d) |- [d]D(d')
Aa not in Dom(D(d),[d]D(d'))
By rule, D(d) |- [d]D(d'),Aa:cap+


CASE:

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

Induction: D(d) |- [d]D(d')
Lemma: D(d,d') |- [d]A(c):cap+
By rule, D(d) |- [d]D(d'),Aa:cap+ where {}#Aa<=[d]A(c)


CASE:

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

Induction: D(d) |- [d]D(d')
Lemma: D(d,d') |- [d]U(c0):cap~
Lemma: D(d,d') |- [d]A(c0):cap+
Lemma: D(d,d') |- [d]A(ck):cap+ for 1<=k<=n
By rule, D(d) |- [d]D(d'),Ab:cap~
By rule, D(d) |- [d]D(d'),Ab:cap~,Aa:cap+
  where [d]Ab#Aa<=[d]A(c0),[d]Ab+[d]U(c0)#Aa<=[d]A(c1),...,[d]Ab+[d]U(c0)#Aa<=[d]A(cn)


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

If |- d and d |- t:type then D(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 or k=cap)
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+) |- [d,A:cap+]T(t):type

  D(d),A:cap+ |- [d][Au<-{}]T(t):type
  -----------------------------------------
  D(d) |- all Aa:cap+. [d][Au<-{}]T(t):type


CASE:

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

Lemma: D(d) |- [d]A(c):cap+
Induction: D(d,A:cap+<=c) |- [d,A:cap+<=c]T(t):type

  D(d),Aa:cap+ where {}#Aa<=[d]A(c) |- [d][Au<-{}]T(t):type
  --------------------------------------------------------------
  D(d) |- all Aa:cap+ where {}#Aa<=[d]A(c). [d][Au<-{}]T(t):type


CASE:

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

Lemma: D(d) |- [d]A(c0):cap+
Lemma: D(d) |- [d]U(c0):cap~
Lemma: D(d) |- [d]A(ck):cap+ where 1<=k<=n
Induction: D(d,A:cap<=c0,c1,...,cn) |- [d,A:cap<=c0,c1,...,cn]T(t):type
Au not in freevars(U(ck)), because A not in freevars(ck)
Au not in freevars(A(c0)), because A not in freevars(c0)

  D(d),Ab:cap~, Aa:cap+
      where [d]Ab#Aa<=[d][Au<-Ab+U(c0)]A(c0),
      [d]Ab+[d][Au<-Ab+U(c0)]U(c0)#Aa<=[d][Au<-Ab+U(c0)]A(c1),...,
      [d]Ab+[d][Au<-Ab+U(c0)]U(c0)#Aa<=[d][Au<-Ab+U(c0)]A(cn)
  |- [d][Au<-Ab+U(c0)]T(t):type
  --------------------------------------------
  D(d) |- all Ab:cap~. all Aa:cap+
            where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=A(c1),...,Ab+[d]U(c0)#Aa<=A(cn). [d][Au<-Ab+U(c0)] T(t)


EASY CASE:

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

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

If |- d and d |- c:cap+ then D(d) |- [d]U(c)={}:cap~

Abbreviations: D = D(d), U1 = [d]U(c1), A1 = [d]A(c1), etc.

CASE:

d1,A:cap+,d2 |- A:cap+
[d1,A:cap+,d2]U(A) = [d1][Au<-{}][d2]Au = {}


CASE:

d1,A:cap+<=c,d2 |- A:cap+
[d1,A:cap+<=c,d2]U(A) = [d1][Au<-{}][d2]Au = {}


CASE:

d |- {}:cap+
  U({}) = {}


CASE:

d |- A:res
--------------
d |- {A+}:cap+
  U({A+}) = {}


CASE:

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

Induction: D(d) |- [d]U(c1)={}:cap~
Induction: D(d) |- [d]U(c2)={}:cap~

  D(d) |- [d]U(c1)={}:cap~    D(d) |- [d]U(c2)={}:cap~    D(d) |- {}:cap~
  ----------------------------------------------------    ---------------------
  D(d) |- [d]U(c1)+[d]U(c2)={}+{}:cap~                    D(d) |- {}+{}={}:cap~
  -----------------------------------------------------------------------------
  D(d) |- [d]U(c1)+[d]U(c2)={}:cap~

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

If |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]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:cap+<=c |- t = t':type
--------------------------------------------- (A not in Dom(d))
d |- all A:cap+<=c.t = all A:cap+<=c'.t':type

similar to proof for lemma "If |- d and d |- t:type then D(d) |- [d]T(t):type"


CASE:

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

similar to proof for lemma "If |- d and d |- t:type then D(d) |- [d]T(t):type"


EASY CASE:

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


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

If |- d and d |- c1<=c2~~>u then D(d) |- [d]U(c1)=[d]u+[d]U(c2):cap~ and D(d) |- [d]u#[d]A(c1)<=[d]A(c2)
Corollary:
  If |- d and d |- c1<=c2 and d |- c2:cap+ then D(d) |- [d]U(c1)#[d]A(c1)<=[d]A(c2)

Abbreviations: D = D(d), U1 = [d]U(c1), A1 = [d]A(c1), etc.
Abbreviations: Ux = [d]ux, Uy = [d]uy
(If d |- c1<=c2~~>ux then D |- U1=Ux+U2:cap~ and D |- Ux#A1<=A2)


Proof of corollary:
  By lemma, D |- U2={}:cap~
  By main lemma, D |- U1=Ux+U2:cap~
                 D |- U1=Ux+{}:cap~
                 D |- U1=Ux:cap~
  By main lemma, D |- Ux#A1<=A2
                 D |- U1#A1<=A2


Proof of main lemma:

CASE:

d |- c1 = c2:k
-------------------- where k = cap or k = cap+
d |- c1 <= c2 ~~> {}

By lemma, D |- U1=U2:cap~
By rule, D |- {}+U2=U2:cap~, so D |- U1={}+U2:cap~

By lemma, D |- A1=A2:cap+
By rule, D |- {}#A1<=A2


CASE:

d |- c1 <= c2 ~~> ux
d |- c2 <= c3 ~~> uy
-----------------------
d |- c1 <= c3 ~~> ux+uy

Induction:
  D |- U1=Ux+U2:cap~ and D |- Ux#A1<=A2
  D |- U2=Uy+U3:cap~ and D |- Uy#A2<=A3

                      D |- Ux=Ux:cap~    D |- U2=Uy+U3:cap~
                      -------------------------------------
D |- U1=Ux+U2:cap~    D |- Ux+U2=Ux+(Uy+U3):cap~
------------------------------------------------
D |- U1=Ux+(Uy+U3):cap~
-----------------------
D |- U1=(Ux+Uy)+U3:cap~

D |- Ux#A1<=A2    D |- Uy#A2<=A3
--------------------------------
D |- Ux+Uy#A1<=A3


CASE:

d |- c1 <= c1' ~~> ux
d |- c2 <= c2' ~~> uy
-------------------------------
d |- c1+c2 <= c1'+c2' ~~> ux+uy

Induction:
  D |- U1=Ux+U1':cap~ and D |- Ux#A1<=A1'
  D |- U2=Uy+U2':cap~ and D |- Uy#A2<=A2'

D |- U1=Ux+U1':cap~    D |- U2=Uy+U2':cap~
------------------------------------------
D |- U1+U2=(Ux+U1')+(Uy+U2'):cap~
---------------------------------
D |- U1+U2=(Ux+Uy)+(U1'+U2'):cap~

D |- Ux#A1<=A1'    D |- Uy#A2<=A2'
----------------------------------
D |- Ux+Uy#A1+A2<=A1'+A2'


CASE:

d1,(A:cap+<=c),d2 |- A<=c ~~> {}
d = d1,(A:cap+<=c),d2

[d1]Aa = Aa
[d1]A(c) = [d]A(c) because freevars(c) are declared in d1

[d] = [d1,A:cap+<=c,d2] = [d1][Au<-{}][d2]
[d]A(A) = [d]Aa = Aa
[d]U(A) = [d]Au = {}

|- d1,(A:cap+<=c),d2 implies d1 |- c:cap+
By weakening, d |- c:cap+
By lemma, D(d) |- [d]U(c) = {}:cap~

Prove D(d) |- [d]U(A)=[d]{}+[d]U(c):cap~
  [d]U(A) = {}
  [d]{} = {}
  D(d) |- [d]U(c) = {}:cap~

Prove D(d) |- [d]{}#[d]A(A)<=[d]A(c)
  D(d) = D(d1,A:cap+<=c,d2)
       = ...,Aa:cap+ where {}#[d1]Aa<=[d1]A(c), ...
       = ...,Aa:cap+ where {}#Aa<=[d]A(c), ...
  ...,Aa:cap+ where {}#Aa<=[d]A(c), ... |- {}#Aa<=[d]A(c)


CASE:

...,(A:cap<=c0,...),... |- A<=c0 ~~> Ab
d = d1,(A:cap<=c0,...),d2

[d] = [d1,(A:cap<=c0,...),d2] = [d1][Au<-[d1]Ab+[d1]U(c0)][d1]

[d1]A(c0) = [d]A(c0) because freevars(c0) are declared in d1
[d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1

[d]Ab = Ab
[d]U(A) = [d]Au = [d1]Ab+[d1]U(c0) = Ab+[d]U(c0)
[d]A(A) = [d]Aa = Aa


Prove D(d) |- [d]U(A)=[d]Ab+[d]U(c0):cap~
      D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0):cap~

Prove D(d) |- [d]Ab#[d]A(A)<=[d]A(c0)
      D(d) |- Ab#Aa<=[d]A(c0)
  D(d) = D(d1,(A:cap<=c0,...),d2)
       = ...,Ab:cap~, (Aa:cap+ where [d1]Ab#Aa<=[d1]A(c0),...),...
       = ...,Ab:cap~, (Aa:cap+ where Ab#Aa<=[d]A(c0),...),...


CASE:

...,(A:cap<=c0,...,ck,...),... |- A<=ck ~~> Ab+U(c0)
d = d1,(A:cap<=c0,...,ck,...),d2

[d] = [d1,(A:cap<=c0,...,ck,...),d2] = [d1][Au<-[d1]Ab+[d1]U(c0)][d1]

[d1]A(c0) = [d]A(c0) because freevars(c0) are declared in d1
[d1]A(ck) = [d]A(ck) because freevars(ck) are declared in d1
[d1]U(c0) = [d]U(c0) because freevars(c0) are declared in d1
[d1]U(ck) = [d]U(ck) because freevars(ck) are declared in d1

[d]Ab = Ab
[d]U(A) = [d]Au = [d1]Ab+[d1]U(c0) = Ab+[d]U(c0)
[d]A(A) = [d]Aa = Aa

|- d1,(A:cap<=c0,...,ck,...),d2 implies d1 |- ck:cap+
By weakening, d |- ck:cap+
By lemma, D(d) |- [d]U(ck) = {}:cap~

Prove D(d) |- [d]U(A)=[d](Ab+U(c0))+[d]U(ck):cap~
      D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0)+[d]U(ck):cap~
      D(d) |- Ab+[d]U(c0)=Ab+[d]U(c0)+{}:cap~

Prove D(d) |- [d](Ab+U(c0))#[d]A(A)<=[d]A(ck)
      D(d) |- Ab+[d]U(c0)#Aa<=[d]A(ck)
  D(d) = D(d1,(A:cap<=c0,...,ck,...),d2)
       = ...,Ab:cap~, (Aa:cap+ where [d1]Ab#Aa<=[d1]A(c0),...,[d1](Ab+U(c0))#Aa<=[d1]A(ck),...),...
       = ...,Ab:cap~, (Aa:cap+ where Ab#Aa<=[d]A(c0),...,Ab+[d]U(c0)#Aa<=[d]A(ck),...),...


CASE:

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

[d]{A p} = {A p}

Prove D(d) |- [d]U({A~})=[d]{A~}+[d]U({A+}):cap~
      D(d) |- {A~}={A~}+{}:cap~

Prove D(d) |- [d]{A~}#[d]A({A~})<=[d]A({A+})
      D(d) |- {A~}#{}<={A+}

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

If |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]U(c1)=[d]U(c2):cap~

CASE:

d |- c:k
------------ k=cap or k=cap+
d |- c = c:k
  By lemma, D(d) |- [d]U(c):cap~


EASY CASES:

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

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

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

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

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

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

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


CASE:

d |- c:cap+
-----------------
d |- c = c+c:cap+
  By lemma, D(d) |- [d]U(c)={}:cap~


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

If |- d and d |- c1=c2:k and k=cap or k=cap+ then D(d) |- [d]A(c1)=[d]A(c2):cap+

CASE:

d |- c:k
------------ k=cap or k=cap+
d |- c = c:k
  By lemma, D(d) |- [d]A(c):cap+


EASY CASES:

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

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

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

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

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

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

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


CASE:

d |- c:cap+
-----------------
d |- c = c+c:cap+
  By lemma, D(d) |- [d]A(c):cap+

  D(d) |- [d]A(c):cap+
  --------------------------------------
  D(d) |- [d]A(c) = [d]A(c)+[d]A(c):cap+

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

If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then A([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]A(c)

CASE:

A(A') = Aa'

A([A'<-c']A') = A(c')
[Au'<-U(c'),Aa'<-A(c')]A(A') = [Au'<-U(c'),Aa'<-A(c')]Aa' = A(c')


CASE:

A(A) = Aa
A([A'<-c']A) = A(A) = Aa
[Au'<-U(c'),Aa'<-A(c')]A(A) = [Au'<-U(c'),Aa'<-A(c')]Aa = Aa
  (where Au'!=Aa and Aa'!=Aa because A'!=A)


CASE:

A({A'+}) = {A'+}
Impossible case: d |- A':k' and d |- A':res cannot both be true


EASY CASES:

A({}) = {}
A({A~}) = {}
A({A+}) = {A+}
A(c1+c2) = A(c1)+A(c2)

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

If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then U([A'<-c']c) = [Au'<-U(c'),Aa'<-A(c')]U(c)

CASES JUST LIKE LEMMA FOR A(c):

U(A') = Au'
U(A) = Au
U({}) = {}
U({A~}) = {A~}
U({A'~}) = {A'~}
U({A+}) = {}
U(c1+c2) = U(c1)+U(c2)

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

If |- d and d |- A':k' (k'=cap or k'=cap+) and d |- t:type then T([A'<-c']t) = [Au'<-U(c'),Aa'<-A(c')]T(t)


CASE:

T(A') = A'
Impossible case: d |- A':k' 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 Aa:cap+. all Au:cap~. T(t)
T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t)
T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t)
T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] 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:k (k=cap or k=cap+) then A([A'<-t']c) = [A'<-T(t')]A(c)
If |- d and d |- A':type and d |- c:k (k=cap or k=cap+) then U([A'<-t']c) = [A'<-T(t')]U(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 Aa:cap+. all Au:cap~. T(t)
T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t)
T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t)
T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] 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) |- [d]G(g)

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

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

If |- d and d |- g then:
  - if d;g |- v:t ~~> v' then D(d);[d]G(g) |- [d]v':[d]T(t)
  - if d;g |- h:t ~~> h' then D(d);[d]G(g) |- [d]h':[d]T(t)
  - if d;g;c |- l==>d';g';c' ~~> l' then D(d);[d]G(g);[d]C(c) |- [d']l'==>D(d');[d']G(g');[d']C(c')
  - if d;g;c |- e ~~> e' then D(d);[d]G(g);[d]C(c) |- [d]e'

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 ~~> h'
---------------------------- (A not in Dom(d))
d;g |- \A:cap.h: all A:cap.t ~~> \Aa:cap+.\Au:cap~.h'

T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t)

Induction: D(d,A:cap);[d,A:cap]G(g) |- [d,A:cap]h':[d,A:cap]T(t)
           D(d),Aa:cap+, Au:cap~;[d]G(g) |- [d]h':[d]T(t)
           ----------------------------------------------------------
           D(d),Aa:cap+;[d]G(g) |- \Au:cap~.[d]h':all Au:cap~.[d]T(t)
           -----------------------------------------------------------------------
           D(d);[d]G(g) |- \Aa:cap+.\Au:cap~.[d]h':all Aa:cap+.all Au:cap~.[d]T(t)
           D(d);[d]G(g) |- [d]\Aa:cap+.\Au:cap~.h':[d]all Aa:cap+.all Au:cap~.T(t)


CASE:

d,A:cap+;g |- h:t ~~> h'
----------------------------- (A not in Dom(d))
d;g |- \A:cap+.h: all A:cap.t ~~> \Aa:cap+.[Au<-{}]h'

T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t)

Induction: D(d,A:cap+);[d,A:cap+]G(g) |- [d,A:cap+]h':[d,A:cap+]T(t)
           D(d),Aa:cap+;[d][Au<-{}]G(g) |- [d][Au<-{}]h':[d][Au<-{}]T(t)
           --------------------------------------------------------------------------
           D(d);[d][Au<-{}]G(g) |- \Aa:cap+.[d][Au<-{}]h':all Aa:cap+.[d][Au<-{}]T(t)
           D(d);[d][Au<-{}]G(g) |- [d]\Aa:cap+.[Au<-{}]h':[d]all Aa:cap+.[Au<-{}]T(t)

[Au<-{}]G(g) = G(g) because d |- g implies A not in freevars(g)


CASE:

d |- all A:cap+<=c.t: type
d,A:cap+<=c;g |- h:t ~~> h'
---------------------------------------------- (A not in Dom(d))
d;g |- \A:cap+<=c.h: all A:cap+<=c.t ~~> \Aa:cap+ where {}#Aa<=A(c).[Au<-{}]h'

T(all A:cap+<=c.t) = all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t)

By lemma, D(d) |- [d]T(all A:cap+<=c.t): type
          D(d) |- [d]all Aa:cap+ where {}#Aa<=A(c). [Au<-{}] T(t):type

Induction: D(d,A:cap+<=c);[d,A:cap+<=c]G(g) |- [d,A:cap+<=c]h':[d,A:cap+<=c]T(t)
           D(d),Aa:cap+ where {}#Aa<=[d]A(c);[d][Au<-{}]G(g) |- [d][Au<-{}]h':[d][Au<-{}]T(t)
           --------------------------------------------------------------------------------------------------------------------
           D(d);[d][Au<-{}]G(g) |- \Aa:cap+ where {}#Aa<=[d]A(c).[d][Au<-{}]h':all Aa:cap+ where {}#Aa<=[d]A(c).[d][Au<-{}]T(t)
           D(d);[d][Au<-{}]G(g) |- [d]\Aa:cap+ where {}#Aa<=A(c).[Au<-{}]h':[d]all Aa:cap+ where {}#Aa<=A(c).[Au<-{}]T(t)

[Au<-{}]G(g) = G(g) because d |- g implies A not in freevars(g)


CASE:

d |- all A:cap<=c0,c1,...,cn.t: type
d,(A:cap<=c0,c1,...,cn);g |- h:t ~~> h'
------------------------------------------------------------ (A not in Dom(d))
d;g |- \A:cap<=c0,c1,...,cn.h: all A:cap<=c0,c1,...,cn.t ~~>
  \Ab:cap~. \Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]h'

T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t)

By lemma, D(d) |- [d]T(all A:cap<=c0,c1,...,cn.t): type
          D(d) |- [d]all Ab:cap~. all Aa:cap+
                     where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t):type
          D(d), [d]all Ab:cap~. |- [d]all Aa:cap+
                     where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t):type


Induction: D(d,(A:k<=c1,...,cn));[d,(A:k<=c1,...,cn)]G(g) |- [d,(A:k<=c1,...,cn)]h':[d,(A:k<=c1,...,cn)]T(t)
           D(d),Ab:cap~, Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn);
             [d][Au<-Ab+U(c0)]G(g) |- [d][Au<-Ab+U(c0)]h':[d][Au<-Ab+U(c0)]T(t)
           -------------------------------------------------------------------------------------------------
           D(d),Ab:cap~;[d][Au<-Ab+U(c0)]G(g) |-
             \Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]h':
             all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]T(t)
           ---------------------------------------------------------------------------------------------------------------
           D(d);[d][Au<-Ab+U(c0)]G(g) |-
             \Ab:cap~.\Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]h':
             all Ab:cap~.all Aa:cap+ where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,Ab+[d]U(c0)#Aa<=[d]A(cn).[d][Au<-Ab+U(c0)]T(t)
           D(d);[d][Au<-Ab+U(c0)]G(g) |-
             [d]\Ab:cap~.\Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]h':
             [d]all Ab:cap~.all Aa:cap+ where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn).[Au<-Ab+U(c0)]T(t)

[Au<-Ab+U(c0)]G(g) = G(g) because d |- g implies A not in freevars(g)


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) |- [d]T(t')=[d]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 ~~> v'
d;g |- c:cap+
-------------------------------------------
d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+]

By lemma, all A:cap+.t:type
T(all A:cap+.t) = all Aa:cap+. [Au<-{}]T(t)
By lemma, D(d) |- all Aa:cap+. [Au<-{}]T(t):type

By lemma, D(d) |- [d]A(c):cap+
By lemma, D(d) |- [d]U(c)={}:cap~
By lemma, D(d) |- [Au<-[d]U(c)][d]all Aa:cap+.T(t)
                      =[Au<-{}][d]all Aa:cap+.T(t):type

Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap+.t)
           D(d);[d]G(g) |- [d]v': all Aa:cap+. [d][Au<-{}]T(t)
           --------------------------------------------------------------------
           D(d);[d]G(g) |- [d]v': all Aa:cap+. [d][Au<-U(c)]T(t)
           ----------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)] [d][Au<-U(c)]T(t)
           D(d);[d]G(g) |- [d](v'[A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)]T(t)

[Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c))
By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t)


CASE:

d;g |- v: all A:cap.t ~~> v'
d;g |- c:cap
-----------------------------------------------------
d;g |- v[c:cap]: [A<-c]t ~~> v'[A(c):cap+][U(c):cap~]

By lemma, d |- all A:cap.t:type
T(all A:cap.t) = all Aa:cap+. all Au:cap~. T(t)

By lemma, D(d) |- [d]A(c):cap+
By lemma, D(d) |- [d]U(c):cap~

Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap.t)
           D(d);[d]G(g) |- [d]v': all Aa:cap+. all Au:cap~. [d]T(t)
           -----------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)]all Au:cap~. [d]T(t)
           --------------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+][[d]U(c):cap~]: [Au<-[d]U(c)][Aa<-[d]A(c)][d]T(t)
           D(d);[d]G(g) |- [d](v'[A(c):cap+][U(c):cap~]): [d][Au<-U(c)][Aa<-A(c)]T(t)

[Au<-U(c)][Aa<-A(c)] = [Au<-U(c),Aa<-A(c)] because Au not in freevars(A(c))
By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t)


CASE:

d;g |- v: all A:cap+<=c0.t ~~> v'
d;g |- c <= c0 ~~> u
d;g |- c:cap+
-------------------------------------------
d;g |- v[c:cap+]: [A<-c]t ~~> v'[A(c):cap+]

By lemma, d |- all A:cap+<=c0.t:type
By inversion, d |- c0:cap+
By lemma, D(d) |- [d]U(c0)={}:cap~

T(all A:cap+<=c0.t) = all Aa:cap+ where {}#Aa<=A(c0). [Au<-{}] T(t)
By lemma, D(d) |- [d]all Aa:cap+ where {}#Aa<=A(c0). [Au<-{}] T(t):type

By lemma, D(d) |- [d]A(c):cap+
By lemma, D(d) |- [d]U(c)={}:cap~
By lemma, D(d) |- all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-[d]U(c)] [d]T(t):type
                = all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-{}] [d]T(t):type

By lemma, D(d) |- [d]U(c)#[d]A(c)<=[d]A(c0)

Induction: D(d);[d]G(g) |- [d]v':[d]T(all A:cap+<=c0.t)
           D(d);[d]G(g) |- [d]v':all Aa:cap+ where {}#Aa<=[d]A(c0). [Au<-{}] [d]T(t)
           -----------------------------------------------------------------------------------
           D(d);[d]G(g) |- [d]v':all Aa:cap+ where [d]U(c)#Aa<=[d]A(c0). [Au<-[d]U(c)] [d]T(t)
           -----------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]A(c):cap+]: [Aa<-[d]A(c)][Au<-[d]U(c)] [d]T(t)
           D(d);[d]G(g) |- [d](v'[A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)] T(t)

[Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c))
By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t)


CASE:

d;g |- v: all A:cap<=c0,...,cn.t ~~> v'
d;g |- c <= c0 ~~> ub
d;g |- c <= c1 ... d;g |- c <= cn
d;g |- c:cap
---------------------------------------------------
d;g |- v[c:cap]: [A<-c]t ~~> v'[ub:cap~][A(c):cap+]

By lemma, d |- all A:cap<=c0,...,cn.t:type
By inversion, d |- ck:cap+ for 1<=k<=n

T(all A:cap<=c0,c1,...,cn.t) = all Ab:cap~. all Aa:cap+
  where Ab#Aa<=A(c0),Ab+U(c0)#Aa<=A(c1),...,Ab+U(c0)#Aa<=A(cn). [Au<-Ab+U(c0)] T(t)

By lemma, D(d) |- [d]ub:cap~
By lemma, D(d) |- [d]A(c):cap+
By lemma, D(d) |- [d]U(c)=[d]ub+[d]U(c0):cap~
      and D(d) |- [d]ub#[d]A(c)<=[d]A(c0)
By lemma, D(d) |- [d]U(c)#[d]A(c)<=A(ck) for 1<=k<=n

By lemma, D(d) |- [Au<-[d]ub+[d]U(c0)][d][Aa<-A(c)][Ab<-ub] T(t)
                =           [Au<-U(c)][d][Aa<-A(c)][Ab<-ub] T(t)

Induction: D(d);[d]G(g) |- [d]v': [d]T(all A:cap<=c0,...,cn.t)
           D(d);[d]G(g) |- [d]v': all Ab:cap~. all Aa:cap+
             where Ab#Aa<=[d]A(c0),Ab+[d]U(c0)#Aa<=[d]A(c1),...,
                                   Ab+[d]U(c0)#Aa<=[d]A(cn). [d][Au<-Ab+U(c0)] T(t)
           ------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]ub:cap~]: all Aa:cap+
             where [d]ub#Aa<=[d]A(c0),[d]ub+[d]U(c0)#Aa<=[d]A(c1),...,
                                      [d]ub+[d]U(c0)#Aa<=[d]A(cn). [d][Au<-ub+U(c0)][Ab<-ub]T(t)
           -------------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]ub:cap~]: all Aa:cap+
             where [d]ub#Aa<=[d]A(c0),[d]U(c)#Aa<=[d]A(c1),...,
                                      [d]U(c)#Aa<=[d]A(cn). [d][Au<-ub+U(c0)][Ab<-ub]T(t)
           -------------------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]ub:cap~][[d]A(c):cap+]: [d][Aa<-A(c)][Au<-ub+U(c0)][Ab<-ub] T(t)
           -------------------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]v')[[d]ub:cap~][[d]A(c):cap+]: [d][Aa<-A(c)][Au<-U(c)][Ab<-ub] T(t)
           D(d);[d]G(g) |- [d](v'[ub:cap~][A(c):cap+]): [d][Aa<-A(c)][Au<-U(c)][Ab<-ub] T(t)


[Aa<-A(c)][Au<-U(c)] = [Au<-U(c),Aa<-A(c)] because Aa not in freevars(U(c))
[Ab<-ub]T(t) = T(t) because Ab not in freevars(T(t))
By lemma, T([A<-c]t) = [Au<-U(c),Aa<-A(c)]T(t)


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~}
[d,A:res] = [d]


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+}


CASE:

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

Induction: D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d);[d]G(g');[d]C(c') and [d]=[d']
Induction: D(d');[d']G(g');[d']C(c') |- [d']e'

  D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c')
  D(d');[d]G(g');[d]C(c') |- [d]e'
  ------------------------------------------
  D(d);[d]G(g);[d]C(c) |- let [d]l' in [d]e'


CASE:

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

Induction: D(d);[d]G(g) |- [d]v1': [d]T((c',t)->0)
Induction: D(d);[d]G(g) |- [d]v2': [d]T(t)
By lemma: D(d) |- [d]U(c)=[d]u+[d]U(c'):cap~ and D(d) |- [d]u#[d]A(c)<=[d]A(c')

  D(d);[d]G(g) |- [d]v1': ([d]U(c')#[d]A(c'),[d]T(t))->0
  D(d);[d]G(g) |- [d]v2': [d]T(t)
  D(d) |- [d]U(c)=[d]u+[d]U(c'):cap~
  D(d) |- [d]u#[d]A(c)<=[d]A(c')
  --------------------------------------------
  D(d);[d]G(g);[d]U(c)#[d]A(c) |- v1' v2'


EASY CASE:

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

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