=================================================
================== CC/SLL =======================
=================================================

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

from CC/CCL, keep: k,b,t,r,g,y,z,v,h,op,l,e,w,m
from lang0, keep: o,d
from lang0, keep c, but change {A} to {r}:

c = A | {} | {r} | c1*c2 | c1&c2 | c1 -o c2 | true

define m1,m2 = m3 if dom(m1) U dom(m2) = dom(m3) and dom(m1),dom(m2) disjoint

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

From langccl:
  keep d |- .
  keep d |- d',A:k

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

From langccl:
  keep d |- .
  keep d |- g,x:t

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

From langccl:
  keep ...,A:k,... |- A:k
  keep d |- int:type
  keep d |- r handle:type
  keep d |- q:res
  keep d |- <t1,...,tn> at r:type
  keep d |- all[d'](c,t1...tn)->0 at r:type
  keep |- {q1:y1...qn:yn}
  keep |- {i1:t1...in:tn}

from lang3a, keep all d |- c:cap rules, but change {A} to {r}:

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

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

From langccl:
  keep d |- . = .
  keep d | d1,A:k = d2,A:k

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

from lang3a, keep all o |- c rules

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

From langccl:
  keep d |- b = b:k
  keep d |- b1 = b2:k
  keep d |- b1 = b3:k

From lang3a:
  keep d |- c1 = c2:k

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

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

From langccl:
  keep d |- <t1,...,tn> at r = <t1',...,tn'> at r:type
  keep d'' |- all[d](c,t1...tn)->0 at r = all[d'](c',t1'...tn')->0 at r:type

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

From langccl:
  keep z;d;g |- fix x[d'](c,x1:t1...xn:tn).e at r: tf
  keep z;d;g |- <v1...vn> at r:<t1...tn> at r
  keep z;d;g |- h at r: t

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

From langccl:
  keep z;d;...,x:t,... |- x: t
  keep z;d;g |- n:int
  keep z;d;g |- q.i:<t1...tn> at q
  keep z;d;g |- q.i:all[d'](c,t1...tn)->0 at q
  keep z;d;g |- q.i:z(q.i)
  keep z;d;g |- handle(q):q handle
  keep d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r)
  keep z;d;g |- v: t

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

From langccl:
  keep z;d;g;c |- x=v ==> d;g,x:t;c
  keep z;d;g;c |- x=v1 op v2 ==> d;g,x:int;c

z;d;g |- v:r handle
z;d;g |- h at r:t
d |- c <= {r}*true
--------------------------------- (x not in dom(g))
z;d;g;c |- x=h at v ==> d;g,x:t;c

z;d;g |- v:<t0...tm-1> at r
d |- c <= {r}*true
------------------------------ (x not in dom(g) and 0<=n<m)
z;d;g;c |- x=v.n ==> d;g,x:tm;c

d |- c*{A} = c':cap
-------------------------------------------------(A not in dom(d) and x not in dom(g))
z;d;g;c |- newrgn A,x ==> d,A:res;g,x:A handle;c'

z;d;g |- v: r handle
d |- c = c'*{r}:cap
-------------------------------
z;d;g;c |- freergn v ==> d;g;c'

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

From langccl:
  keep z;d;g;c |- let l in e
  keep z;d;g;c |- if0 v then e2 else e3

z;d;g |- v: all[](c',t1...tn)->0 at r
z;d;g |- v1: t1
...
z;d;g |- vn: tn
d |- c <= {r}*true
d |- c <= c'
---------------------
z;d;g;c |- v(v1...vn)

z;d;g |- v:int
-----------------
z;d;g;c |- halt v

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

From langccl:
  keep |- q1->w1...qn->wn:z
  keep z |- {i1->h1...in->hn} at q:{i1:t1...in:tn}
  keep |- (m,e)

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

{} sat {}

{q:y} sat {q}

z1 sat c1
z2 sat c2
---------------
z1,z2 sat c1*c2

z sat c1
z sat c2
-----------
z sat c1&c2

forall z2.(z2=z,z1 and z1 sat c1 ==> z2 sat c2)
-----------------------------------------------
z sat c1 -o c2

z sat true

z1 sat c1
...
zn sat cn
-----------------------
z1,...,zn sat c1,...,cn

=================================================
========== CC/CCL->CC/SLL TRANSLATION ===========
=================================================

From lang1:
  keep C,S,D (call these C1,S1,D1)
    change {A p} to {r p}

From lang2:
  keep U,A,D,[] (call these U2,A2,D2,[]2)
    change {A p} to {r p}
  keep d |- c1<=c2 ~~> ub
    change {A p} to {r p}

From lang3:
  keep U,A,D,[] (call these U3,A3,D3,[]3)
    change {A p} to {r p} and {A} to {r}

C(d,c) = [d]C(c)
C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)
D(d) = D3(D2(D1(d)))
[d] = [D2(D1(d))]3 U3([D1(d)]2)

U3([A1<-u1...An<-un]) = [A1<-U3(u1)...An<-U3(un)]

T(A) = A
T(int) = int
T(r handle) = r handle
T(all[d](c,t1...tn)->0 at r) = all[D(d)]([d]C(c),[d]T(t1)...[d]T(tn))->0 at r
T(<t1...tn> at r) = <T(t1)...T(tn)> at r

G(.) = .
G(x:t,g) = x:T(t),G(g)
Y(i1:t1...in:tn) = i1:T(t1)...in:T(tn)
Z(q1:y1...qn:yn) = q1:Y(y1)...qn:Y(yn)

z;d;g |- v:t ~~> v'
z;d;g |- h at r:t ~~> h'
z;d;g;c |- l ==> d';g';c' ~~> l'
z;d;g;c |- e ~~> e'
(but continue to write V(v),H(h at r),L(l),E(e) when typing derivation not relevant)

V(x) = x
V(n) = n
V(q.i) = q.i
V(handle(q)) = handle(q)

k=res
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[b]

k=type
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[T(b)]

k=cap
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[A3(A2(S1(b)))][U3(U2(C1(b)))][A3(A2(C1(b)))]

z;d;g |- v: all[A<=c'',d'](c',t1...tn)->0 at r ~~> v'
d |- c <= c''
D1(d) |- C1(c)<=C1(c'') ~~> ub
--------------------------------------------------
z;d;g |- v[c]: [A<-c](all[d'](c',t1...tn)->0 at r) ~~> v'[A3(A2(S1(c)))][U3(ub)][A3(A2(C1(c)))]

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

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

H(fix x[d](c,x1:t1,...,xn:tn).e at r) = fix x[D(d)]([d]C(c),x1:[d]T(t1)...xn:[d]T(tn)).E(e)
H(<v1...vn> at r) = <V(v1)...V(vn)>

L(x=v) = x=V(v)
L(x=v1 op v1) = x=V(v1) op V(V2)

z;d;g |- v:r handle ~~> v'
z;d;g |- h at r:t ~~> h'
d |- c<=c'+{r+}
--------------------------------- (x not in dom(g))
z;d;g;c |- x=h at v ==> d;g,x:t;c ~~> x=h' at v'

L(x=v.n) = x=V(v).n
L(newrgn A,x) = newrgn A,x
L(freergn v) = freergn V(v)
E(let l in e) = let L(l) in E(e)
E(if0 v then e2 else e3) = if0 V(v) then E(e2) else E(e3)
E(v(v1...vn)) = V(v)(V(v1)...V(vn))
E(halt v) = halt V(v)

|- z
z |- w1 at q1:y1~~>w1'
...
z |- wn at qn:yn~~>wn'
z = q1:y1...qn:yn
--------------------
|- q1->w1...qn->wn:z~~>q1->w1'...qn->wn'

z;; |- h1 at q:t1~~>h1'
...
z;; |- hn at q:tn~~>hn'
-------------------------------------------
z |- {i1->h1...in->hn} at q:{i1:t1...in:tn}~~>{i1->h1'...in->hn'}

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

Key lemma for soundness ("sat preservation"):
 -- if z sat o and o |- c then z sat c

Lemmas from the Walker,Crary,Morrisett tech report (WCM-TR) that easily continue to hold:
  10, 11, 12, 13, 14, 15, 24 (where 24.A2 is omitted), 25, 26, 27, 30, 31, 32
In addition, Theorem 39 (soundness) easily holds, given the proofs of preservation and progress below.
Due to CC/SLL's weak halt rule, theorem 40 (complete collection) does not hold.

Lemmas 18,20,21,22,23,33 are irrelevant (replaced by sat preservation).

Lemmas shown below:
-- Lemma 28
-- Lemma 29
-- Lemma 34
-- Lemma 35
-- Lemma 36 (preservation)
-- Lemma 37 (progress)

Translation lemmas:
 -- if |- d and d |- r:res then [d]r = r
 -- lemma -1: If |- d and d |- c:cap then D(d) |- [d]C(c):cap
 -- lemma -2: If |- d and d |- c1=c2:cap then D(d) |- [d]C(c1)=[d]C(c2):cap
 -- lemma -3: If |- d and d |- c1<=c2 then D(d) |- [d]C(c1)<=[d]C(c2)
              If in addition D1(d) |- C1(c1)<=C1(c2) ~~> u
                then D(d) |- [d]U3(U2(C1(c1)))=[d]U3(u+U2(C1(c2))):cap
                 and D(d) |- [d]U3(u)*[d]A3(A2(C1(c1)))*true<=[d]A3(A2(C1(c2)))*true
 -- lemma -4: If |- d and d |- c=c'+{r~}:cap then D(d) |- [d]C(c)=([d]C(c'))*{r}:cap
 -- lemma -5: If |- d and d |- c<=c'+{r+} then D(d) |- [d]C(c)<={r}*true
 -- lemma -6: If |- d then |- [d]C({})

 -- if |- d and d |- t:type then D(d) |- [d]T(t):type
 -- if |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type
 -- if |- z and z(q.i) exists then Z(z)(q.i) = [d]T(z(q.i))
 -- if |- d and d |- A':cap and d |- c:cap
     then C([A'<-c']c) = [Au'<-U3(U2(C1(c'))),Aa'<-A3(A2(C1(c'))),Asu'<-U3(U2(S1(c'))),Asa'<-A3(A2(S1(c')))]C(c)
 -- if |- d and d |- A':cap and d |- t:type
     then T([A'<-c']t) = [Au'<-U3(U2(C1(c'))),Aa'<-A3(A2(C1(c'))),Asu'<-U3(U2(S1(c'))),Asa'<-A3(A2(S1(c')))]T(t)
 -- if |- d and d |- A':type and d |- t:type then T([A'<-t']t) = [A'<-T(t')]T(t)
 -- if |- z and |- d and d |- g then:
    - if z;d;g |- v:t ~~> v' then Z(z);D(d);[d]G(g) |- [d]v':[d]T(t)
    - if z;d;g |- h at r:t ~~> h' then Z(z);D(d);[d]G(g) |- [d]h' at r:[d]T(t)
    - if z;d;g;c |- l==>d';g';c' ~~> l' then Z(z);D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c') and [d]=[d']
    - if z;d;g;c |- e ~~> e' then Z(z);D(d);[d]G(g);[d]C(c) |- [d]e'
 -- if |-z and |- m:z~~>m' and z sat c and z;;;c |- e~~>e'
     then |- m':Z(z) and Z(z) sat C(c) and Z(z);;;C(c) |- e'

