---

Step * of Lemma parallel-eclass2-right

∀[Info,B,C:Type]. ∀[X:EClass(B ─→ bag(C))]. ∀[X1,X2:EClass(B)].  ((X o X1) || (X o X2) = (X o X1 || X2) ∈ 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-right<" 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN RWO "bag-combine-append-left" 0⋅
   THEN Auto) }

---

Latex:


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


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-right<"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  RWO  "bag-combine-append-left"  0\mcdot{}
  THEN  Auto)

---

Home Index