---

Step * of Lemma joint-embedding-preserves-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-joint-embedding(Info;eo1;eo2;eo;f;g)
    ⇒ (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo1)
    ⇒ (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo2)
    ⇒ (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo))
BY
{ (RepeatFor 9 (Intro)
   THEN InstLemma `causal-invariant_wf` [⌈Info⌉;⌈R⌉;⌈P⌉]⋅
   THEN Auto
   THEN Thin (-3)
   THEN All (RepUR ``causal-invariant es-joint-embedding``)⋅
   THEN Auto
   THEN (With ⌈e⌉ (D (-5))⋅ 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. (g embeds eo2 into eo)@i
11. ∀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
12. ∀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
13. e : E@i
14. es-local-property(i,L.P[i;L];eo;e)@i
15. e1 : E@i
16. 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. (g embeds eo2 into eo)@i
11. ∀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
12. ∀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
13. e : E@i
14. es-local-property(i,L.P[i;L];eo;e)@i
15. e2 : E@i
16. 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-joint-embedding(Info;eo1;eo2;eo;f;g)
        {}\mRightarrow{}  (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo1)
        {}\mRightarrow{}  (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo2)
        {}\mRightarrow{}  (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo))


By

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

---

Home Index