The proofs of the lemmas also rely on lemmas from lang1, lang2, lang3a
(adapted to use {r} in place of {A} and {r p} in place of {A p}).

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

  - if z sat o and o |- c then z sat c

EASY CASES:

c |- c

|- {}

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


CASE:

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

inverting z sat o1,o2 yields z=z1,z2 where z1 sat o1 and z2 sat o2
by induction, z1 sat c1
by induction, z2 sat c2
by rule, z1,z2 sat c1*c2


CASE:

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

inverting z sat o,c1*c2 yields z=z0,z1,z2 where z0 sat o and z1 sat c1 and z2 sat c2
by induction, z0,z1,z2 sat c3


CASE:

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

z sat o
by induction, z sat c1
by induction, z sat c2
by rule, z sat c1&c2


CASE:

o,ck |- c3
------------- k=1 or k=2
o,c1&c2 |- c3

inverting z sat o,c1&c2 yields z=z',z'' where z' sat o and z'' sat c1&c2
inverting z'' sat c1&c2 yields z'' sat ck
by induction, z sat c3


CASE:

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

z sat o
for any z2 such that z2=z,z1 and z1 sat c1:
  z2 sat o,c1
  by induction, z2 sat c2
by rule, z sat c1 -o c2


CASE:

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

inverting z sat o1,o2,c1 -o c2 yields z=z1,z2,z' where z1 sat o1 and z2 sat o2 and z' sat c1 -o c2
by induction, z1 sat c1
inverting z' sat c1 -o c2 yields forall z2'.(z2'=z',z1' and z1' sat c1 ==> z2' sat c2)
  choosing z2'=z',z1 proves z',z1 sat c2
  so z2,z',z1 sat o2,c2
by induction, z2,z',z1 sat c3


EASY CASE:

o |- true

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

 -- if |- d and d |- r:res then [d]r = r

If r = q, then [d]{q} = {q}
Otherwise, r = A and d |- A:res, so d(A)=res, so [d]A = A, by definition of [d]

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

lemma -1: If |- d and d |- c:cap then D(d) |- [d]C(c):cap

C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)
D(d) = D3(D2(D1(d)))
[d] = [D2(D1(d))]3 U3([D1(d)]2)

From lang1:
 -- if |- d then |- D1(d)
 -- if d |- c:cap then D1(d) |- C1(c):cap
From lang2:
 -- if |- d then |- D2(d)
 -- if |- d and d |- c:cap then D2(d) |- [d]2 U2(c):cap~
 -- if |- d and d |- c:cap then D2(d) |- [d]2 A2(c):cap+
 so:
 -- if |- D1(d) then |- D2(D1(d))
 -- if |- D1(d) and D1(d) |- C1(c):cap then D2(D1(d)) |- [D1(d)]2 U2(C1(c)):cap~
 -- if |- D1(d) and D1(d) |- C1(c):cap then D2(D1(d)) |- [D1(d)]2 A2(C1(c)):cap+
