---

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


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)
BY
{ ((FLemma `iseg_length` [6] THENA Auto)
   THEN (Assert λx.x ∈ E ─→ E BY
               (RWO "global-eo-E-sq" 0 THEN Auto))
   THEN (Assert f ∈ E ─→ E BY
               (RWO "global-eo-E-sq" 0 THEN Auto))
   THEN InstConcl [⌈λx.x⌉;⌈f⌉]⋅
   THEN Auto
   THEN (D 0 THEN Reduce 0)
   THEN Try (Trivial)
   THEN SplitAndConcl) }

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))
14. ||L1|| ≤ ||L||
15. λx.x ∈ E ─→ E
16. f ∈ E ─→ E
⊢ es-local-embedding(Info;global-eo(L2);global-eo(L);f)

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. (λx.x embeds global-eo(L1) into global-eo(L))
14. ||L1|| ≤ ||L||
15. λx.x ∈ E ─→ E
16. f ∈ E ─→ E
⊢ ∀e:E. ((∃e1:E. (e = e1 ∈ E)) ∨ (∃e2:E. (e = (f e2) ∈ E)))

3
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))
14. ||L1|| ≤ ||L||
15. λx.x ∈ E ─→ E
16. f ∈ E ─→ E
⊢ ∀x,y:E.  ((x < y) ⇒ ((f x < f y) ∨ (∃z:E. ((f y) = z ∈ E))))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  L1  :  (Id  \mtimes{}  Info)  List@i
3.  L2  :  (Id  \mtimes{}  Info)  List@i
4.  L1  ||  L2@i
5.  L  :  (Id  \mtimes{}  Info)  List
6.  L1  \mleq{}  L
7.  f  :  \mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L||
8.  \mforall{}i,j:\mBbbN{}||L2||.    (i  <  j  {}\mRightarrow{}  (f  i  <  f  j  \mvee{}  f  j  <  ||L1||))
9.  \mforall{}j:\mBbbN{}||L2||
          ((L2[j]  =  L[f  j])
          \mwedge{}  (filter(\mlambda{}x.fst(x)  =  fst(L2[j]);firstn(j  +  1;L2))
              =  filter(\mlambda{}x.fst(x)  =  fst(L2[j]);firstn((f  j)  +  1;L))))
10.  \mforall{}x:\mBbbN{}||L||.  (x  <  ||L1||  \mvee{}  (\mexists{}i:\mBbbN{}||L2||.  (x  =  (f  i))))
11.  L2  \mleq{}  L,  locally
12.  \mforall{}i:Id
            ((filter(\mlambda{}x.fst(x)  =  i;L)  =  filter(\mlambda{}x.fst(x)  =  i;L1))
            \mvee{}  (filter(\mlambda{}x.fst(x)  =  i;L)  =  filter(\mlambda{}x.fst(x)  =  i;L2)))
13.  (\mlambda{}x.x  embeds  global-eo(L1)  into  global-eo(L))
\mvdash{}  \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)


By

---

Latex:
((FLemma  `iseg\_length`  [6]  THENA  Auto)
  THEN  (Assert  \mlambda{}x.x  \mmember{}  E  {}\mrightarrow{}  E  BY
                          (RWO  "global-eo-E-sq"  0  THEN  Auto))
  THEN  (Assert  f  \mmember{}  E  {}\mrightarrow{}  E  BY
                          (RWO  "global-eo-E-sq"  0  THEN  Auto))
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (D  0  THEN  Reduce  0)
  THEN  Try  (Trivial)
  THEN  SplitAndConcl)

---

Home Index