=================================================
================== LANG3a =======================
=================================================

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

k = type | res | cap
b = A | t | c
t = A | A handle | all A:k.t | (c,t)->0 | <t1,t2>
c = A | {} | {A} | c1*c2 | c1&c2 | c1 -o c2 | true

o = c1,...,cn (unordered list)
d = . | d,A:k
g = . | g,x:t

v = x | v[b:k]
h = \A:k.h | \(c,x:t).e | <v1,v2>
l = x=v | x=h | x=v.n | new A,x | free v | use v
e = let l in e | v1 v2 | halt

define o1,o2 = o3 if each c in o3 appears in either o1 or o2.

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

from lang0:
  keep ...,A:k,... |- A:k
  keep d |- A handle:type
  keep d |- <t1,t2>:type
  keep d |- all A:k.t:type
  keep d |- (c,t)->0:type
  keep d |- {}:cap

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

d |- c1:cap
d |- c2:cap
--------------
d |- c1*c2:cap

d |- c1:cap
d |- c2:cap
--------------
d |- c1&c2:cap

d |- c1:cap
d |- c2:cap
-----------------
d |- c1 -o c2:cap

d |- true:cap

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

c |- c

|- {}

o |- c
---------
o,{} |- c

o1 |- c1
o2 |- c2
--------------
o1,o2 |- c1*c2

o,c1,c2 |- c3
-------------
o,c1*c2 |- c3

o |- c1
o |- c2
----------
o |- c1&c2

o,c1 |- c3
-------------
o,c1&c2 |- c3

o,c2 |- c3
-------------
o,c1&c2 |- c3

o,c1 |- c2
-------------
o |- c1 -o c2

o1 |- c1
o2,c2 |- c3
--------------------
o1,o2,c1 -o c2 |- c3

o |- true

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

from lang0:
  keep d |- b = b:k
  keep d |- b1 = b2:k
  keep d |- b1 = b3:k

d |- c1:k
d |- c2:k
c1 |- c2
c2 |- c1
--------------
d |- c1 = c2:k

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

from lang0:
  keep d |- <t1,t2> = <t1',t2'>:type
  keep d |- all A:k.t = all A:k.t':type
  keep d |- (c,t)->0 = (c',t')->0:type

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

from lang0:
  keep d;g |- \A:k.h: all A:k.t
  keep d;g |- \(c,x:t).e: (c,t)->0
  keep d;g |- <v1,v2>: <t1,t2>
  keep d;g |- h: t

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

from lang0:
  keep d;...,x:t,... |- x: t
  keep d;g |- v[b:k]: [A<-b]t
  keep d;g |- v: t

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

from lang0:
  keep d;g;c |- x=v ==> d;g,x:t;c
  keep d;g;c |- x=h ==> d;g,x:t;c
  keep d;g;c |- x=v.n ==> d;g,x:t_n;c

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

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

d;g |- v: A handle
c |- {A}*true
------------------------
d;g;c |- use v ==> d;g;c

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

from lang0:
  keep d;g;c |- let l in e

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

d;g;c |- halt

=================================================
========== LANG2->LANG3a TRANSLATION ============
=================================================

K(type) = type
K(res) = res
K(cap p) = cap

