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