EXTENSIONS TO LANG3A:

c = ... | c1(+)c2 | !c
t = ... | !c=>t
v = ... | v[!]
h = ... | \!c.h
o = c1,...,ck,[!ck+1],...,[!cn]
[o] = [!c1],...,[!cn]

c1 x c2 = !(c1 * c2)
c1=>c2 = !(c1 -o c2)
c1<=>c2 = (c1=>c2) x (c2=>c1)
c1[+]c2 = !(c1(+)c2)

[o] |- {}

[o],c |- c

[o],[!c] |- c

o,[!c],[!c] |- c'
---------------
o,[!c] |- c'

o |- c'
-----------
o,[!c] |- c'

[o] |- c
---------
[o] |- !c

o,[!c] |- c'
-----------
o,!c |- c'

lemma:
o,c |- c'
-----------
o,[!c] |- c'

o |- c1
-----------
o |- c1(+)c2

o |- c2
-----------
o |- c1(+)c2

o,c1 |- c3
o,c2 |- c3
--------------
o,c1(+)c2 |- c3

In d;g |- v:t and d;g |- h:t rules, replace d;g with d;g;[o]
In d;g;c |- d ==> d';g';c' rules, replace d;g;c with d;g;[o];c
In d;g;c |- e rules, replace d;g;c with d;g;[o];c

d |- c1:k
d |- c2:k
[o],c1 |- c2
[o],c2 |- c1
--------------
d;[o] |- c1 = c2:k

d;g;[o] |- v:!c=>t
[o] |- !c
------------------
d;g;[o] |- v[!]:t

d |- c:cap
d;g;[o],[!c] |- h:t
----------------------
d;g;[o] |- \!c.h:!c=>t

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

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

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

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

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

CHANGES TO LANG3A TRANSLATION:

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

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

