---

Step * 1 of Lemma Q-R-glued-first


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))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `pairwise` 0
   THEN Reduce 0
   THEN DVar `Ibs'
   THEN Reduce 0
   THEN Auto
   THEN Auto') }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ⟶ E ⟶ ℙ
4. [R] : E ⟶ E ⟶ ℙ
5. [A] : Type
6. [B] : Type
7. f : E(first-class([])) ⟶ B@i
8. ∀i:ℕ0. ∀j:ℕi.  ⊥ ⋂ ⊥ = 0
9. ∀i:ℕ0. ∀j:ℕi.  ⊥ ⋂ ⊥ = 0
10. 0 = 0 ∈ ℤ
11. ∀i:ℕ0. ⊥:Q →─f⟶  ⊥:R@i
12. ∀i:ℕ0. ∀j:ℕi. ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b ⊥) and (↑e ∈b ⊥))
⊢ first-class([]):Q →─f⟶  first-class([]):R

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [Q]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  [R]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [A]  :  Type
6.  [B]  :  Type
\mvdash{}  \mforall{}Ibs:EClass(B)  List.  \mforall{}f:E(first-class([]))  {}\mrightarrow{}  B.
        ((\mforall{}i:\mBbbN{}||[]||.  [][i]:Q  \mrightarrow{}{}f{}\mrightarrow{}    Ibs[i]:R)
              {}\mRightarrow{}  first-class([]):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class(Ibs):R 
                    supposing  (\mforall{}Ia1,Ia2\mmember{}[].    \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 
              ((||[]||  =  ||Ibs||)  and 
              (\mforall{}Ib1,Ib2\mmember{}Ibs.    Ib1  \mcap{}  Ib2  =  0)  and 
              (\mforall{}Ia1,Ia2\mmember{}[].    Ia1  \mcap{}  Ia2  =  0))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `pairwise`  0
  THEN  Reduce  0
  THEN  DVar  `Ibs'
  THEN  Reduce  0
  THEN  Auto
  THEN  Auto')

---

Home Index