---

Step * of Lemma bag-member-remove-repeats

∀[T:Type]. ∀[b:bag(T)]. ∀[eq:EqDecider(T)]. ∀[x:T].  uiff(x ↓∈ b;x ↓∈ bag-remove-repeats(eq;b))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN Auto
   THEN (BagToList 2 THENA Auto)
   THEN Try (Unfold `bag-remove-repeats` 0)
   THEN Try (Unfold `bag-remove-repeats` (-1))
   THEN (FLemma `bag-member-list` [-1] THENA Auto)
   THEN (RWO "bag-member-list" 0 THENA Auto)
   THEN Try ((RWO "member-list-to-set" 0 THEN Auto))
   THEN Try ((RWO "member-list-to-set" (-1) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].    uiff(x  \mdownarrow{}\mmember{}  b;x  \mdownarrow{}\mmember{}  bag-remove-repeats(eq;b))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (BagToList  2  THENA  Auto)
  THEN  Try  (Unfold  `bag-remove-repeats`  0)
  THEN  Try  (Unfold  `bag-remove-repeats`  (-1))
  THEN  (FLemma  `bag-member-list`  [-1]  THENA  Auto)
  THEN  (RWO  "bag-member-list"  0  THENA  Auto)
  THEN  Try  ((RWO  "member-list-to-set"  0  THEN  Auto))
  THEN  Try  ((RWO  "member-list-to-set"  (-1)  THEN  Auto)))

---

Home Index