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

Step * 2 of Lemma weak-joint-embedding-preserves-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
⊢ ∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e))
BY
{ (InstHyp [⌈e2⌉] 13⋅ 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
⊢ es-local-property(i,L.P[i;L];eo2;e2)

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. ((e' < e2) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;e';e2))
⊢ ∃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{} (\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{} (\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 \mvdash{} \mexists{}e':E. ((e' < e) \mwedge{} es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e)) By (InstHyp [\mkleeneopen{}e2\mkleeneclose{}] 13\mcdot{} THENA Auto) Home Index