From lang3a:
 -- if |- d and d |- u:cap~ then D3(d) |- [d]3 U3(u):cap
 -- if |- d and d |- a:cap+ then D3(d) |- [d]3 A3(a):cap
 so:
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 U2(C1(c)):cap~ then D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c))):cap
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 A2(C1(c)):cap+ then D3(D2(D1(d))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c))):cap

So:
 D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c))):cap
 D3(D2(D1(d))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c))):cap

 D(d) |- [d]U3(U2(C1(c))):cap
 D(d) |- [d]A3(A2(C1(c))):cap

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

lemma -2: If |- d and d |- c1=c2:cap then D(d) |- [d]C(c1)=[d]C(c2):cap

C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)
D(d) = D3(D2(D1(d)))
[d] = [D2(D1(d))]3 U3([D1(d)]2)

From lang1:
 -- if |- d then |- D1(d)
 -- if d |- c1=c2:cap then D1(d) |- C1(c1)=C1(c2):cap
From lang2:
 -- if |- d then |- D2(d)
 -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D2(d) |- [d]2 U2(c1)=[d]2 U2(c2):cap~
 -- if |- d and d |- c1=c2:k and k=cap or k=cap+ then D2(d) |- [d]2 A2(c1)=[d]2 A2(c2):cap+
 so:
 -- if |- D1(d) then |- D2(D1(d))
 -- if |- D1(d) and D1(d) |- C1(c1)=C1(c2):cap then D2(D1(d)) |- [D1(d)]2 U2(C1(c1))=[D1(d)]2 U2(C1(c2)):cap~
 -- if |- D1(d) and D1(d) |- C1(c1)=C1(c2):cap then D2(D1(d)) |- [D1(d)]2 A2(C1(c1))=[D1(d)]2 A2(C1(c2)):cap+
From lang3:
 -- if |- d and d |- u1=u2:cap~ then D3(d) |- [d]3 U3(u1)=[d]3 U3(u2):cap
 -- if |- d and d |- a1=a2:cap+ then D3(d) |- [d]3 A3(a1)*true=[d]3 A3(a2)*true:cap
 so:
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 U2(C1(c1))=[D1(d)]2 U2(C1(c2)):cap~
    then D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c1)))=[D2(D1(d))]3 U3([D1(d)]2 U2(C1(c2))):cap
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 A2(C1(c1))=[D1(d)]2 A2(C1(c2)):cap+
    then D3(D2(D1(d))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c1)))*true=[D2(D1(d))]3 A3([D1(d)]2 A2(C1(c2)))*true:cap
So:
  D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c1)))=[D2(D1(d))]3 U3([D1(d)]2 U2(C1(c2))):cap
  D3(D2(D1(d))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c1)))*true=[D2(D1(d))]3 A3([D1(d)]2 A2(C1(c2)))*true:cap

  D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2) U3(U2(C1(c1)))=[D2(D1(d))]3 U3([D1(d)]2) U3(U2(C1(c2))):cap
  D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2) A3(A2(C1(c1)))*true=[D2(D1(d))]3 U3([D1(d)]2) A3(A2(C1(c2)))*true:cap

  D(d) |- [d] U3(U2(C1(c1)))=[d] U3(U2(C1(c2))):cap
  D(d) |- [d] A3(A2(C1(c1)))*true=[d] A3(A2(C1(c2)))*true:cap

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

lemma -3: If |- d and d |- c1<=c2 then D(d) |- [d]C(c1)<=[d]C(c2)
  If in addition D1(d) |- C1(c1)<=C1(c2) ~~> u
    then D(d) |- [d]U3(U2(C1(c1)))=[d]U3(u+U2(C1(c2))):cap
     and D(d) |- [d]U3(u)*[d]A3(A2(C1(c1)))*true<=[d]A3(A2(C1(c2)))*true

By lemma -1, D(d) |- [d]C(c1):cap 
By lemma -1, D(d) |- [d]C(c2):cap 

