---

Step * of Lemma glued-first

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A,B:Type].
      ∀Ias:EClass(A) List. ∀Ibs:EClass(B) List. ∀f:E(first-class(Ias)) ─→ B.
        ((∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])) ⇒ glued(es;B;f;first-class(Ias);first-class(Ibs))) supposing 
           ((||Ias|| = ||Ibs|| ∈ ℤ) and 
           (∀Ib1,Ib2∈Ibs.  Ib1 ∩ Ib2 = 0) and 
           (∀Ia1,Ia2∈Ias.  ∀es:EO+(Info). ∀e,e':E.  (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))\000C)
BY
{ ((InstLemma `Q-R-glued-first` []
    THEN RepeatFor 2 (ParallelLast')
    THEN (InstHyp [⌈λe,e'. e ≤loc e' ⌉;⌈λe,e'. e ≤loc e' ⌉] (-1)⋅ THENA Auto)
    THEN Thin (-2))
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN Try ((BLemma `es-E-interface-first-class` THEN Auto)⋅)) }

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||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ glued(es;B;f;first-class(Ias);first-class(Ibs))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B:Type].
            \mforall{}Ias:EClass(A)  List.  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class(Ias))  {}\mrightarrow{}  B.
                ((\mforall{}i:\mBbbN{}||Ias||.  glued(es;B;f;Ias[i];Ibs[i]))
                      {}\mRightarrow{}  glued(es;B;f;first-class(Ias);first-class(Ibs)))  supposing 
                      ((||Ias||  =  ||Ibs||)  and 
                      (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
                      (\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))))


By

---

Latex:
((InstLemma  `Q-R-glued-first`  []
    THEN  RepeatFor  2  (ParallelLast')
    THEN  (InstHyp  [\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{};\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
    THEN  Thin  (-2))
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  Try  ((BLemma  `es-E-interface-first-class`  THEN  Auto)\mcdot{}))

---

Home Index