---

Step * of Lemma parallel-eclass2-left

∀[Info,B,C:Type]. ∀[X1,X2:EClass(B ─→ bag(C))]. ∀[X:EClass(B)].  ((X1 o X) || (X2 o X) = (X1 || X2 o X) ∈ EClass(C))
BY
{ (Auto
   THEN RepUR ``parallel-class eclass-compose2 eclass2 eclass class-ap`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN Fold `class-ap` 0
   THEN RWO "bag-combine-append-left" 0
   THEN Auto) }

---

Latex:


\mforall{}[Info,B,C:Type].  \mforall{}[X1,X2:EClass(B  {}\mrightarrow{}  bag(C))].  \mforall{}[X:EClass(B)].
    ((X1  o  X)  ||  (X2  o  X)  =  (X1  ||  X2  o  X))


By

(Auto
  THEN  RepUR  ``parallel-class  eclass-compose2  eclass2  eclass  class-ap``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  Fold  `class-ap`  0
  THEN  RWO  "bag-combine-append-left"  0
  THEN  Auto)

---

Home Index