---

Step * 2 of Lemma member-parallel-class


1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. e : E
7. ↑(e ∈b X ∨be ∈b Y)
⊢ ↑e ∈b X || Y
BY
{ (All (RepUR ``parallel-class eclass-compose2 member-eclass``)
   THEN Repeat (AllPushDown)
   THEN RWO "bag-size-append" 0
   THEN Auto') }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  Y  :  EClass(A)
5.  es  :  EO+(Info)
6.  e  :  E
7.  \muparrow{}(e  \mmember{}\msubb{}  X  \mvee{}\msubb{}e  \mmember{}\msubb{}  Y)
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  X  ||  Y


By

---

Latex:
(All  (RepUR  ``parallel-class  eclass-compose2  member-eclass``)
  THEN  Repeat  (AllPushDown)
  THEN  RWO  "bag-size-append"  0
  THEN  Auto')

---

Home Index