C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)
D(d) = D3(D2(D1(d)))
[d] = [D2(D1(d))]3 U3([D1(d)]2)
define C3(u#a) = U3(U)*A3(a)*true

From lang1:
 -- if |- d then |- D1(d)
 -- if d |- c1<=c2 then D1(d) |- C1(c1)<=C1(c2)
From lang2:
 -- if |- d then |- D2(d)
 -- if |- d and d |- c1<=c2~~>u then D2(d) |- [d]2 U2(c1)=[d]2 u+[d]2 U2(c2):cap~ and D2(d) |- [d]2 u#[d]2 A2(c1)<=[d]2 A2(c2)
 so:
 -- if |- D1(d) then |- D2(D1(d))
 -- if |- D1(d) and D1(d) |- C1(c1)<=C1(c2)~~>u
    then D2(D1(d)) |- [D1(d)]2 U2(C1(c1))=[D1(d)]2 u+[D1(d)]2 U2(C1(c2)):cap~
     and D2(D1(d)) |- [D1(d)]2 u#[D1(d)]2 A2(C1(c1))<=[D1(d)]2 A2(C1(c2))
From lang3a:
 -- if |- d and d |- u1=u2:cap~ then D3(d) |- [d]3 U3(u1)=[d]3 U3(u2):cap
 -- if |- d and d |- c<=a then [d]3 C3(c) |- [d]3 A3(a)*true
 so:
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 U2(C1(c1)) = [D1(d)]2 u+[D1(d)]2 U2(C1(c2)):cap~
    then D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c1))) = [D2(D1(d))]3 U3([D1(d)]2 u+[D1(d)]2 U2(C1(c2))):cap
 -- if |- D2(D1(d)) and D2(D1(d)) |- [D1(d)]2 u#[D1(d)]2 A2(C1(c1))<=[D1(d)]2 A2(C1(c2))
    then [D2(D1(d))]3 C3([D1(d)]2 u#[D1(d)]2 A2(C1(c1))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c2)))*true
So:
  D3(D2(D1(d))) |- [D2(D1(d))]3 U3([D1(d)]2 U2(C1(c1))) = [D2(D1(d))]3 U3([D1(d)]2 u+[D1(d)]2 U2(C1(c2))):cap
  [D2(D1(d))]3 C3([D1(d)]2 u#[D1(d)]2 A2(C1(c1))) |- [D2(D1(d))]3 A3([D1(d)]2 A2(C1(c2)))*true

  D(d) |- [d]U3(U2(C1(c1))) = [d]U3(u+U2(C1(c2))):cap
  [d]C3(u#A2(C1(c1))) |- [d]A3(A2(C1(c2)))*true

  [d]U3(U2(C1(c1))) |- [d]U3(u+U2(C1(c2)))
  [d]C3(u#A2(C1(c1))) |- [d]A3(A2(C1(c2)))*true

Let u1 = [d]U3(U2(C1(c1)))
Let u2 = [d]U3(U2(C1(c2)))
Let a1 = [d]A3(A2(C1(c1)))
Let a2 = [d]A3(A2(C1(c2)))
Let u3 = [d]U3(u)
[d]U3(u+U2(C1(c2))) = [d]U3(u)*[d]U3(U2(C1(c2))) = u3*u2
[d]C3(u#A2(C1(c1))) = [d]U3(u)*[d]A3(A2(C1(c1)))*true = u3*a1
So:
  u1 |- u3*u2
  u3*a1 |- a2*true

                                 u3*a1 |- a2*true    a2*true,u2,true |- u2*a2*true
                                 ------------------------------------------------- cut
               u3,a1 |- u3*a1    u3*a1,u2,true |- u2*a2*true
               --------------------------------------------- cut
               u3,a1,u2,true |- u2*a2*true
               ---------------------------
u1 |- u3*u2    u3*u2,a1,true |- u2*a2*true
------------------------------------------ cut
u1,a1,true |- u2*a2*true
------------------------
u1*a1*true |- u2*a2*true

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

lemma -4: If |- d and d |- c=c'+{r~}:cap then D(d) |- [d]C(c)=([d]C(c'))*{r}:cap

C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)

C1(c'+{r~}) = c1+{r~} = for c1=C1(c')
U2(c1+{r~}) = u2+{r~} for u2=U2(c1)
A2(c1+{r~}) = a2 for a2=A2(c1)
U3(u2+{r~}) = u3*{r} for u3=U3(u2)
A3(a2) = a3 for a3=A3(a2)

By lemma -2, D(d) |- [d]C(c)=[d]C(c'+{r~})
so D(d) |- [d]C(c)=[d](u3*{r}*a3*true)
so D(d) |- [d]C(c)=([d]u3*a3*true)*{r}
so D(d) |- [d]C(c)=([d]C(c'))*{r}

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

lemma -5: If |- d and d |- c<=c'+{r+} then D(d) |- [d]C(c)<={r}*true

C(c) = (U3(U2(C1(c)))*A3(A2(C1(c)))*true)

C1(c'+{r+}) = c1+{r+} = for c1=C1(c')
U2(c1+{r+}) = u2 for u2=U2(c1)
A2(c1+{r+}) = a2+{r+} for a2=A2(c1)
U3(u2) = u3 for u3=U3(u2)
A3(a2+{r+}) = (a3*true) & ({r}*true) for a3=A3(a2)

By lemma -3, D(d) |- [d]C(c)<=[d]C(c'+{r+})
so D(d) |- [d]C(c)<=[d](u3*((a3*true) & ({r}*true))*true)
so D(d) |- [d]C(c)<=([d]u3*(([d]a3*true) & ({r}*true))*true)
so [d]C(c) |- [d]u3*(([d]a3*true) & ({r}*true))*true

[d]u3,{r},true,true |- {r}*true
--------------------------------------------------
[d]u3,{r}*true,true |- {r}*true
--------------------------------------------------
[d]u3,([d]a3*true) & ({r}*true),true |- {r}*true
--------------------------------------------------
[d]u3*(([d]a3*true) & ({r}*true))*true |- {r}*true

D(d) |- [d]C(c)<=([d]u3*(([d]a3*true) & ({r}*true))*true) implies D(d) |- {r}*true:cap

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

lemma -6: If |- d then |- [d]C({})

C1({}) = {}
U2({}) = {}
A2({}) = {}
U3({}) = {}
A3({}) = {}
[d]C({}) = {}*{}*true

|- {}    |- {}    |- true
-------------------------
|- {}*{}*true

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

if |- z and z(q.i) exists then Z(z)(q.i) = [d]T(z(q.i))

Definition of Z(z) implies Z(z)(q.i) = T(z(q.i))

Definition of |- z implies |- z(q.i):type
  by lemma, |- T(z(q.i)):type
  so T(z(q.i)) has no free type variables
  so [d]T(z(q.i)) = T(z(q.i))

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

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

EASY CASES:

T(A) = A
T(int) = int
T(r handle) = r handle
T(<t1...tn> at r) = <T(t1)...T(tn)> at r


CASE:

d |- d'
d,d' |- t1:type
...
d,d' |- tn:type
d,d' |- c:cap
d |- r:res
------------------------------------
d |- all[d'](c,t1...tn)->0 at r:type

d |- d' implies that d,d' contains no duplicate variable bindings, so D(d) |- [d]D(d') must hold.

By induction:
  D(d,d') |- [d,d']T(tk):type
By lemma:
  D(d,d') |- [d,d']C(c):cap
By cases r=q and r=A:
  D(d,d') |- r:res

D(d,d')
  = D3(D2(D1(d,d')))
  = D3(D2(D1(d),D1(d')))
  = D3(D2(D1(d)),[D1(d)]2 D2(D1(d')))
  = D3(D2(D1(d))), [D2(D1(d))]3 D3([D1(d)]2 D2(D1(d')))
  = D3(D2(D1(d))), [D2(D1(d))]3 U3([D1(d)]2) D3(D2(D1(d')))
  = D(d), [d]D(d')

D(d) |- [d]D(d')
D(d),[d]D(d') |- [d][d']T(t1):type
...
D(d),[d]D(d') |- [d][d']T(tn):type
D(d),[d]D(d') |- [d][d']C(c):cap
D(d),[d]D(d') |- r:res
------------------------------------
D(d) |- all[[d]D(d')][d][d'](C(c),T(t1)...T(tn))->0 at r:type

[d]T(all[d'](c,t1...tn)->0 at r)
  = [d]all[D(d')]([d']C(c),[d']T(t1)...[d']T(tn))->0 at r
  = all[[d]D(d')][d][d'](C(c),T(t1)...T(tn))->0 at r

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

if |- d and d |- t1=t2:type then D(d) |- [d]T(t1)=[d]T(t2):type

EASY CASES:

T(A) = A
T(int) = int
T(r handle) = r handle
T(<t1...tn> at r) = <T(t1)...T(tn)> at r


CASE:

d'' |- d = d'
d'',d |- t1 = t1':type
...
d'',d |- tn = tn':type
d'',d |- c = c':cap
d |- r:res
---------------------------------------------------------------------
d'' |- all[d](c,t1...tn)->0 at r = all[d'](c',t1'...tn')->0 at r:type

d'' |- d = d' implies that d and d' share the same variable-to-kind mappings,
so D(d) and D(d') also share the same variable-to-kind mappings,
so D(d'') |- D(d) = D(d')

Rest of case follows case for D(d) |- [d]T(t):type proof, with
  t=t':type replacing t:type
  c=c':cap replacing c:cap
  r=r':res replacing r:res

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

if |- d and d |- A':cap and d |- c:cap
then C([A'<-c']c) = [Au'<-U3(U2(C1(c'))),Aa'<-A3(A2(C1(c'))),Asu'<-U3(U2(S1(c'))),Asa'<-A3(A2(S1(c')))]C(c)

Composing the following lemmas:
 From lang1:
 -- if |- d then |- D1(d)
 -- if d |- c:cap then D(d) |- S(c):cap+
 -- if d |- c:cap then D(d) |- C(c):cap
 -- if |- d and d |- A':cap and d |- c:cap then C1([A'<-c']c) = [A'<-C1(c'),As'<-S1(c')]C1(c)
 From lang2:
 -- if |- d then |- D2(d)
 -- 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 |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then A2([A'<-c']c) = [Au'<-U2(c'),Aa'<-A2(c')]A2(c)
 -- if |- d and d |- A':k' (k'=cap or k'=cap+) and d |- c:k (k=cap or k=cap+) then U2([A'<-c']c) = [Au'<-U2(c'),Aa'<-A2(c')]U2(c)
 From lang3:
 -- if |- d and d |- A':cap+ and d |- a:cap+ then A3([A'<-a']a) = [A'<-A3(a')]A3(a)
 -- if |- d and d |- A':cap+ and d |- u:cap~ then U3([A'<-a']u) = [A'<-a'']U3(u) for any a''
 -- if |- d and d |- A':cap~ and d |- a:cap+ then A3([A'<-u']a) = [A'<-u'']A3(a) for any u''
 -- if |- d and d |- A':cap~ and d |- u:cap~ then U3([A'<-u']u) = [A'<-U3(u')]U3(u)

yields:
  C([A'<-c']c)
    = (U3(U2(C1([A'<-c']c)))*A3(A2(C1([A'<-c']c)))*true)
    = (U3(U2([A'<-C1(c'),As'<-S1(c')]C1(c)))*
       A3(A2([A'<-C1(c'),As'<-S1(c')]C1(c)))*true)
    = (U3([Au'<-U2(C1(c')),Aa'<-A2(C1(c')),Asu'<-U2(S1(c')),Asa'<-A2(S1(c'))]U2(C1(c)))*
       A3([Au'<-U2(C1(c')),Aa'<-A2(C1(c')),Asu'<-U2(S1(c')),Asa'<-A2(S1(c'))]A2(C1(c)))*true)
    = ([Au'<-U3(U2(C1(c'))),Aa'<-ua,Asu'<-U3(U2(S1(c'))),Asa'<-usa]U3(U2(C1(c)))*
       [Au'<-au,Aa'<-A3(A2(C1(c'))),Asu'<-asu,Asa'<-A3(A2(S1(c')))]A3(A2(C1(c)))*true)
for any ua,usa,au,asu
choose ua=A3(A2(C1(c')))
choose usa=A3(A2(S1(c')))
choose au=U3(U2(C1(c')))
choose asu=U3(U2(S1(c')))

C([A'<-c']c) = [Au'<-U3(U2(C1(c'))),Aa'<-A3(A2(C1(c'))),Asu'<-U3(U2(S1(c'))),Asa'<-A3(A2(S1(c')))]C(c)

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

if |- d and d |- A':cap and d |- t:type
then T([A'<-c']t) = [Au'<-U3(U2(C1(c'))),Aa'<-A3(A2(C1(c'))),Asu'<-U3(U2(S1(c'))),Asa'<-A3(A2(S1(c')))]T(t)

