---

Step * of Lemma bag-member-remove

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,z:T].  uiff(z ↓∈ bs - x;z ↓∈ bs ∧ (¬(z = x ∈ T)))
BY
{ xxx((UnivCD THENA Auto)
      THEN Unfold `bag-remove` 0
      THEN RWO "bag-member-filter" 0
      THEN Auto
      THEN ((All (RW assert_pushdownC)  THENM Try (ParallelLast)) THENA Auto))xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x,z:T].    uiff(z  \mdownarrow{}\mmember{}  bs  -  x;z  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\mneg{}(z  =  x)))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  Unfold  `bag-remove`  0
        THEN  RWO  "bag-member-filter"  0
        THEN  Auto
        THEN  ((All  (RW  assert\_pushdownC)    THENM  Try  (ParallelLast))  THENA  Auto))xxx

---

Home Index