---

Step * of Lemma global-order-compat-joint-embedding

∀[Info:Type]
  ∀L1,L2:(Id × Info) List.
    (L1 || L2
    ⇒ (∃L:(Id × Info) List
         ((∃f:E ⟶ E. ∃g:E ⟶ E. es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g))
         ∧ (∀L':(Id × Info) List. (L1 || L' ⇒ L2 || L' ⇒ L || L')))))
BY
{ (InstLemma `global-order-compat-combine` []⋅
   THEN (RepeatFor 4 (ParallelLast') THENA Auto)
   THEN ExRepD
   THEN With ⌜L⌝ (D 0)⋅
   THEN Auto
   THEN (InstLemma `iseg-es-embedding` [⌜Info⌝;⌜L1⌝;⌜L⌝]⋅ THENA Auto)) }

1
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 || L2@i
5. L : (Id × Info) List
6. L1 ≤ L
7. f : ℕ||L2|| ⟶ ℕ||L||
8. ∀i,j:ℕ||L2||.  (i < j ⇒ (f i < f j ∨ f j < ||L1||))
9. ∀j:ℕ||L2||
     ((L2[j] = L[f j] ∈ (Id × Info))
     ∧ (filter(λx.fst(x) = fst(L2[j]);firstn(j + 1;L2))
       = filter(λx.fst(x) = fst(L2[j]);firstn((f j) + 1;L))
       ∈ ((Id × Info) List)))
10. ∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||L2||. (x = (f i) ∈ ℤ)))
11. L2 ≤ L, locally
12. ∀i:Id
      ((filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L1) ∈ ((Id × Info) List))
      ∨ (filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L2) ∈ ((Id × Info) List)))
13. (λx.x embeds global-eo(L1) into global-eo(L))
⊢ ∃f:E ⟶ E. ∃g:E ⟶ E. es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g)

2
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 || L2@i
5. L : (Id × Info) List
6. L1 ≤ L
7. f : ℕ||L2|| ⟶ ℕ||L||
8. ∀i,j:ℕ||L2||.  (i < j ⇒ (f i < f j ∨ f j < ||L1||))
9. ∀j:ℕ||L2||
     ((L2[j] = L[f j] ∈ (Id × Info))
     ∧ (filter(λx.fst(x) = fst(L2[j]);firstn(j + 1;L2))
       = filter(λx.fst(x) = fst(L2[j]);firstn((f j) + 1;L))
       ∈ ((Id × Info) List)))
10. ∀x:ℕ||L||. (x < ||L1|| ∨ (∃i:ℕ||L2||. (x = (f i) ∈ ℤ)))
11. L2 ≤ L, locally
12. ∀i:Id
      ((filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L1) ∈ ((Id × Info) List))
      ∨ (filter(λx.fst(x) = i;L) = filter(λx.fst(x) = i;L2) ∈ ((Id × Info) List)))
13. ∃f:E ⟶ E. ∃g:E ⟶ E. es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g)
14. L' : (Id × Info) List@i
15. L1 || L'@i
16. L2 || L'@i
17. (λx.x embeds global-eo(L1) into global-eo(L))
⊢ L || L'

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}L1,L2:(Id  \mtimes{}  Info)  List.
        (L1  ||  L2
        {}\mRightarrow{}  (\mexists{}L:(Id  \mtimes{}  Info)  List
                  ((\mexists{}f:E  {}\mrightarrow{}  E
                        \mexists{}g:E  {}\mrightarrow{}  E.  es-weak-joint-embedding(Info;global-eo(L1);global-eo(L2);global-eo(L);f;g))
                  \mwedge{}  (\mforall{}L':(Id  \mtimes{}  Info)  List.  (L1  ||  L'  {}\mRightarrow{}  L2  ||  L'  {}\mRightarrow{}  L  ||  L')))))


By

---

Latex:
(InstLemma  `global-order-compat-combine`  []\mcdot{}
  THEN  (RepeatFor  4  (ParallelLast')  THENA  Auto)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}L\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `iseg-es-embedding`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index