easy induction, using C([A'<c']c) lemma above

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

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

easy induction

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

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


EASY CASES:

From langccl:
  keep z;d;...,x:t,... |- x: t
  keep z;d;g |- n:int
  keep z;d;g |- q.i:<t1...tn> at q
  keep z;d;g |- q.i:all[d'](c,t1...tn)->0 at q
  keep z;d;g |- handle(q):q handle


CASE:

z;d;g |- q.i:z(q.i) ~~> q.i

Z(z);D(d);[d]G(g) |- q.i:Z(z)(q.i)

By lemma, Z(z)(q.i) = [d]T(z(q.i))


EASY CASES:

k=res
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[b]

k=type
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[T(b)]


CASE:

k=cap
z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r ~~> v'
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r) ~~> v'[A3(A2(S1(b)))][U3(U2(C1(b)))][A3(A2(C1(b)))]

Similar to v[c] case below.


CASE:

z;d;g |- v: all[A<=c'',d'](c',t1...tn)->0 at r ~~> v'
d |- c <= c''
D1(d) |- C1(c)<=C1(c'') ~~> ub
--------------------------------------------------
z;d;g |- v[c]: [A<-c](all[d'](c',t1...tn)->0 at r) ~~> v'[A3(A2(S1(c)))][U3(ub)][A3(A2(C1(c)))]

