---

Step * 1 3 1 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
⊢ (∀Ia1,Ia2∈Ias.  ∀e,e':E.  ((¬e ≤loc e' ) ∧ (¬e' ≤loc e )) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
BY
{ (RepeatFor 2 (ParallelOp (-4))
   THEN ParallelLast
   THEN (InstHyp [⌈es⌉] (-1)⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)
   THEN D 0
   THEN ParallelLast
   THEN Auto) }

---

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{}Ia1,Ia2\mmember{}Ias.    \mforall{}e,e':E.    ((\mneg{}e  \mleq{}loc  e'  )  \mwedge{}  (\mneg{}e'  \mleq{}loc  e  ))  supposing  ((\muparrow{}e'  \mmember{}\msubb{}  Ia2)  and  (\muparrow{}e  \mmember{}\msubb{}  Ia1))\000C)


By

---

Latex:
(RepeatFor  2  (ParallelOp  (-4))
  THEN  ParallelLast
  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast)
  THEN  D  0
  THEN  ParallelLast
  THEN  Auto)

---

Home Index