T(A) = A
T(A handle) = A handle
T(all A:k.t) = all A:K(k).T(t)
T(all A:cap+ where u1#A<=a1,...,un#A<=an.t) = all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>

C(u#a) = U(u)*(A(a)*true)

U(A) = A
U({}) = {}
U({A p}) = {A}
U(u1+u2) = U(u1)*U(u2)

A(A) = A
A({}) = {}
A({A p}) = {A}
A(a1+a2) = (A(a1)*true) & (A(a2)*true)

D(.) = .
D(A:k,d) = A:K(k), D(d)
D(A:cap+ where u1#A<=a1,...,un#A<=an,d) = A:cap, [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]D(d)

[.] = []
[A:k,d] = [d]
[A:cap+ where u1#A<=a1,...,un#A<=an,d] = [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))][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[u:cap~]) = V(v)[U(u):cap]
V(v[a:cap+]) = V(v)[A(a):cap]

H(\A:k.h) = \A:K(k).H(h)
H(\A:cap+ where u1#A<=a1,...,un#A<=an.h) = \A:cap.[A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]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 o1 |- c2 and o2,c2 |- c3 then o1,o2 |- c3
    (corollary: if |- c2 and o2,c2 |- c3 then o2 |- c3)
    (corollary: if c1 |- c2 and o2, c1 -o c2 |- c3 then o2 |- c3)
  - 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 |- u:cap~ then D(d) |- [d]U(u):cap
 -- if |- d and d |- a:cap+ then D(d) |- [d]A(a):cap
 -- if |- d and d |- t:type then D(d) |- [d]T(t):type
 -- if |- d and d |- u1=u2:cap~ then D(d) |- [d]U(u1)=[d]U(u2):cap
 -- if |- d and d |- a1=a2:cap+ then D(d) |- [d]A(a1)*true=[d]A(a2)*true:cap
 -- if |- d and d |- c<=a then [d]C(c) |- [d]A(a)*true
 -- if |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type
 -- if |- d and d |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A(a')]A(a)
 -- if |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'']U(u) for any a''
 -- if |- d and d |- A':cap~ and d |- a:cap+ then A([A'<-u']a) = [A'<-u'']A(a) for any u''
 -- if |- d and d |- A':cap~ and d |- u:cap~ then U([A'<-u']u) = [A'<-U(u')]U(u)
 -- if |- d and d |- A':cap+ and d |- t:type then T([A'<-a']t) = [A'<-A(a')]T(t)
 -- if |- d and d |- A':cap~ and d |- t:type then T([A'<-u']t) = [A'<-U(u')]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:
    - if d;g |- v:t then D(d);[d]G(g) |- [d]V(v):[d]T(t)
    - if d;g |- h:t then D(d);[d]G(g) |- [d]H(h):[d]T(t)
    - if d;g;c |- l==>d';g';c' then D(d);[d]G(g);[d]C(c) |- [d]L(l)==>D(d');[d]G(g');[d]C(c') and [d]=[d']
    - if d;g;c |- e then D(d);[d]G(g);[d]C(c) |- [d]E(e)

Some basic properties of the logic:

c |- c

If c1 |- c2 and c2 |- c3 then c1 |- c3 (follows from cut)

If c1 |- c1' and c2 |- c2' then:

  c1 |- c1'    c2 |- c2'
  ----------------------
  c1,c2 |- c1'*c2'
  ----------------
  c1*c2 |- c1'*c2'

  c1 |- c1'       c2 |- c2'
  ------------    ------------
  c1&c2 |- c1'    c1&c2 |- c2'
  ----------------------------
  c1&c2 |- c1'&c2'


c1,c2 |- c2*c1
--------------
c1*c2 |- c2*c1

   c2 |- c2       c1 |- c1
-----------    -----------
c1&c2 |- c2    c1&c2 |- c1
--------------------------
c1&c2 |- c2&c1

c1 |- c1    c2,c3 |- c2*c3
--------------------------
c1,c2,c3 |- c1*(c2*c3)
------------------------
(c1*c2)*c3 |- c1*(c2*c3)


                    c1&c2 |- c2         c3 |- c3
                    ----------------    ----------------
c1&c2 |- c1         (c1&c2)&c3 |- c2    (c1&c2)&c3 |- c3
----------------    ------------------------------------
(c1&c2)&c3 |- c1    (c1&c2)&c3 |- c2&c3
--------------------------------------
(c1&c2)&c3 |- c1&(c2&c3)

(similar proofs for:
  c1*(c2*c3) |- (c1*c2)*c3
  c1&(c2&c3) |- (c1&c2)&c3
)

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

If |- d and d |- a:cap+ then D(d) |- [d]A(a):cap

By induction on d, then by induction on derivation of d |- a:cap+

CASE:

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

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


CASE:

...,(A:cap+ where u1#A<=a1,...,un#A<=an),... |- A:cap+
d = d1,(A:cap+ where u1#A<=a1,...,un#A<=an),d2

|- d implies:
  d1 |- u1:cap~ ... d1 |- un:cap~
  d1 |- a1:cap+ ... d1 |- an:cap+
By lemma:
  D(d1) |- [d1]U(u1):cap ... D(d1) |- [d1]U(un):cap
By induction:
  D(d1) |- [d1]A(a1):cap ... D(d1) |- [d1]A(an):cap
By weakening:
  D(d) |- [d1]U(u1):cap ... D(d) |- [d1]U(un):cap
  D(d) |- [d1]A(a1):cap ... D(d) |- [d1]A(an):cap

[d1,A:cap+ where u1#A<=a1,...,un#A<=an,d2]A(A) = A&([d1]U(u1) -o [d1]A(a1)*true)&...&([d1]U(un) -o [d1]A(an)*true)
D(d1,A:cap+ where u1#A<=a1,...,un#A<=an,d2) = ..., A:cap, ...


EASY CASES:

d |- {}:cap+

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

d |- a1:cap+
d |- a2:cap+
---------------
d |- a1+a2:cap+

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

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

CASE:

d1,A:type,d2 |- A:type

[d1,A:type,d2]T(A) = [d1][d2]A = A
D(d1,A:type,d2) = ...,A:type,...


EASY CASES:

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

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

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


CASE:

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,A:cap+ where u1#A<=a1,...,un#A<=an
Induction: D(d,A:cap+ where u1#A<=a1,...,un#A<=an) |- [d,A:cap+ where u1#A<=a1,...,un#A<=an]T(t):type
           D(d),A:cap |- [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t):type
           ---------------------------------------------------------------------------------------
           D(d) |- all A:cap. [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t):type
           D(d) |- [d]all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t):type


EASY CASE:

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


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

If |- d and d |- u1=u2:cap~ then D(d) |- [d]U(u1)=[d]U(u2):cap

Abbreviations: U1 = [d]U(u1), A1 = [d]A(a1), etc.

CASE:

d |- u:k
------------ where k = cap~
d |- u = u:k

by c |- c rule


CASE:

d |- u2 = u1:k
-------------- where k = cap~
d |- u1 = u2:k

by definition of =


CASE:

d |- u1 = u2:k
d |- u2 = u3:k
-------------- where k = cap~
d |- u1 = u3:k

follows from transitivity of |-


CASE:

d |- u1 = u1':k
d |- u2 = u2':k
---------------------- where k = cap~
d |- u1+u2 = u1'+u2':k

follows from congruence of *


CASE:

d |- u1:k
----------------- where k = cap~
d |- {}+u1 = u1:k

U1 |- U1
-----------
{},U1 |- U1
-----------
{}*U1 |- U1

|- {}    U1 |- U1
-----------------
U1 |- {}*U1


CASE:

d |- u1:k
d |- u2:k
-------------------- where k = cap~
d |- u1+u2 = u2+u1:k

by commutivity of *


CASE:

d |- u1:k
d |- u2:k
d |- u3:k
------------------------------ where k = cap~
d |- (u1+u2)+u3 = u1+(u2+u3):k

by associativity of *

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

If |- d and d |- a1=a2:cap+ then D(d) |- [d]A(a1)*true=[d]A(a2)*true:cap

Abbreviations: U1 = [d]U(u1), A1 = [d]A(a1), etc.

CASE:

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

by c |- c rule


CASE:

d |- a2 = a1:k
-------------- where k = cap+
d |- a1 = a2:k

by definition of =


CASE:

d |- a1 = a2:k
d |- a2 = a3:k
-------------- where k = cap+
d |- a1 = a3:k

follows from transitivity of |-


CASE:

d |- a1 = a1':k
d |- a2 = a2':k
---------------------- where k = cap+
d |- a1+a2 = a1'+a2':k

A1*true |- A1'*true
A2*true |- A2'*true

A1*true&A2*true |- A1'*true&A2'*true
--------------------------------------------------
(A1*true&A2*true)*true |- (A1'*true&A2'*true)*true



CASE:

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

|- {}    A1*true |- true
-----    ---------------
A1*true |- {}*true      A1*true |- A1*true
------------------      ------------------
A1*true |- ({}*true)&(A1*true)
-------------------------------------
A1*true |- (({}*true)&(A1*true))*true

true,true |- true
-----------------------
A1,true,true |- A1*true
-----------------------
A1*true,true |- A1*true
-----------------------------------
({}*true)&(A1*true),true |- A1*true
-------------------------------------
(({}*true)&(A1*true))*true |- A1*true


CASE:

d |- a1:k
d |- a2:k
-------------------- where k = cap+
d |- a1+a2 = a2+a1:k

...by commutivity of &...
----------------------------------
A1*true&A2*true |- A2*true&A1*true
------------------------------------------------
(A1*true&A2*true)*true |- (A2*true&A1*true)*true


CASE:

d |- a1:k
d |- a2:k
d |- a3:k
------------------------------ where k = cap+
d |- (a1+a2)+a3 = a1+(a2+a3):k

A2*true,true |- A2*true
-------------------------------
A1*true&A2*true,true |- A2*true
---------------------------------
(A1*true&A2*true)*true |- A2*true
-----------------------------------------
(A1*true&A2*true)*true&A3*true |- A2*true    A3*true |- A3*true
---------------------------------------------------------------
(A1*true&A2*true)*true&A3*true |- A2*true&A3*true
--------------------------------------------------------
(A1*true&A2*true)*true&A3*true |- (A2*true&A3*true)*true
--------------------------------------------------------(1)

A1*true,true |- A1*true
-------------------------------
A1*true&A2*true,true |- A1*true
---------------------------------
(A1*true&A2*true)*true |- A1*true
---------------------------------    ---------------------------(1)
(A1*true&A2*true)*true&A3*true |- A1*true&(A2*true&A3*true)*true
------------------------------------------------------------------------------
((A1*true&A2*true)*true&A3*true)*true |- (A1*true&(A2*true&A3*true)*true)*true


CASE:

d |- a1:cap+
--------------------
d |- a1 = a1+a1:cap+

A1*true |- A1*true&A1*true    |- true
-------------------------------------
A1*true |- (A1*true&A1*true)*true

A1*true,true |- A1*true
-------------------------------
A1*true&A1*true,true |- A1*true
---------------------------------
(A1*true&A1*true)*true |- A1*true

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

If |- d and d |- c<=a then [d]C(c) |- [d]A(a)*true

Abbreviations: U1 = [d]U(u1), A1 = [d]A(a1), etc.

/*
CASE:

d = ...,(A:cap+ where ...,u1#A<=a2,...),...
d |- u1#A<=a2

[d] = [..., A<-(A&...&(U1 -o A2)&...), ...]
[d]C(u1#A) = U1*((A&...&(U1 -o A2)&...)*true)
[d]A(a2) = A2

A2,true |- A2*true
------------------(1)

U1 |- U1
--------    -----------------(1)
U1,(U1 -o A2),true |- A2*true
-----------------------------------------
U1,(A&...&(U1 -o A2)&...),true |- A2*true
-------------------------------------------
U1*((A&...&(U1 -o A2)&...)*true) |- A2*true
*/

CASE:

d = ...,(A:cap+ where ...,u1#A<=a2,...),...
d |- u1#A<=a2

[d] = [..., A<-(A&...&(U1 -o A2*true)&...), ...]
[d]C(u1#A) = U1*((A&...&(U1 -o A2*true)&...)*true)
[d]A(a2) = A2

true,true |- true
-----------------------
A2,true,true |- A2*true
-----------------------
A2*true,true |- A2*true
-----------------------(1)

U1 |- U1
--------    ----------------------(1)
U1,(U1 -o A2*true),true |- A2*true
----------------------------------------------
U1,(A&...&(U1 -o A2*true)&...),true |- A2*true
------------------------------------------------
U1*((A&...&(U1 -o A2*true)&...)*true) |- A2*true


CASE:

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

A,true |- A*true
-------------------
A,{},true |- A*true
---------------------
A*({}*true) |- A*true


CASE:

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

By lemma, A1*true |- A2*true and A2*true |- A1*true

A1,true |- A1*true    A2*true |- A2*true
------------------    ------------------
A1*true -o A2*true, A1,true |- A2*true
-------------------------------------- cut
A1,true |- A2*true
---------------------
{},A1,true |- A2*true
-----------------------
{}*(A1*true) |- A2*true


CASE:

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

induction: U1*(A1*true) |- A2*true
induction: U2*(A2*true) |- A3*true

A3*true |- A3*true
------------------(2)

U2,A2,true |- U2*(A2*true)
--------------------------     --------------(2)
U2,A2,true,U2*(A2*true) -o A3*true |- A3*true
--------------------------------------------- cut
U2,A2,true |- A3*true
--------------------------
U2,A2*true |- A3*true
--------------------------(1)

U1,A1,true |- U1*(A1*true)
--------------------------     ------------------(1)
U1,U2,A1,true, U1*(A1*true) -o A2*true |- A3*true
------------------------------------------------- cut
U1,U2,A1,true |- A3*true
---------------------------------
(U1*U2)*(A1*true) |- A3*true


CASE:

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

induction: U1*(A1*true) |- A1'*true
induction: U2*(A2*true) |- A2'*true

...see proof of (1) below...
-------------------------------------
U1,U2,(A1*true)&(A2*true) |- A2'*true
-------------------------------------(2)

A1' |- A1'    U2,true |- true
----------    ---------------
U2,A1',true |- A1'*true
-----------------------
U2,A1'*true |- A1'*true
-----------------------(1')

U1,A1*true |- U1*(A1*true)
--------------------------    ---------------------(1')
U1,U2,A1*true, U1*(A1*true) -o A1'*true |- A1'*true
--------------------------------------------------- cut
U1,U2,A1*true |- A1'*true
-------------------------------------
U1,U2,(A1*true)&(A2*true) |- A1'*true
-------------------------------------(1)

-------------------(1)    ------------------------(2)
U1,U2,(A1*true)&(A2*true) |- (A1'*true)&(A2'*true)
--------------------------------------------------------------
U1,U2,(A1*true)&(A2*true),true |- ((A1'*true)&(A2'*true))*true
--------------------------------------------------------------------
(U1*U2)*(((A1*true)&(A2*true))*true) |- ((A1'*true)&(A2'*true))*true


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

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

|- d,A:cap+ where u1#A<=a1,...,un#A<=an
Induction: D(d,A:cap+ where u1#A<=a1,...,un#A<=an)
                |- [d,A:cap+ where u1#A<=a1,...,un#A<=an]T(t)
                 = [d,A:cap+ where u1#A<=a1,...,un#A<=an]T(t'):type
           D(d),A:cap
                |- [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
                 = [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]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 |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A(a')]A(a)
If |- d and d |- A':cap~ and d |- a:cap+ then A([A'<-u']a) = [A'<-u'']A(a) for any u''


CASE:

d |- A':cap+
A(A') = A'

A([A'<-a']A') = A(a')
[A'<-A(a')]A(A') = [A'<-A(a')]A' = A(a')


CASE:

d |- A':cap~
A(A') = A'

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


EASY CASES:

A(A) = A
A({}) = {}
A({A p}) = {A}
A({A' p}) = {A'}
A(a1+a2) = (A(a1)*true) & (A(a2)*true)


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

If |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'']U(u) for any a''
If |- d and d |- A':cap~ and d |- u:cap~ then U([A'<-u']u) = [A'<-U(u')]U(u)


CASE:

d |- A':cap~
U(A') = A'

U([A'<-u']A') = U(u')
[A'<-U(u')]U(A') = [A'<-U(u')]A' = U(u')


CASE:

d |- A':cap+
U(A') = A'

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


EASY CASES:

U(A) = A
U({}) = {}
U({A p}) = {A}
U({A' p}) = {A'}
U(u1+u2) = U(u1)*U(u2)

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

If |- d and d |- A':cap+ and d |- t:type then T([A'<-a']t) = [A'<-A(a')]T(t)
If |- d and d |- A':cap~ and d |- t:type then T([A'<-u']t) = [A'<-U(u')]T(t)

CASE:

T(A') = A'
Impossible case: d |- A':cap p 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:k.t) = all A:K(k).T(t)


CASE:

T(all A:cap+ where u1#A<=a1,....t) = all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...]T(t)
(if d |- A':cap+):
T([A'<-a']t) = T(all A:cap+ where [A'<-a']u1#A<=[A'<-a']a1,....[A'<-a']t)
             = all A:cap. [A<-(A&(U([A'<-a']u1) -o A([A'<-a']a1)*true)&...]T([A'<-a']t)
             = all A:cap. [A<-(A&([A'<-A(a')]U(u1) -o [A'<-A(a')]A(a1)*true)&...][A'<-A(a')]T(t)
             = [A'<-A(a')]all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...]T(t)
(if d |- A':cap~):
T([A'<-u']t) = T(all A:cap+ where [A'<-u']u1#A<=[A'<-u']a1,....[A'<-u']t)
             = all A:cap. [A<-(A&(U([A'<-u']u1) -o A([A'<-u']a1)*true)&...]T([A'<-u']t)
             = all A:cap. [A<-(A&([A'<-U(u')]U(u1) -o [A'<-U(u')]A(a1)*true)&...][A'<-U(u')]T(t)
             = [A'<-U(u')]all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...]T(t)


EASY CASES:

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 CASES:

T(A) = A
T(A handle) = A handle
T(all A:k.t) = all A:K(k).T(t)
T(all A:cap+ where u1#A<=a1,...,un#A<=an.t) = all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
T((c,t)->0) = (C(c),T(t))->0
T(<t1,t2>) = <T(t1),T(t2)>

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

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


EASY CASE:

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


CASE:

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

d'' = (A:cap+ where u1#A<=a1,...,un#A<=an)
d' = d,d''
D(d') = D(d),A:cap
[d'] = [d][d''] = [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]
T(all A:cap+ where u1#A<=a1,...,un#A<=an.t) = all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
H(\A:cap+ where u1#A<=a1,...,un#A<=an.h) = \A:cap.[A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]H(h)

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

d |- g implies that A not in freevars(g), so [d']G(g)=[d]G(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

Induction: D(d);[d]G(g) |- [d]H(h): [d]T(t')
By lemma: D(d) |- [d]T(t') = [d]T(t):type


CASE:

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

[d]G(...,x:t,...) = [d](...,x:T(t),...)


CASE:

d;g |- v: all A':k.t'
d |- b:k
-----------------------
d;g |- v[b:k]: [A'<-b]t'

By lemma: d |- all A':k.t':type

T(all A':k.t') = all A':K(k).T(t')
V(v[t:type]) = V(v)[T(t):type] = V(v)[B(b):K(k)]
V(v[A:res]) = V(v)[A:res] = V(v)[B(b):K(k)]
V(v[u:cap~]) = V(v)[U(u):cap] = V(v)[B(b):K(k)]
V(v[a:cap+]) = V(v)[A(a):cap] = V(v)[B(b):K(k)]

By lemma:
 d |- u:cap~ implies D(d) |- [d]U(u):cap
 d |- a:cap+ implies D(d) |- [d]A(a):cap
 d |- t:type implies D(d) |- [d]T(t):type

Induction: D(d);[d]G(g) |- [d]V(v): [d]T(all A':k.t')
           D(d);[d]G(g) |- [d]V(v): all A':K(k).[d]T(t')
           --------------------------------------------------------
           D(d);[d]G(g) |- ([d]V(v))[[d]B(b):K(k)]: [A'<-[d]B(b)][d]T(t')
           D(d);[d]G(g) |- [d](V(v)[B(b):K(k)]): [d][A'<-B(b)]T(t')

By lemma, T([A'<-b]t') = [A'<-B(b)]T(t')


CASE:

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

T(all A:cap+ where u1#A<=a1,...,un#A<=an.t) = all A:cap. [A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
V(v[a:cap+]) = V(v)[A(a):cap]

By lemma: D(d) |- [d]A(a):cap

Induction: D(d);[d]G(g) |- [d]V(v): [d]T(all A:cap+ where u1#A<=a1,...,un#A<=an.t)
           D(d);[d]G(g) |- [d]V(v): all A:cap. [d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
           ---------------------------------------------------------------------------------------------------
           D(d);[d]G(g) |- ([d]V(v))[[d]A(a):cap]:
             [A<-[d]A(a)][d][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
           D(d);[d]G(g) |- [d](V(v)[A(a):cap]):
             [d][A<-A(a)][A<-(A&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
           D(d);[d]G(g) |- [d](V(v)[A(a):cap]):
             [d][A<-(A(a)&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)

for 1<=k<=n:
  d |- uk#a <= ak
  By lemma: [d]C(uk#a) |- [d]A(ak)*true
            [d]U(uk)*([d]A(a)*true) |- [d]A(ak)*true

  Abbreviate Uk = [d]U(uk), Aa = [d]A(a), Ak = [d]A(ak)

    Uk |- Uk    Aa |- Aa*true
    -------------------------
    Aa,Uk |- Uk*(Aa*true)        Uk*(Aa*true) |- Ak*true
    ---------------------------------------------------- cut
    Aa,Uk |- Ak*true
    -------------------
    Aa |- Uk -o Ak*true

  So [d]A(a) |- [d](U(uk) -o A(ak)*true)
From this, we conclude:
  [d]A(a) |- [d]A(a) & [d](U(u1) -o A(a1)*true) & ... & [d](U(un) -o A(an)*true)
It's trivial to show:
  [d]A(a) & [d](U(u1) -o A(a1)*true) & ... & [d](U(un) -o A(an)*true) |- [d]A(a)
Therefore:
  D(d) |- [d]A(a) = [d]A(a) & [d](U(u1) -o A(a1)*true) & ... & [d](U(un) -o A(an)*true):cap
By lemma, D(d) |- [A<-[d]A(a)][d]T(t) = [A<-[d](A(a)&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))][d]T(t)

           D(d);[d]G(g) |- [d](V(v)[A(a):cap]):
             [d][A<-(A(a)&(U(u1) -o A(a1)*true)&...&(U(un) -o A(an)*true))]T(t)
           --------------------------------------------------------------------
           D(d);[d]G(g) |- [d](V(v)[A(a):cap]):
             [d][A<-A(a)]T(t)

By lemma, T([A<-a]t) = [A<-A(a)]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;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' = d,A:res
[d']=[d]
D(d,A:res) = D(d),A:res
G(g,x:A handle) = G(g),x:A handle
L(new A,x) = new A,x
C(u#a) = U(u)*(A(a)*true)
C(u+{A~}#a) = (U(u)*{A})*(A(a)*true)

[d](U(u)*(A(a)*true))*{A} |- [d]((U(u)*{A})*(A(a)*true))

D(d);[d]G(g);[d]C(u#a) |- [d]L(new A,x) ==> D(d');[d]G(g,x:A handle);[d]C(u+{A~}#a)


CASE:

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

|- d implies [d]A = A

C(u#a) = U(u)*(A(a)*true)
C(u'#a) = U(u')*(A(a)*true)
By lemma, D(d) |- [d]U(u)=[d]U(u'+{A~}):cap
          D(d) |- [d]U(u)=[d]U(u')*{A}:cap

Induction: D(d);[d]G(g) |- [d]V(v): [d]A handle
           D(d);[d]G(g) |- [d]V(v): A handle
           [d](U(u)*(A(a)*true)) |- [d]((U(u')*(A(a)*true))*{A})
           ------------------------------------------------------------
           D(d);[d]G(g);C(u#a) |- free [d]V(v) ==> D(d);[d]G(g);C(u'#a)


CASE:

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

|- d implies [d]A = A

C(u#a) = U(u)*(A(a)*true)
By lemma, D(d) |- [d]U(u)=[d]U(u1+u2):cap
          D(d) |- [d]U(u)=[d]U(u1)*[d]U(u2):cap
          [d]U(u) |- [d]U(u1)*[d]U(u2)
By lemma, [d]C(u1#a) |- [d]A(a'+{A+})*true
          [d]U(u1)*([d]A(a)*true) |- (([d]A(a')*true) & ({A}*true))*true
Abbreviate Uu=[d]U(u), U1=[d]U(u1), U2=[d]U(u2), Aa=[d]A(a), Aa'=[d]A(a')

                                               {A},true,true,U2 |- {A}*true
                                               ----------------------------
                                               {A}*true,true,U2 |- {A}*true
                                               -----------------------------------------
                                               (Aa'*true & {A}*true),true,U2 |- {A}*true
                                               -----------------------------------------
U1*(Aa*true) |- (Aa'*true & {A}*true)*true     (Aa'*true & {A}*true)*true,U2 |- {A}*true
                          -------------------------------------------------------------- cut
U1,Aa*true |- U1*(Aa*true)    U1*(Aa*true),U2 |- {A}*true
--------------------------------------------------------- cut
               U1,U2,Aa*true |- {A}*true
               -------------------------
Uu |- U1*U2    U1*U2,Aa*true |- {A}*true    
---------------------------------------- cut
Uu,(Aa*true) |- {A}*true
------------------------
Uu*(Aa*true) |- {A}*true

Induction: D(d);[d]G(g) |- [d]V(v): [d]A handle
           D(d);[d]G(g) |- [d]V(v): A handle
           [d]U(u)*([d]A(a)*true) |- {A}*true
           ----------------------------------------------------------------
           D(d);[d]G(g);[d]C(u#a) |- use [d]V(v) ==> D(d);[d]G(g);[d]C(u#a)


EASY CASE:

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


CASE:

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

E(v1 v2) = V(v1) V(v2)

Induction: D(d);[d]G(g) |- [d]V(v1): [d]T((u'#a',t)->0)
           D(d);[d]G(g) |- [d]V(v1): ([d]U(u')*([d]A(a')*true),[d]T(t))->0
Induction: D(d);[d]G(g) |- [d]V(v2): [d]T(t)

By lemma: D(d) |- [d]U(u) = [d]U(ub+u'):cap
          D(d) |- [d]U(u) = [d]U(ub)*[d]U(u'):cap
          [d]U(u) |- [d]U(ub)*[d]U(u')
By lemma: [d]C(ub#a) |- [d]A(a')*true
          [d]U(ub)*([d]A(a)*true) |- [d]A(a')*true

Abbreviate Uu=[d]U(u), Uu'=[d]U(u'), Ub=[d]U(ub), Aa=[d]A(a), Aa'=[d]A(a')

              Ub,Aa*true |- Ub*(Aa*true)    Ub*(Aa*true) |- Aa'*true
              ------------------------------------------------------ cut
Uu' |- Uu'                  Ub,Aa*true |- Aa'*true
--------------------------------------------------
                Ub,Uu',(Aa*true) |- Uu'*(Aa'*true)
                ----------------------------------
Uu |- Ub*Uu'    Ub*Uu',(Aa*true) |- Uu'*(Aa'*true)
-------------------------------------------------- cut
Uu,(Aa*true) |- Uu'*(Aa'*true)
------------------------------
Uu*(Aa*true) |- Uu'*(Aa'*true)


CASE:

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

E(halt) = halt

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