By induction, then Z(z);D(d);[d]G(g) |- [d]v':[d]T(all[A<=c'',d'](c',t1...tn)->0 at r)

T(all[A<=c'',d'](c',t1...tn)->0 at r)
  = all[D(A<=c'',d')](C(c'),T(t1)...T(tn))->0 at r
  = all[D3(D2(D1(A<=c'',d')))](C(c'),T(t1)...T(tn))->0 at r
  = all[D3(D2(As:cap+<=S1(c''), (A:cap<=C1(c''),As), D1(d')))](C(c'),T(t1)...T(tn))->0 at r
  = all[D3(
           Asa:cap+ where {}#Asa<=A2(S1(c'')), [Asu<-{}]
           Ab:cap~, Aa:cap+ where Ab#Aa<=A2(C1(c'')),Ab+U2(C1(c''))#Aa<=A2(As), [Au<-Ab+U2(C1(c''))]
           D2(D1(d')))](C(c'),T(t1)...T(tn))->0 at r
  = all[
        Asa:cap, [Asa<-(Asa&(U3({}) -o A3(A2(S1(c'')))*true))] U3([Asu<-{}])
        Ab:cap,
        Aa:cap, [Aa<-(Aa&(U3(Ab) -o A3(A2(C1(c'')))*true)&(U3(Ab+U2(C1(c''))) -o A3(A2(As))*true))] U3([Au<-Ab+U2(C1(c''))])
        D3(D2(D1(d')))](C(c'),T(t1)...T(tn))->0 at r
  = all[
        Asa:cap, [Asa<-(Asa&({} -o s''*true))] [Asu<-{}]
        Ab:cap,
        Aa:cap, [Aa<-(Aa&(Ab -o a''*true)&(Ab*u'' -o Asa*true))] [Au<-Ab*u'']
        D(d')](C(c'),T(t1)...T(tn))->0 at r
where s'' = A3(A2(S1(c'')))
where s0'' = U3(U2(S1(c'')))
where a'' = A3(A2(C1(c'')))
where u'' = U3(U2(C1(c'')))

[A<=c'']
  = [D2(D1(A<=c''))]3 U3([D1(A<=c'')]2)
  = [Asa:cap+ where {}#Asa<=A2(S1(c'')), [Asu<-{}]
           Ab:cap~, Aa:cap+ where Ab#Aa<=A2(C1(c'')),Ab+U2(C1(c''))#Aa<=A2(As)]3
    U3([As:cap+<=S1(c''), (A:cap<=C1(c''),As)]2)
  = [Asa<-(Asa&({} -o s''*true))]
    [Aa<-[Asu<-{}](Aa&(Ab -o a''*true)&(Ab*u'' -o Asa*true))]
    U3([Asu<-{}][Au<-Ab+U2(C1(c''))])
  = [Asa<-(Asa&({} -o s''*true))]
    [Aa<-[Asu<-{}](Aa&(Ab -o a''*true)&(Ab*u'' -o Asa*true))]
    [Asu<-{}][Au<-Ab*u'']
  = [Asa<-(Asa&({} -o s''*true))]
    [Asu<-{}]
    [Aa<-(Aa&(Ab -o a''*true)&(Ab*u'' -o Asa*true))]
    [Au<-Ab*u'']

T(all[A<=c'',d'](c',t1...tn)->0 at r)
  = all[Asa:cap,Ab:cap,Aa:cap,[A<=c'']D(d')].[A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r

Z(z);D(d);[d]G(g) |- [d]v':[d]all[Asa:cap,Ab:cap,Aa:cap,[A<=c'']D(d')].[A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- [d]v':all[Asa:cap,Ab:cap,Aa:cap,[d][A<=c'']D(d')].[d][A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- ([d]v')[[d]s]:[Asa<-[d]s]
                       all[Ab:cap,Aa:cap,[d][A<=c'']D(d')].[d][A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- ([d]v')[[d]s][[d]U3(ub)]:[Ab<-[d]U3(ub)][Asa<-[d]s]
                       all[Aa:cap,[d][A<=c'']D(d')].[d][A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- ([d]v')[[d]s][[d]U3(ub)][[d]a]:[Aa<-[d]a][Ab<-[d]U3(ub)][Asa<-[d]s]
                       all[[d][A<=c'']D(d')].[d][A<=c'',d'](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- [d](v'[s][U3(ub)][a]):[d][Aa<-a][Ab<-U3(ub)][Asa<-s][A<=c'']
                       all[D(d')].[d'](C(c'),T(t1)...T(tn))->0 at r
where s0 = U3(U2(S1(c)))
where s = A3(A2(S1(c)))
where a = A3(A2(C1(c)))
where u = U3(U2(C1(c)))

By lemma:
T([A<-c](all[d'](c',t1...tn)->0 at r))
  = [Au<-U3(U2(C1(c))),Aa<-A3(A2(C1(c))),Asu<-U3(U2(S1(c))),Asa<-A3(A2(S1(c)))]T(all[d'](c',t1...tn)->0 at r)
  = [Au<-u,Aa<-a,Asu<-s0,Asa<-s]T(all[d'](c',t1...tn)->0 at r)
  = [Au<-u,Aa<-a,Asu<-s0,Asa<-s]all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r

We know:
Z(z);D(d);[d]G(g) |- [d](v'[s][U3(ub)][a]):
                       [d][Aa<-a][Ab<-U3(ub)][Asa<-s][A<=c''] all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r

We need to prove:
Z(z);D(d);[d]G(g) |- [d](v'[s][U3(ub)][a]):
                       [d][Au<-u,Aa<-a,Asu<-s0,Asa<-s]        all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r

Prove this by showing:
D(d) |-                [d][Aa<-a][Ab<-U3(ub)][Asa<-s][A<=c''] all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r
      =                [d][Au<-u,Aa<-a,Asu<-s0,Asa<-s]        all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r  :type
then use v retyping rule for equivalent types (if v:t' and t=t' then v:t).

To show type equivalence, first show substitution equivalence:
  For each A<-c1 in [d][Aa<-a][Ab<-U3(ub)][Asa<-s][A<=c'']
       and A<-c2 in [d][Au<-u,Aa<-a,Asu<-s0,Asa<-s]
  either D(d) |- c1 = c2:cap
      or A is not free in all[D(d')][d'](C(c'),T(t1)...T(tn))->0 at r
Type equivalence then follows (easy induction)

(note that well-formedness of c and c'' in d implies that Aa,Ab,Asa,Asu do not appear free in s0,u,a,s,s0'',u'',a'',s'')
[Aa<-a][Ab<-U3(ub)][Asa<-s][A<=c'']
  = [Aa<-a][Ab<-U3(ub)][Asa<-s]
    [Asa<-(Asa&({} -o s''*true))]
    [Asu<-{}]
    [Aa<-(Aa&(Ab -o a''*true)&(Ab*u'' -o Asa*true))]
    [Au<-Ab*u'']
  = [Asa<-(s&({} -o s''*true)),
     Asu<-{},
     Aa<-(a&(U3(ub) -o a''*true)&(U3(ub)*u'' -o (s&({} -o s''*true))*true)),
     Au<-U3(ub)*u'',
     Ab<-U3(ub)]
By definition of C(c'), Ab does not appear free in C(c').
For Asa,Asu,Aa,Au, must show:
  D(d) |- [d](s&({} -o s''*true)) = [d]s:cap
  D(d) |- [d]{} = [d]s0:cap
  D(d) |- [d](a&(U3(ub) -o a''*true)&(U3(ub)*u'' -o (s&({} -o s''*true))*true)) = [d]a:cap
  D(d) |- [d]U3(ub)*u'' = [d]u:cap

D(d) |- [d]{} = [d]s0:cap follows from lang1 and lang2 lemmas:
 -- if d |- c:cap then D(d) |- S(c):cap+
 -- if |- d and d |- c:cap+ then D(d) |- [d]U2(c)={}:cap~

For other cases, use lemma -3:
By lemma -3, D(d) |- [d]C(c)<=[d]C(c'')
 and D(d) |- [d]U3(U2(C1(c)))=[d]U3(ub+U2(C1(c''))):cap
 and D(d) |- [d]U3(ub)*[d]A3(A2(C1(c)))*true<=[d]A3(A2(C1(c'')))*true
so D(d) |- [d]u*[d]a*true<=[d]u''*[d]a''*true
 and D(d) |- [d]u=[d]U3(ub)*[d]u'':cap
 and D(d) |- [d]U3(ub)*[d]a*true<=[d]a''*true
so
 [d]U3(ub)*[d]a*true |- [d]a''*true
By lang0 rule, d |- /c <= /c''
By lemma -3:
  D(d) |- [d]C(/c)<=[d]C(/c'')
  D(d) |- [d](U3(U2(S1(c)))*A3(A2(S1(c)))*true)<=[d](U3(U2(S1(c'')))*A3(A2(S1(c'')))*true)
  D(d) |- [d]s0*[d]s*true<=[d]s0''*[d]s''*true
so
  [d]s0*[d]s*true |- [d]s0''*[d]s''*true
since D(d) |- [d]{} = [d]s0:cap, this simplifies to:
  [d]s*true |- [d]s0''*[d]s''*true
combine the [d]s0'' into the true:
  [d]s*true |- [d]s''*true
By lang0 rule, d |- c <= /c
By lemma -3:
  D(d) |- [d]C(c)<=[d]C(/c)
  D(d) |- [d](U3(U2(C1(c)))*A3(A2(C1(c)))*true)<=[d](U3(U2(S1(c)))*A3(A2(S1(c)))*true)
  D(d) |- [d]u*[d]a*true <= [d]s0*[d]s*true
so
  [d]u*[d]a*true |- [d]s0*[d]s*true
combine the [d]s0 into the true:
  [d]u*[d]a*true |- [d]s*true

Derivations for D(d) |- [d](s&({} -o s''*true)) = [d]s:cap

[d]s |- [d]s
----------------------------------
[d]s & ({} -o [d]s''*true) |- [d]s


                [d]s |- [d]s*true    [d]s*true |- [d]s''*true
                --------------------------------------------- cut
                [d]s |- [d]s''*true
                -------------------------
[d]s |- [d]s    [d]s |- {} -o [d]s''*true
-----------------------------------------
[d]s |- [d]s&({} -o [d]s''*true)

Derivations for D(d) |- [d](a&(U3(ub) -o a''*true)&(U3(ub)*u'' -o (s&({} -o s''*true))*true)) = [d]a:cap

[d]a |- [d]a
---------------------------------------------------------------------------------------------
[d]a&([d]U3(ub) -o [d]a''*true)&([d]U3(ub)*[d]u'' -o ([d]s&({} -o [d]s''*true))*true) |- [d]a

                                                                                                                                      proved above
                                                                                                                                      --------------------------------
                                                                                                                                      [d]s |- [d]s&({} -o [d]s''*true)
                                                                                                                                      --------------------------------------------
                                                                        d[a],[d]u |- d[a]*[d]u*true    d[a]*[d]u*true |- [d]s*true    [d]s*true |- ([d]s&({} -o [d]s''*true))*true
                                                                        ---------------------------------------------------------------------------------------------------------- cut(twice)
                                                [d]U3(ub)*[d]u'' |- [d]u    d[a],[d]u |- ([d]s&({} -o [d]s''*true))*true
                                                ------------------------------------------------------------------------ cut
                d[a],[d]U3(ub) |- [d]a''*true       d[a],[d]U3(ub)*[d]u'' |- ([d]s&({} -o [d]s''*true))*true
                --------------------------------    -----------------------------------------------------------
                d[a] |- [d]U3(ub) -o [d]a''*true    d[a] |- [d]U3(ub)*[d]u'' -o ([d]s&({} -o [d]s''*true))*true
                -----------------------------------------------------------------------------------------------
[d]a |- [d]a    d[a] |- ([d]U3(ub) -o [d]a''*true)&([d]U3(ub)*[d]u'' -o ([d]s&({} -o [d]s''*true))*true)
--------------------------------------------------------------------------------------------------------
[d]a |- [d]a&([d]U3(ub) -o [d]a''*true)&([d]U3(ub)*[d]u'' -o ([d]s&({} -o [d]s''*true))*true)



CASE:

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

By induction, Z(z);D(d);[d]G(g) |- [d]v':[d]T(t')
By lemma, D(d) |- [d]T(t1')=[d]T(t2'):type

Z(z);D(d);[d]G(g) |- [d]v':[d]T(t')
D(d) |- [d]T(t1')=[d]T(t2'):type
-----------------------------------
Z(z);D(d);[d]G(g) |- [d]v': [d]T(t)


CASE:

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

similar to v~~>v' case above


CASE:

d |- d'
d,d' |- c:cap
d,d' |- t1:type
...
d,d' |- tn:type
d |- r:res
z;d,d';g,x:tx,x1:t1...xn:tn;c |- e ~~> e'
tx = all[d'](c,t1...tn)->0 at r
--------------------------------------------- (x,x1...xn not in dom(g))
z;d;g |- fix x[d'](c,x1:t1...xn:tn).e at r:tx ~~> fix x[D(d')](C(c),x1:T(t1)...xn:T(tn)).e' at r

T(tx) = all[D(d')]([d']C(c),[d']T(t1)...[d']T(tn))->0 at r
[d']T(tx) = T(tx)

By induction:
  Z(z);D(d,d');[d,d']G(g),x:[d,d']T(tx),x1:[d,d']T(t1)...xn:[d,d']T(tn);[d,d']C(c) |- e'
  Z(z);D(d,d');[d][d']G(g),x:[d][d']T(tx),x1:[d][d']T(t1)...xn:[d][d']T(tn);[d][d']C(c) |- e'
  Z(z);D(d,d');[d][d']G(g),x:[d]T(tx),x1:[d][d']T(t1)...xn:[d][d']T(tn);[d][d']C(c) |- e'
By lemmas:
  D(d,d') |- [d,d']C(c):cap
  D(d,d') |- [d,d']T(t1):type
  ...
  D(d,d') |- [d,d']T(tn):type
  D(d) |- r:res

D(d,d')
  = D3(D2(D1(d,d')))
  = D3(D2(D1(d),D1(d')))
  = D3(D2(D1(d)),[D1(d)]2 D2(D1(d')))
  = D3(D2(D1(d))), [D2(D1(d))]3 D3([D1(d)]2 D2(D1(d')))
  = D3(D2(D1(d))), [D2(D1(d))]3 U3([D1(d)]2) D3(D2(D1(d')))
  = D(d), [d]D(d')

d |- d' implies that d,d' contains no duplicate variable bindings, so D(d) |- [d]D(d') must hold.
d |- d' and d |- g imply that [d']G(g) = G(g)


D(d) |- [d]D(d')
D(d),[d]D(d') |- [d][d']C(c):cap
D(d),[d]D(d') |- [d][d']T(t1):type
...
D(d),[d]D(d') |- [d][d']T(tn):type
D(d) |- r:res
Z(z);D(d),[d]D(d');[d]G(g),x:tx',x1:[d][d']T(t1)...xn:[d][d']T(tn);[d][d']C(c) |- e'
tx' = all[[d]D(d')][d][d'](C(c),T(t1)...T(tn))->0 at r
----------------------------------------------------------------------------------------
Z(z);D(d);[d]G(g) |- [d](fix x[D(d')]([d']C(c),x1:[d']T(t1)...xn:[d']T(tn)).e' at r):tx'

[d]T(tx)
  = [d]all[D(d')]([d']C(c),[d']T(t1)...[d']T(tn))->0 at r
  = all[[d]D(d')][d][d'](C(c),T(t1)...T(tn))->0 at r
  = tx'


EASY CASE:

From langccl:
  keep z;d;g |- <v1...vn> at r:<t1...tn> at r


EASY CASES:

From langccl:
  keep z;d;g;c |- x=v ==> d;g,x:t;c
  keep z;d;g;c |- x=v1 op v2 ==> d;g,x:int;c


CASE:

z;d;g |- v:r handle ~~> v'
z;d;g |- h at r:t ~~> h'
d |- c<=c'+{r+}
--------------------------------- (x not in dom(g))
z;d;g;c |- x=h at v ==> d;g,x:t;c ~~> x=h' at v'

By induction, Z(z);D(d);[d]G(g) |- [d]v':r handle
By induction, Z(z);D(d);[d]G(g) |- [d]h' at r:[d]T(t)
By lemma -5, D(d) |- [d]C(c)<={r}*true

Z(z);D(d);[d]G(g) |- [d]v':r handle
Z(z);D(d);[d]G(g) |- [d]h' at r:[d]T(t)
D(d) |- [d]C(c) <= {r}*true
-------------------------------------------------------------------------------- (x not in dom(g))
Z(z);D(d);[d]G(g);[d]C(c) |- x=[d]h' at [d]v' ==> D(d);[d]G(g),x:[d]T(t);[d]C(c)


CASE:

z;d;g |- v:<t0...tm-1> at r ~~> v'
d |- c<=c'+{r+}
------------------------------ (x not in dom(g) and 0<=n<m)
z;d;g;c |- x=v.n ==> d;g,x:tm;c ~~> x=v'.n

z;d;g |- v:<t0...tm-1> at r
d |- c <= {r}*true
------------------------------ (x not in dom(g) and 0<=n<m)
z;d;g;c |- x=v.n ==> d;g,x:tm;c

Similar to x=h at v case.


CASE:

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

By lemma -4, d |- c+{A~}=c+{A~}:cap implies D(d) |- [d]C(c+{A~})=([d]C(c))*{A}:cap

D(d) |- ([d]C(c))*{A} = [d]C(c+{A~}):cap
--------------------------------------------------------------------------------------(A not in dom(d) and x not in dom(g))
Z(z);D(d);[d]G(g);[d]C(c) |- newrgn A,x ==> D(d),A:res;[d]G(g),x:A handle;[d]C(c+{A~})


CASE:

z;d;g |- v: r handle ~~> v'
d |- c = c'+{r~}:cap
-------------------------------
z;d;g;c |- freergn v ==> d;g;c' ~~> freergn v'

By induction, Z(z);D(d);[d]G(g) |- [d]v':[d]T(r handle)
By lemma -4, D(d) |- [d]C(c)=([d]C(c'))*{r}:cap

Z(z);D(d);[d]G(g) |- [d]v':r handle
D(d) |- [d]C(c)=([d]C(c'))*{r}:cap
--------------------------------------------------------------------
Z(z);D(d);[d]G(g);[d]C(c) |- freergn [d]v' ==> D(d);[d]G(g);[d]C(c')


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

By induction, Z(z);D(d);[d]G(g);[d]C(c) |- [d]l'==>D(d');[d]G(g');[d]C(c') and [d]=[d']
By induction, Z(z);D(d');[d']G(g');[d']C(c') |- [d']e'

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


EASY CASE:

From langccl:
  keep z;d;g;c |- if0 v then e2 else e3


CASE:

z;d;g |- v: all[](c',t1...tn)->0 at r ~~> v'
z;d;g |- v1: t1 ~~> v1'
...
z;d;g |- vn: tn ~~> vn'
d |- c<=c''+{r+}
d |- c <= c'
---------------------
z;d;g;c |- v(v1...vn) ~~> v'(v1'...vn')

By induction, Z(z);D(d);[d]G(g) |- [d]v':[d]T(all[](c',t1...tn)->0 at r)
By induction, Z(z);D(d);[d]G(g) |- [d]vk':[d]T(tk)
By lemma -5, D(d) |- [d]C(c)<={r}*true
By lemma -3, If |- d and d |- c<=c' then D(d) |- [d]C(c)<=[d]C(c')

T(all[](c',t1...tn)->0 at r) = all[](C(c'),T(t1)...T(tn))->0 at r

Z(z);D(d);[d]G(g) |- [d]v':[d]all[](C(c'),T(t1)...T(tn))->0 at r
Z(z);D(d);[d]G(g) |- [d]v1':[d]T(t1)
...
Z(z);D(d);[d]G(g) |- [d]vn':[d]T(tn)
D(d) |- [d]C(c)<={r}*true
D(d) |- [d]C(c)<=[d]C(c')
------------------------------------------
Z(z);D(d);[d]G(g);[d]C(c) |- v'(v1'...vn')


CASE:

z;d;g |- v:int ~~> v'
d |- c = {}:cap
-----------------
z;d;g;c |- halt v ~~> halt v'

By induction, Z(z);D(d);[d]G(g) |- [d]v':[d]T(int)

Z(z);D(d);[d]G(g) |- [d]v':int
---------------------------------------
Z(z);D(d);[d]G(g);[d]C(c) |- halt [d]v'


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

 -- if |-z and |- m:z~~>m' and z sat c and z;;;c |- e~~>e'
     then |- m':Z(z) and Z(z) sat C(c) and Z(z);;;C(c) |- e'

|- m:z implies that for each q in dom(m), for each i in dom(m(q)):
  z;; |- m(q.i) at q:z(q.i)
By the translation lemma for h at r:
  Z(z);; |- H(m(q.i) at q):T(z(q.i))
so
  Z(z);; |- m'(q.i) at q:Z(z)(q.i)
Therefore |- m':Z(z)

z sat c implies:
  |- c={q1 p1}+...+{qn pn}:cap
  where all qk are distinct
  and dom(z) = {q1,...,qn}
define c' = {q1~}+...+{qn~}
C(c')
  = U3(U2(C1(c')))*A3(A2(C1(c')))*true
  = U3(U2({q1~}+...+{qn~}))
   *A3(A2({q1~}+...+{qn~}))*true
  = U3({q1~}+...+{qn~})
   *A3({}+...+{})*true
  = {q1}*...*{qn}
   *A3({}+...+{})*true
by definition of sat and A3:
  {q1},...,{qn} sat {q1}*...*{qn}
  {} sat A3({}+...+{})
  {} sat true
and dom(Z(z))=dom(z) = {q1,...,qn}, so
  Z(z) sat C(c')
by rules:
  |- c' <= c
by lemma:
  |- C(c') <= C(c)
so:  
  C(c') |- C(c)
by sat preservation:
  Z(z) sat C(c)


By the translation lemma for e:
  Z(z);;;C(c) |- e'


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

Lemma 28:

- if |- (M,e) and q appears nowhere in (M,e) then there is a derivation of |- (M,e)
  that never mentions q

(Note that lemma 28 as stated in WCM-TR does not hold for CC/SLL.
Since d |- c = c*({q} -o {q}):cap for any q, for many t it is possible
to construct a d |- t=t':type such that t' contains an arbitrary q.)

Proof:
Pick a q' that appears nowhere in the given derivation of |- (M,e).
Substitute q' for q everywhere in |- (M,e).
This generates a valid derivation of |- (M,e) that does not mention q' (easy induction).

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

Lemma 29:

If |- m:z and z;{};{} |- v:t then

1. If t=int then v=n
2. If t=q handle then v=handle(q)
3. If t=all[d](C,t1...tn)->0 at q then v=q.i[c1...cm] and either q not in domain(z) or:
  (b),(c),(d),(e) from WCM-TR (without 
4. If t=<t1...tn> at r then v=q.i and either q not in domain(z) or:
  (b),(c) from WCM-TR

Proof follows WCM-TR

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

Lemma 34:

- If z sat c and |- c=c':cap then z sat c'
By definition of |- c=c':cap conclude c |- c'
Then use lemma above (sat preservation).

- If z sat c and |- c<=c' then z sat c'
By definition of |- c<=c':cap conclude c |- c'
Then use lemma above (sat preservation).

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

Lemma 35:

If z sat c*{q} then z\q sat c

By inversion, z=z1,z2 where:
  z1 sat c
  z2 sat {q}
  ---------------
  z1,z2 sat c*{q}
Since z1=z\{q}, z\q sat c

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

Lemma 36 (preservation):

CASES THAT DIRECTLY FOLLOW WCM-TR:

let v

let h

v.n

freergn (note the role of the new version of Lemma 35)

if0

v0(v1,...,vn)


CASE newrgn:

We are given a q that does not appear in (M,e).
By lemma 28, there is a derivation |- (M,e) that does not mention q; use this derivation
(so that we can invoke the memory extension lemma).

1,3 follow WCM-TR.
2. z sat c.  Since q not in domain(z), z'=z,{q:{}} is well-formed.  Therefore, z' sat c*{q}.
   Since d |- c*{q}=c':cap, we know c*{q} |- c'.  By sat preservation, z' sat c'.

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

Lemma 37 (progress):

CASES THAT DIRECTLY FOLLOW WCM-TR:

let v

let h
(z sat {q}*true implies that for some y and z', z={q:y},z', so q in domain(z))

v.n
(z sat {q}*true implies that for some y and z', z={q:y},z', so q in domain(z))

newrgn

freergn
(z sat c'*{q} implies that for some y and z', z=z',{q:y}, so q in domain(z))

if0

v0(v1,...,vn)
(z sat {q}*true implies that for some y and z', z={q:y},z', so q in domain(z))

halt

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