---

Step * of Lemma Q-R-glued-first

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[Q,R:E ⟶ E ⟶ ℙ]. ∀[A,B:Type].
      ∀Ias:EClass(A) List. ∀Ibs:EClass(B) List. ∀f:E(first-class(Ias)) ⟶ B.
        ((∀i:ℕ||Ias||. Ias[i]:Q →─f⟶  Ibs[i]:R)
           ⇒ first-class(Ias):Q →─f⟶  first-class(Ibs):R 
              supposing (∀Ia1,Ia2∈Ias.  ∀e,e':E.
                                          ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposi\000Cng 
           ((||Ias|| = ||Ibs|| ∈ ℤ) and 
           (∀Ib1,Ib2∈Ibs.  Ib1 ⋂ Ib2 = 0) and 
           (∀Ia1,Ia2∈Ias.  Ia1 ⋂ Ia2 = 0))
BY
{ InductionOnList }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ⟶ E ⟶ ℙ
4. [R] : E ⟶ E ⟶ ℙ
5. [A] : Type
6. [B] : Type
⊢ ∀Ibs:EClass(B) List. ∀f:E(first-class([])) ⟶ B.
    ((∀i:ℕ||[]||. [][i]:Q →─f⟶  Ibs[i]:R)
       ⇒ first-class([]):Q →─f⟶  first-class(Ibs):R 
          supposing (∀Ia1,Ia2∈[].  ∀e,e':E.
                                     ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
       ((||[]|| = ||Ibs|| ∈ ℤ) and 
       (∀Ib1,Ib2∈Ibs.  Ib1 ⋂ Ib2 = 0) and 
       (∀Ia1,Ia2∈[].  Ia1 ⋂ Ia2 = 0))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ⟶ E ⟶ ℙ
4. [R] : E ⟶ E ⟶ ℙ
5. [A] : Type
6. [B] : Type
7. u : EClass(A)@i'
8. v : EClass(A) List@i'
9. ∀Ibs:EClass(B) List. ∀f:E(first-class(v)) ⟶ B.
     ((∀i:ℕ||v||. v[i]:Q →─f⟶  Ibs[i]:R)
        ⇒ first-class(v):Q →─f⟶  first-class(Ibs):R 
           supposing (∀Ia1,Ia2∈v.  ∀e,e':E.
                                     ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposing 
        ((||v|| = ||Ibs|| ∈ ℤ) and 
        (∀Ib1,Ib2∈Ibs.  Ib1 ⋂ Ib2 = 0) and 
        (∀Ia1,Ia2∈v.  Ia1 ⋂ Ia2 = 0))@i 2
⊢ ∀Ibs:EClass(B) List. ∀f:E(first-class([u / v])) ⟶ B.
    ((∀i:ℕ||[u / v]||. [u / v][i]:Q →─f⟶  Ibs[i]:R)
       ⇒ first-class([u / v]):Q →─f⟶  first-class(Ibs):R 
          supposing (∀Ia1,Ia2∈[u / v].  ∀e,e':E.
                                          ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))) supposi\000Cng 
       ((||[u / v]|| = ||Ibs|| ∈ ℤ) and 
       (∀Ib1,Ib2∈Ibs.  Ib1 ⋂ Ib2 = 0) and 
       (∀Ia1,Ia2∈[u / v].  Ia1 ⋂ Ia2 = 0))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \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||.  Ias[i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
                      {}\mRightarrow{}  first-class(Ias):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R 
                            supposing  (\mforall{}Ia1,Ia2\mmember{}Ias.    \mforall{}e,e':E.
                                                                                    ((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  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))


By

---

Latex:
InductionOnList

---

Home Index