---

Step * of Lemma member-disjoint-union-comb

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].  uiff(↑e ∈b X (+) Y;↑(e ∈b X ∨be ∈b Y))
BY
{ (RepUR ``member-eclass disjoint-union-comb parallel-class eclass-compose2`` 0
   THEN RepUR ``lifting-1 lifting1 lifting-gen-rev`` 0
   THEN RepeatFor 2 ((RecUnfold `lifting-gen-list-rev` 0⋅ THEN Reduce 0))
   THEN RepUR ``simple-comb-1 simple-comb`` 0
   THEN (RWW "bag-combine-single-right-as-map bag-size-append bag-size-map" 0 THENA Auto)
   THEN Fold `class-ap` 0) }

1
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(↑¬b(#(X(e)) + #(Y(e)) =z 0);↑((¬b(#(X(e)) =z 0)) ∨b(¬b(#(Y(e)) =z 0))))

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  X  (+)  Y;\muparrow{}(e  \mmember{}\msubb{}  X  \mvee{}\msubb{}e  \mmember{}\msubb{}  Y))


By

---

Latex:
(RepUR  ``member-eclass  disjoint-union-comb  parallel-class  eclass-compose2``  0
  THEN  RepUR  ``lifting-1  lifting1  lifting-gen-rev``  0
  THEN  RepeatFor  2  ((RecUnfold  `lifting-gen-list-rev`  0\mcdot{}  THEN  Reduce  0))
  THEN  RepUR  ``simple-comb-1  simple-comb``  0
  THEN  (RWW  "bag-combine-single-right-as-map  bag-size-append  bag-size-map"  0  THENA  Auto)
  THEN  Fold  `class-ap`  0)

---

Home Index