C(u#a) = U(u)*(A(a)*Z(a))
S(u1#a1<=a2) = (C(u1#a1)=>A(a2)*Z(a2)) x (U(u1)(+)Z(a1)=>Z(a2))

T(all A:cap+.t) = all A:cap.all Az:cap. ((A<=>{}) x (Az<=>{}) [+] (Az<=>true))=>T(t)
T(all A:cap+ where c1<=a1,...,cn<=an.t) =
  all A:cap. all Az:cap.
    (((A<=>{}) x (Az<=>{}) [+] (Az<=>true)) x S(c1<=a1) x ... x S(cn<=an))=>T(t)

D(A:cap+,d) = A:cap,Az:cap,D(d)
D(A:cap+ where c1<=a1,...,cn<=an.t,d) = A:cap,Az:cap,D(d)

[d] = []

O(.) = .
O(A:k,d) = O(d) where k != cap+
O(A:cap+,d) =
 [((A<=>{}) x (Az<=>{}) [+] (Az<=>true))],O(d)
O(A:cap+ where c1<=a1,...,cn<=an.t,d) =
 [((A<=>{}) x (Az<=>{}) [+] (Az<=>true)) x S(c1<=a1) x ... x S(cn<=an)],O(d)

V(v[a:cap+]) = V(v)[A(a):cap][Z(a):cap][!]

H(\A:cap+.h) = \A:cap.\Az:cap.\(((A<=>{}) x (Az<=>{})) [+] (Az<=>true)).H(h)
H(\A:cap+ where u1#A<=a1,...,un#A<=an.h) =
  \A:cap.\Az:cap.\((((A<=>{}) x (Az<=>{})) [+] (Az<=>true)) x S(c1<=a1) x ... x S(cn<=an)).H(h)

New or modified lemmas (complete proofs shown below):
  - if |- d and d |- a:cap+ then O(d) |- ((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true))
    corollaries:
    - O(d),Z(a) |- Z(a)*Z(a)
    - O(d),Z(a)*Z(a) |- Z(a)
    - O(d),A(a) |- Z(a)
    - O(d),A(a) |- A(a)*Z(a)
  - if |- d and d |- a1=a2 then D(d);O(d) |- Z(a1)=Z(a2):cap
  - if |- d and d |- a1=a2:cap+ then D(d);O(d) |- A(a1)*Z(a1)=A(a2)*Z(a2):cap and d |- a1:cap+ and d |- a2:cap+
  - if |- d and d |- u#a<=a' then O(d),U(u)(+)Z(a) |- Z(a') and d |- a:cap+ and d |- a':cap+
    corollaries:
    - O(d),U(u) |- Z(a')
    - O(d),Z(a) |- Z(a')
  - if |- d and d |- u#a<=a' then O(d),C(u#a) |- A(a')*Z(a') and d |- a1:cap+ and d |- a2:cap+

Other lemmas in lang3a remain the same, except:
  - [d] is now equal to [] and can be dropped
  - [A'<-A(a')] substitution turns into [A'<-A(a'),Az'<-Z(a')]:
    - if |- d and d |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A(a'),Az'<-Z(a')]A(a)
    - if |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'',Az'<-az'']U(u) for any a'',az''
    - if |- d and d |- A':cap+ and d |- t:type then T([A'<-a']t) = [A'<-A(a'),Az'<-Z(a')]T(t)
  - For each A([...]A) substitution lemma, there is a Z([...]A) lemma:
    - if |- d and d |- A':cap+ and d |- a:cap+ then Z([A'<-a']a) = [A'<-A(a'),Az<-Z(a')]Z(a)
    - if |- d and d |- A':cap~ and d |- a:cap+ then Z([A'<-u']a) = [A'<-u'']Z(a) for any u''
  - The v,h,l,e lemmas have O(d) in the judgments:
    - if d;g |- v:t then D(d);G(g);O(d) |- V(v):T(t)
    - if d;g |- h:t then D(d);G(g);O(d) |- H(h):T(t)
    - if d;g;c |- l==>d';g';c' then D(d);G(g);O(d);C(c) |- L(l)==>D(d');G(g');O(d');C(c')
    - if d;g;c |- e then D(d);G(g);O(d);C(c) |- E(e)
Rather than rewrite the proofs for these lemmas,
it's easier just to scan through lang3a's existing proofs,
with the above updates in mind.  The interesting cases are:

===

lang3a lemma:
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''
...
A([A'<-a']A') = A(a')
[A'<-A(a')]A(A') = [A'<-A(a')]A' = A(a')

lang4a revision:
If |- d and d |- A':cap+ and d |- a:cap+ then A([A'<-a']a) = [A'<-A(a'),Az'<-Z(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''
If |- d and d |- A':cap+ and d |- a:cap+ then Z([A'<-a']a) = [A'<-A(a'),Az<-Z(a')]Z(a)
If |- d and d |- A':cap~ and d |- a:cap+ then Z([A'<-u']a) = [A'<-u'']Z(a) for any u''
...
A([A'<-a']A') = A(a')
[A'<-A(a'),Az'<-Z(a')]A(A') = [A'<-A(a'),Az'<-Z(a')]A' = A(a')

Z([A'<-a']A') = Z(a')
[A'<-A(a'),Az'<-Z(a')]Z(A') = [A'<-A(a'),Az'<-Z(a')]Az' = Z(a')

===

lang3a lemma:
If |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'']U(u) for any a''
...
Impossible case: d |- A':cap+ and d |- A':cap~ cannot both be true

lang4a revision:
If |- d and d |- A':cap+ and d |- u:cap~ then U([A'<-a']u) = [A'<-a'',Az'<-az'']U(u) for any a'',az''
...
Impossible case: d |- A':cap+ and d |- A':cap~ cannot both be true

===

lang3a lemmas for v,h,l,e:

CASE:

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

Induction: D(d,A:cap+);G(g);O(d,A:cap+) |- H(h):T(t)
           D(d),A:cap,Az:cap;G(g);O(d),[((A<=>{}) x (Az<=>{}) [+] (Az<=>true))] |- H(h):T(t)
           ----------------------------------------------------------------------------------
           D(d),A:cap,Az:cap;G(g);O(d) |- \(((A<=>{}) x (Az<=>{}) [+] (Az<=>true))).H(h):T(t)
           -----------------------------------------------------------------------------------
           D(d),A:cap;G(g);O(d) |- \Az:cap.\(((A<=>{}) x (Az<=>{}) [+] (Az<=>true))).H(h):T(t)
           ------------------------------------------------------------------------------------
           D(d);G(g);O(d) |- \A:cap.\Az:cap.\(((A<=>{}) x (Az<=>{}) [+] (Az<=>true))).H(h):T(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

similar to previous case


CASE:

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

lemma: O(d) |- ((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true))

Induction: D(d);G(g);O(d) |- V(v):T(all A':cap+.t')
           D(d);G(g);O(d) |- V(v):all A':cap.all Az':cap. ((A'<=>{}) x (Az'<=>{}) [+] (Az'<=>true))=>T(t')
           ----------------------------------------------------------------------------------------------------------
           D(d);G(g);O(d) |- V(v)[A(a):cap]:all Az':cap. ((A(a)<=>{}) x (Az'<=>{}) [+] (Az'<=>true))=>[A'<-A(a)]T(t')
           -------------------------------------------------------------------------------------------------------------------
           D(d);G(g);O(d) |- V(v)[A(a):cap][Z(a):cap]:((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true))=>[A'<-A(a),Az'<-Z(a)]T(t')
           -------------------------------------------------------------------------------------------------------------------
           D(d);G(g);O(d) |- V(v)[A(a):cap][Z(a):cap][!]:[A'<-A(a),Az'<-Z(a)]T(t')

lemma: T([A'<-a]t') = [A'<-A(a),Az'<-Z(a)]T(t')


CASE:

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

similar to previous case
(use lemmas:
  if |- d and d |- a:cap+ then O(d) |- ((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true))
  if |- d and d |- u#a<=a' then O(d),C(u#a) |- A(a')*Z(a')
  if |- d and d |- u#a<=a' then O(d),U(u)(+)Z(a) |- Z(a')
to show:
  O(d) |- (((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true)) x S(c1<=a1) x ... x S(cn<=an))
where:
  S(u1#a1<=a2) = (C(u1#a1)=>A(a2)*Z(a2)) x (U(u1)(+)Z(a1)=>Z(a2))
)


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

(see lang3a case)

C(u#a) = U(u)*(A(a)*Z(a))
C(u+{A~}#a) = (U(u)*{A})*(A(a)*Z(a))

(U(u)*(A(a)*Z(a)))*{A} |- (U(u)*{A})*(A(a)*Z(a))


CASE:

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

(see lang3a case)

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


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

(see lang3a case)

O(d),U(u2),Z(a')*true,Z(a'),true |- true
------------------------------------------------
O(d),U(u2),{A}*Z(a')*true,Z(a'),true |- {A}*true
-----------------------------------------------------------------------
O(d),U(u2),(A(a')*Z(a')*true) & ({A}*Z(a')*true)*Z(a')*true |- {A}*true
----------------------------------------------------------------------- lemma: U(u1)*A(a)*Z(a) |- (A(a')*Z(a')*true) & ({A}*Z(a')*true)*Z(a')*true
O(d),U(u1)*U(u2)*A(a)*Z(a) |- {A}*true
-------------------------------------- lemma: U(u) |- U(u1)*U(u2)
O(d),U(u)*A(a)*Z(a) |- {A}*true


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

(see lang3a case)

----------------------------------------------- lemma: U(ub)*A(a)*Z(a) |- A(a')*Z(a')
O(d),U(ub)*U(u')*A(a)*Z(a) |- U(u')*A(a')*Z(a')
----------------------------------------------- lemma: U(u) |- U(ub)*U(u')
O(d),U(u)*A(a)*Z(a) |- U(u')*A(a')*Z(a')


CASE:

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

O(d),{}*{}*{} |- {}
------------------------- lemmas: U(u) |- {} and A(a)*Z(z) |- {}*{}
O(d),U(u)*A(a)*Z(z) |- {}

O(d),{} |- {}*{}*{}
------------------------- lemmas: {} |- U(u) and {}*{} |- A(a)*Z(z)
O(d),{} |- U(u)*A(a)*Z(z)


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

If |- d and d |- a:cap+ then O(d) |- ((A(a)<=>{}) x (Z(a)<=>{}) [+] (Z(a)<=>true))

Abbreviations: U1 = U(u1), A1 = A(a1), Z1 = Z(a1), etc.
Elide nonlinear assumptions for conciseness.

CASES:

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

[((A<=>{}) x (Az<=>{}) [+] (Az<=>true))] |- ((A<=>{}) x (Az<=>{}) [+] (Az<=>true))



CASE:

d |- {}:cap+

|- ({}<=>{}) x ({}<=>{})
----------------------------------------
|- ({}<=>{}) x ({}<=>{}) [+] ({}<=>true)


CASE:

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

|- true<=>true
---------------------------------------------
|- ({A}<=>{}) x (true<=>{}) [+] (true<=>true)


CASE:

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

(note:
  true |- true*true
  true*true |- true
  {}*{} |- {}
  {} |- {}*{}
)


A1<=>{},Z1<=>{},A2<=>{},Z2<=>{} |- ({}*{}*{}) & ({}*{}*{})<=>{}
----------------------------------------------------------------
A1<=>{},Z1<=>{},A2<=>{},Z2<=>{} |- (A1*Z1*Z2) & (A2*Z1*Z2)<=>{}
---------------------------------------------------------------------------------
A1<=>{},Z1<=>{},A2<=>{},Z2<=>{} |- ((A1*Z1*Z2) & (A2*Z1*Z2)<=>{}) x (Z1*Z2<=>{})
--------------------------------------------------------------------------------------------------------------------------------------- CASE left1,left2

A2<=>{}, Z2<=>{}, Z1<=>true |- Z1*Z2<=>true
--------------------------------------------------------------------------------------------------------------------------------------- CASE right1,left2

A1<=>{}, Z1<=>{}, Z2<=>true |- Z1*Z2<=>true
--------------------------------------------------------------------------------------------------------------------------------------- CASE left1,right2

Z1<=>true, Z2<=>true |- Z1*Z2<=>true
--------------------------------------------------------------------------------------------------------------------------------------- CASE right1,right2
(A1<=>{}) x (Z1<=>{}) [+] (Z1<=>true), (A2<=>{}) x (Z2<=>{}) [+] (Z2<=>true) |- ((A1*Z1*Z2) & (A2*Z1*Z2)<=>{}) x (Z1*Z2<=>{}) [+] (Z1*Z2<=>true))
----------------------------------------------------------------------------------------------------------------------------------------- cut (induction)
... |- ((A1*Z1*Z2) & (A2*Z1*Z2)<=>{}) x (Z1*Z2<=>{}) [+] (Z1*Z2<=>true))


Corollary: O(d),Z(a) |- Z(a)*Z(a)

true |- true*true
----------- case lemma right: Z1<=>true

{} |- {}*{}
----------- case lemma left: (A1<=>{}) x (Z1<=>{})
Z1 |- Z1*Z1


Corollary: O(d),Z(a)*Z(a) |- Z(a)

true*true |- true
----------- case lemma right: Z1<=>true

{}*{} |- {}
----------- case lemma left: (A1<=>{}) x (Z1<=>{})
Z1*Z1 |- Z1


Corollary: O(d),A(a) |- Z(a)

A1 |- true
---------- case lemma right: Z1<=>true

{} |- {}
---------- case lemma left: (A1<=>{}) x (Z1<=>{})
A1 |- Z1


Corollary: O(d),A(a) |- A(a)*Z(a)

|- true
-------------
A1 |- A1*true
------------- case lemma right: Z1<=>true

{} |- {}*{}
------------- case lemma left: (A1<=>{}) x (Z1<=>{})
A1 |- A1*Z1


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

If |- d and d |- a1=a2 then D(d);O(d) |- Z(a1)=Z(a2):cap

Abbreviations: U1 = U(u1), A1 = A(a1), Z1 = Z(a1), etc.
Elide nonlinear assumptions for conciseness.

EASY CASES:

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

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

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



CASE:

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

Z(a1) |- Z(a1')    Z(a2) |- Z(a2')
----------------------------------
Z(a1)*Z(a2) |- Z(a1')*Z(a2')


CASE:

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

{},Z(a1) |- Z(a1)
-----------------
{}*Z(a1) |- Z(a1)

|- {}    Z(a1) |- Z(a1)
-----------------------
Z(a1) |- {}*Z(a1)


EASY CASES:

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

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


CASE:

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

true*true |- true
----------------- case lemma right: Z1<=>true

{}*{} |- {}
----------- case lemma left: (A1<=>{}) x (Z1<=>{})
Z1*Z1 |- Z1


true |- true*true
----------------- case lemma right: Z1<=>true

{} |- {}*{}
----------- case lemma left: (A1<=>{}) x (Z1<=>{})
Z1 |- Z1*Z1


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

If |- d and d |- a1=a2:cap+ then D(d);O(d) |- A(a1)*Z(a1)=A(a2)*Z(a2):cap and d |- a1:cap+ and d |- a2:cap+


Abbreviations: U1 = U(u1), A1 = A(a1), Z1 = Z(a1), etc.
Elide nonlinear assumptions for conciseness.

EASY CASES:

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

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

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



CASE:

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

---------------- induction
A2*Z2 |- A2'*Z2'
--------------------------- lemma: Z1=Z1'
(A2*Z1*Z2) |- (A2'*Z1'*Z2')
-------------------------------------------------------- case right

---------------- induction
A1*Z1 |- A1'*Z1'
--------------------------- lemma: Z2=Z2'
(A1*Z1*Z2) |- (A1'*Z1'*Z2')
-------------------------------------------------------- case left
(A1*Z1*Z2) & (A2*Z1*Z2) |- (A1'*Z1'*Z2') & (A2'*Z1'*Z2')
-------------------------------------------------------------------------- lemma: Z1=Z1', Z2=Z2'
((A1*Z1*Z2) & (A2*Z1*Z2))*Z1*Z2 |- ((A1'*Z1'*Z2') & (A2'*Z1'*Z2'))*Z1'*Z2'

induction: d |- a1:cap+ and d |- a1':cap+
induction: d |- a2:cap+ and d |- a2':cap+


CASE:

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


A1*{}*Z1 |- A1*Z1
--------------------------------
({}*{}*Z1) & (A1*{}*Z1) |- A1*Z1
-------------------------------------------
(({}*{}*Z1) & (A1*{}*Z1))*{}*Z1 |- A1*Z1*Z1
------------------------------------------- lemma: Z1*Z1 |- Z1
(({}*{}*Z1) & (A1*{}*Z1))*{}*Z1 |- A1*Z1


-------------- lemma: A1 |- A1*Z1
A1 |- A1*{}*Z1
------------------------------- case right

-------------- lemma: A1 |- Z1
A1 |- {}*{}*Z1
------------------------------- case left
A1 |- (({}*{}*Z1) & (A1*{}*Z1))
----------------------------------------
A1*Z1 |- (({}*{}*Z1) & (A1*{}*Z1))*{}*Z1


EASY CASE:

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


CASE:

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



Z1*true |- true
---------------------------
A3*Z1*true*Z3 |- A3*true*Z3
------------------------------------------------------------------------------- case right

Z1,true,Z1,true |- true
-----------------------------------
A2*Z1*true,Z1,true,Z3 |- A2*true*Z3
--------------------------------------------------
(A1*Z1*true & A2*Z1*true)*Z1*true*Z3 |- A2*true*Z3
------------------------------------------------------------------------------- case left
(A1*Z1*true & A2*Z1*true)*Z1*true*Z3 & A3*Z1*true*Z3 |- A2*true*Z3 & A3*true*Z3
-------------------------------------------------------------------------------------------------------
(A1*Z1*true & A2*Z1*true)*Z1*true*Z3 & A3*Z1*true*Z3,Z1,true,Z3 |- (A2*true*Z3 & A3*true*Z3)*Z1*true*Z3
------------------------------------------------------------------------------------------------------- case lemma right: Z2<=>true

------------------------- lemmas: A3 |- Z3 and A3 |- A3*Z3
A3 |- {}*{}*Z3 & A3*{}*Z3
---------------------------------------------
A3,Z1,{},Z3 |- ({}*{}*Z3 & A3*{}*Z3)*Z1*{}*Z3
------------------------------------------------------ lemma: Zk*Zk |- Zk
A3*Z1*{}*Z3,Z1,{},Z3 |- ({}*{}*Z3 & A3*{}*Z3)*Z1*{}*Z3
---------------------------------------------------------------------------------------
(A1*Z1*{} & {}*Z1*{})*Z1*{}*Z3 & A3*Z1*{}*Z3,Z1,{},Z3 |- ({}*{}*Z3 & A3*{}*Z3)*Z1*{}*Z3
------------------------------------------------------------------------------------------------------- case lemma left: (A2<=>{}) x (Z2<=>{})
(A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2*Z3 & A3*Z1*Z2*Z3,Z1,Z2,Z3 |- (A2*Z2*Z3 & A3*Z2*Z3)*Z1*Z2*Z3
----------------------------------------------------------------------------------------------------- case right


A1,Z1,Z2,Z3 |- A1*Z1*Z2*Z3
----------------------------------------- lemma: Zk*Zk |- Zk
A1*Z1*Z2,Z1,Z2,Z3,Z1,Z2,Z3 |- A1*Z1*Z2*Z3
------------------------------------------------------
(A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2*Z3,Z1,Z2,Z3 |- A1*Z1*Z2*Z3
----------------------------------------------------------------------------------------------------- case left
(A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2*Z3 & A3*Z1*Z2*Z3,Z1,Z2,Z3 |- A1*Z1*Z2*Z3 & (A2*Z2*Z3 & A3*Z2*Z3)*Z1*Z2*Z3
---------------------------------------------------------------------------------------------------------------------------
((A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2*Z3 & A3*Z1*Z2*Z3)*Z1*Z2*Z3*Z1*Z2*Z3 |- (A1*Z1*Z2*Z3 & (A2*Z2*Z3 & A3*Z2*Z3)*Z1*Z2*Z3)*Z1*Z2*Z3
--------------------------------------------------------------------------------------------------------------------------- lemma: Zk |- Zk*Zk
((A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2*Z3 & A3*Z1*Z2*Z3)*Z1*Z2*Z3 |- (A1*Z1*Z2*Z3 & (A2*Z2*Z3 & A3*Z2*Z3)*Z1*Z2*Z3)*Z1*Z2*Z3


CASE:

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


A1*Z1*Z1 & A1*Z1*Z1 |- A1*Z1*Z1
---------------------------------------------
(A1*Z1*Z1 & A1*Z1*Z1)*Z1*Z1 |- A1*Z1*Z1*Z1*Z1
--------------------------------------------- lemma: Z1*Z1 |- Z1
(A1*Z1*Z1 & A1*Z1*Z1)*Z1*Z1 |- A1*Z1


A1*Z1*Z1 |- A1*Z1*Z1 & A1*Z1*Z1
---------------------------------------------
A1*Z1*Z1*Z1*Z1 |- (A1*Z1*Z1 & A1*Z1*Z1)*Z1*Z1
--------------------------------------------- lemma: Z1 |- Z1*Z1
A1*Z1 |- (A1*Z1*Z1 & A1*Z1*Z1)*Z1*Z1


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

If |- d and d |- u#a<=a' then O(d),U(u)(+)Z(a) |- Z(a') and d |- a:cap+ and d |- a':cap+

Abbreviations: U1 = U(u1), A1 = A(a1), Z1 = Z(a1), etc.
Elide nonlinear assumptions for conciseness.

CASE:

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

|- d implies d |- a2:cap+

O(d) = ...,[((A<=>{}) x (Az<=>{}) [+] (Az<=>true)) x ... x (U1(+)Z1=>Z2) x ...]

O(d),U1(+)Z1 |- Z2

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


CASE:

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

{A}(+){} |- true

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


CASE:

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

lemma: d |- a2:cap+

{} |- true
---------- case lemma right: Z2<=>true

{} |- {}
---------- case lemma left: (A2<=>{}) x (Z2<=>{})
{} |- Z2
------------- case left
{}(+)Z1 |- Z2

-------- lemma: Z1 |- Z2
Z1 |- Z2
------------- case right
{}(+)Z1 |- Z2

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


CASE:

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

induction: d |- a1:cap+ and d |- a2:cap+
induction: d |- a2:cap+ and d |- a3:cap+
(needed for Z3*Z3 |- Z3)

induction: U1(+)Z1 |- Z2
induction: U2(+)Z2 |- Z3

-------- lemma: Z2 |- Z3
Z2 |- Z3
-------- lemma: Z1 |- Z2
Z1 |- Z3
---------------- case right

----------- lemma: Z3*Z3 |- Z3
Z3,Z3 |- Z3
----------- induction: Z2 |- Z3
Z2,Z3 |- Z3
----------- induction: U2 |- Z3
Z2,U2 |- Z3
----------- induction: U1 |- Z2
U1*U2 |- Z3
---------------- case left
U1*U2(+)Z1 |- Z3


CASE:

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

induction: U1(+)Z1 |- Z1'
induction: U2(+)Z2 |- Z2'

---------------- induction: Z1 |- Z1' and Z2 |- Z2'
Z1*Z2 |- Z1'*Z2'
------------------------ case right

---------------- induction: U1 |- Z1' and U2 |- Z2'
U1*U2 |- Z1'*Z2'
------------------------ case left
U1*U2(+)Z1*Z2 |- Z1'*Z2'

induction: d |- a1:cap+ and d |- a1':cap+
induction: d |- a2:cap+ and d |- a2':cap+


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

If |- d and d |- u#a<=a' then O(d),C(u#a) |- A(a')*Z(a') and d |- a:cap+ and d |- a':cap+

Abbreviations: U1 = U(u1), A1 = A(a1), Z1 = Z(a1), etc.
Elide nonlinear assumptions for conciseness.

CASE:

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

O(d) = ...,[((A<=>{}) x (Az<=>{}) [+] (Az<=>true)) x ... x (U1*A*Az=>A2*Z2) x ...]

O(d),U1*A*Az |- A2*Z2

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


CASE:

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

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

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


CASE:

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

----------------- lemma: A1*Z1 |- A2*Z2
{}*A1*Z1 |- A2*Z2

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


CASE:

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

----------------- induction: U2*A2*Z2 |- A3*Z3
U2*A2*Z2 |- A3*Z3
-------------------- induction: U1*A1*Z1 |- A2*Z2
U1*U2*A1*Z1 |- A3*Z3

induction: d |- a1:cap+ and d |- a2:cap+
induction: d |- a2:cap+ and d |- a3:cap+


CASE:

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

induction: d |- a1:cap+ and d |- a1':cap+
induction: d |- a2:cap+ and d |- a2':cap+
(needed for Z2'*Z2' |- Z2')

-------------------------------------------------------- case right: symmetric to left case

------------------- induction: U1*A1*Z1 |- A1'*Z1'
U1,A1*Z1 |- A1'*Z1'
-------------------------- lemma: Z2 |- Z2'
U1,A1*Z1*Z2 |- A1'*Z1'*Z2'
--------------------------------- lemma: U2 |- Z2'
U1,U2,A1*Z1*Z2 |- A1'*Z1'*Z2'*Z2'
--------------------------------- lemma: Z2'*Z2' |- Z2'
U1,U2,A1*Z1*Z2 |- A1'*Z1'*Z2'
-------------------------------------------------------- case left
U1*U2*(A1*Z1*Z2 & A2*Z1*Z2) |- A1'*Z1'*Z2' & A2'*Z1'*Z2'
------------------------------------------------------------------------ lemma: Z1 |- Z1' and Z2 |- Z2'
U1*U2*(A1*Z1*Z2 & A2*Z1*Z2)*Z1*Z2 |- (A1'*Z1'*Z2' & A2'*Z1'*Z2')*Z1'*Z2'

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