---

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

∀[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[P:Id ─→ Info List+ ─→ ℙ].
  ∀eo1,eo2,eo:EO+(Info). ∀f:E ─→ E. ∀g:E ─→ E.
    (es-weak-joint-embedding(Info;eo1;eo2;eo;f;g)
    ⇒ (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo1)
    ⇒ (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo2)
    ⇒ (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo))
BY
{ (RepeatFor 9 (Intro)
   THEN InstLemma `squash-causal-invariant_wf` [⌈Info⌉;⌈R⌉;⌈P⌉]⋅
   THEN Auto
   THEN Thin (-3)
   THEN All (RepUR ``squash-causal-invariant es-weak-joint-embedding``)⋅
   THEN Auto
   THEN (With ⌈e⌉ (D (-6))⋅ THENA Auto)
   THEN D -1
   THEN ExRepD) }

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. e1 : E@i
17. e = (f e1) ∈ E@i
⊢ ↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e))

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
⊢ ↓∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo;e';e))

---

Latex:


\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}eo1,eo2,eo:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.  \mforall{}g:E  {}\mrightarrow{}  E.
        (es-weak-joint-embedding(Info;eo1;eo2;eo;f;g)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo1)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo2)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo))


By

(RepeatFor  9  (Intro)
  THEN  InstLemma  `squash-causal-invariant\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Thin  (-3)
  THEN  All  (RepUR  ``squash-causal-invariant  es-weak-joint-embedding``)\mcdot{}
  THEN  Auto
  THEN  (With  \mkleeneopen{}e\mkleeneclose{}  (D  (-6))\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index