---

Step * 1 2 of Lemma glued-first


1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e'  →─f─→  Ibs[i]:λe,e'. e ≤loc e' )
      ⇒ first-class(Ias):λe,e'. e ≤loc e'  →─f─→  first-class(Ibs):λe,e'. e ≤loc e'  
         supposing (∀Ia1,Ia2∈Ias.  ∀e,e':E.
                                     ((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing 
                                        ((↑e' ∈b Ia2) and 
                                        (↑e ∈b Ia1)))) supposing 
      ((||Ias|| = ||Ibs|| ∈ ℤ) and 
      (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
      (∀Ia1,Ia2∈Ias.  Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias.  ∀es:EO+(Info). ∀e,e':E.  (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. ∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ ∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e'  →─f─→  Ibs[i]:λe,e'. e ≤loc e' 
BY
{ (ParallelLast THEN Unfold `glued` -1 THEN Unfold `Q-R-glued` 0)⋅ }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e'  →─f─→  Ibs[i]:λe,e'. e ≤loc e' )
      ⇒ first-class(Ias):λe,e'. e ≤loc e'  →─f─→  first-class(Ibs):λe,e'. e ≤loc e'  
         supposing (∀Ia1,Ia2∈Ias.  ∀e,e':E.
                                     ((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing 
                                        ((↑e' ∈b Ia2) and 
                                        (↑e ∈b Ia1)))) supposing 
      ((||Ias|| = ||Ibs|| ∈ ℤ) and 
      (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
      (∀Ia1,Ia2∈Ias.  Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias.  ∀es:EO+(Info). ∀e,e':E.  (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. i : ℕ||Ias||@i
13. ∃g:E(Ibs[i]) ─→ E. g glues Ias[i] ──f─→ Ibs[i]
⊢ ∃g:E(Ibs[i]) ─→ E. g glues Ias[i]:λe,e'. e ≤loc e'  ──f─→ Ibs[i]:λe,e'. e ≤loc e' 

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [A]  :  Type
4.  [B]  :  Type
5.  Ias  :  EClass(A)  List@i'
6.  Ibs  :  EClass(B)  List@i'
7.  f  :  E(first-class(Ias))  {}\mrightarrow{}  B@i
8.  ((\mforall{}i:\mBbbN{}||Ias||.  Ias[i]:\mlambda{}e,e'.  e  \mleq{}loc  e'    \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:\mlambda{}e,e'.  e  \mleq{}loc  e'  )
            {}\mRightarrow{}  first-class(Ias):\mlambda{}e,e'.  e  \mleq{}loc  e'    \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):\mlambda{}e,e'.  e  \mleq{}loc  e'   
                  supposing  (\mforall{}Ia1,Ia2\mmember{}Ias.    \mforall{}e,e':E.
                                                                          ((\mneg{}((\mlambda{}e,e'.  e  \mleq{}loc  e'  )  e  e'))
                                                                                \mwedge{}  (\mneg{}((\mlambda{}e,e'.  e  \mleq{}loc  e'  )  e'  e)))  supposing 
                                                                                ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and 
                                                                                (\muparrow{}e  \mmember{}\msubb{}  Ia1))))  supposing 
            ((||Ias||  =  ||Ibs||)  and 
            (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
            (\mforall{}Ia1,Ia2\mmember{}Ias.    Ia1  \mcap{}  Ia2  =  0))
9.  (\mforall{}Ia1,Ia2\mmember{}Ias.    \mforall{}es:EO+(Info).  \mforall{}e,e':E.
                                          (\mneg{}(loc(e)  =  loc(e')))  supposing  ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and  (\muparrow{}e  \mmember{}\msubb{}  Ia1)))
10.  (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)
11.  ||Ias||  =  ||Ibs||
12.  \mforall{}i:\mBbbN{}||Ias||.  glued(es;B;f;Ias[i];Ibs[i])@i
\mvdash{}  \mforall{}i:\mBbbN{}||Ias||.  Ias[i]:\mlambda{}e,e'.  e  \mleq{}loc  e'    \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:\mlambda{}e,e'.  e  \mleq{}loc  e' 


By

---

Latex:
(ParallelLast  THEN  Unfold  `glued`  -1  THEN  Unfold  `Q-R-glued`  0)\mcdot{}

---

Home Index