---

Step * 2 of Lemma parallel-classrel


1. T : Type
2. Info : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. v : T
8. ↓v ∈ X(e) ∨ v ∈ Y(e)
⊢ v ∈ X || Y(e)
BY
{ (RepUR ``classrel parallel-class eclass-compose2`` 0
   THEN (RWO "bag-member-append" 0 THENA Auto)
   THEN Fold `classrel` 0
   THEN Auto)⋅ }

---

Latex:



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


By

(RepUR  ``classrel  parallel-class  eclass-compose2``  0
  THEN  (RWO  "bag-member-append"  0  THENA  Auto)
  THEN  Fold  `classrel`  0
  THEN  Auto)\mcdot{}

---

Home Index