Step
*
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
⊢ ↓∃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
THEN (InstLemma `embedding-preserves-local-property` [⌈Info⌉;⌈P⌉;⌈eo2⌉;⌈eo⌉;⌈g⌉;⌈e2⌉]⋅ THENA Auto)
THEN BHyp -1
THEN Auto
THEN RevHypSubst' (-3) 0
THEN Auto)
)
THEN SqExRepD
) }
1
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)
⊢ ↓∃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
\mvdash{} \mdownarrow{}\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
THEN (InstLemma `embedding-preserves-local-property` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}eo2\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN BHyp -1
THEN Auto
THEN RevHypSubst' (-3) 0
THEN Auto)
)
THEN SqExRepD
)
Home
Index