Proof of Nuprl Lemma : weak-joint-embedding-preserves-squash-causal-invariant

Step * 2 1 2 of Lemma weak-joint-embedding-preserves-squash-causal-invariant

1. Info : Type
2. R : Id ─→ Id ─→ Info List⁺ ─→ Info List⁺ ─→ ℙ
3. P : Id ─→ Info List⁺ ─→ ℙ
4. eo1 : EO+(Info)@i'
5. eo2 : EO+(Info)@i'
6. eo : EO+(Info)@i'
7. f : E ─→ E@i
8. g : E ─→ E@i
9. (f embeds eo1 into eo)@i
10. es-local-embedding(Info;eo2;eo;g)@i
11. ∀x,y:E.  ((x < y) ⇒ ((g x < g y) ∨ (∃z:E. ((g y) = (f z) ∈ E))))@i
12. ∀e:E
      (es-local-property(i,L.P[i;L];eo1;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e';e))))@i
13. ∀e:E
      (es-local-property(i,L.P[i;L];eo2;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e))))@i
14. e : E@i
15. es-local-property(i,L.P[i;L];eo;e)@i
16. e2 : E@i
17. e = (g e2) ∈ E@i
18. e' : E
19. (e' < e2)
20. es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e2)
21. ∃z:E. ((g e2) = (f z) ∈ E)
⊢ ↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e))
BY
{ (ExRepD THEN (Assert e = (f z) ∈ E BY Eq) THEN (InstHyp [⌈z⌉] 12⋅ THENA Auto)) }

1
.....antecedent.....
1. Info : Type
2. R : Id ─→ Id ─→ Info List⁺ ─→ Info List⁺ ─→ ℙ
3. P : Id ─→ Info List⁺ ─→ ℙ
4. eo1 : EO+(Info)@i'
5. eo2 : EO+(Info)@i'
6. eo : EO+(Info)@i'
7. f : E ─→ E@i
8. g : E ─→ E@i
9. (f embeds eo1 into eo)@i
10. es-local-embedding(Info;eo2;eo;g)@i
11. ∀x,y:E.  ((x < y) ⇒ ((g x < g y) ∨ (∃z:E. ((g y) = (f z) ∈ E))))@i
12. ∀e:E
      (es-local-property(i,L.P[i;L];eo1;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e';e))))@i
13. ∀e:E
      (es-local-property(i,L.P[i;L];eo2;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e))))@i
14. e : E@i
15. es-local-property(i,L.P[i;L];eo;e)@i
16. e2 : E@i
17. e = (g e2) ∈ E@i
18. e' : E
19. (e' < e2)
20. es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e2)
21. z : E
22. (g e2) = (f z) ∈ E
23. e = (f z) ∈ E
⊢ es-local-property(i,L.P[i;L];eo1;z)

2
1. Info : Type
2. R : Id ─→ Id ─→ Info List⁺ ─→ Info List⁺ ─→ ℙ
3. P : Id ─→ Info List⁺ ─→ ℙ
4. eo1 : EO+(Info)@i'
5. eo2 : EO+(Info)@i'
6. eo : EO+(Info)@i'
7. f : E ─→ E@i
8. g : E ─→ E@i
9. (f embeds eo1 into eo)@i
10. es-local-embedding(Info;eo2;eo;g)@i
11. ∀x,y:E.  ((x < y) ⇒ ((g x < g y) ∨ (∃z:E. ((g y) = (f z) ∈ E))))@i
12. ∀e:E
      (es-local-property(i,L.P[i;L];eo1;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e';e))))@i
13. ∀e:E
      (es-local-property(i,L.P[i;L];eo2;e)
      ⇒ (↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e))))@i
14. e : E@i
15. es-local-property(i,L.P[i;L];eo;e)@i
16. e2 : E@i
17. e = (g e2) ∈ E@i
18. e' : E
19. (e' < e2)
20. es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e2)
21. z : E
22. (g e2) = (f z) ∈ E
23. e = (f z) ∈ E
24. ↓∃e':E. ((e' < z) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e';z))
⊢ ↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e))

Latex:

1. Info : Type 2. R : Id {}\mrightarrow{} Id {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} \mBbbP{} 3. P : Id {}\mrightarrow{} Info List\msupplus{} {}\mrightarrow{} \mBbbP{} 4. eo1 : EO+(Info)@i' 5. eo2 : EO+(Info)@i' 6. eo : EO+(Info)@i' 7. f : E {}\mrightarrow{} E@i 8. g : E {}\mrightarrow{} E@i 9. (f embeds eo1 into eo)@i 10. es-local-embedding(Info;eo2;eo;g)@i 11. \mforall{}x,y:E. ((x < y) {}\mRightarrow{} ((g x < g y) \mvee{} (\mexists{}z:E. ((g y) = (f z)))))@i 12. \mforall{}e:E (es-local-property(i,L.P[i;L];eo1;e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e';e))))@i 13. \mforall{}e:E (es-local-property(i,L.P[i;L];eo2;e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e))))@i 14. e : E@i 15. es-local-property(i,L.P[i;L];eo;e)@i 16. e2 : E@i 17. e = (g e2)@i 18. e' : E 19. (e' < e2) 20. es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e2) 21. \mexists{}z:E. ((g e2) = (f z)) \mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e)) By (ExRepD THEN (Assert e = (f z) BY Eq) THEN (InstHyp [\mkleeneopen{}z\mkleeneclose{}] 12\mcdot{} THENA Auto)) Home Index