---

Step * of Lemma count-bag-remove-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].
  ((#x in bag-remove-repeats(eq;bs)) ~ if 0 <z (#x in bs) then 1 else 0 fi )
BY
{ (Auto
   THEN BagD (-2)
   THEN (Subst' (#x in bag-remove-repeats(eq;as)) = (#x in bag-remove-repeats(eq;bs)) ∈ ℤ 0
         THENA RepeatFor 2 ((EqCD THEN Auto))
         )
   THEN ThinVar `as'⋅
   THEN RenameVar `b2' (-1)) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b2 : T List
⊢ (#x in bag-remove-repeats(eq;b2)) = if 0 <z (#x in b2) then 1 else 0 fi  ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].
    ((\#x  in  bag-remove-repeats(eq;bs))  \msim{}  if  0  <z  (\#x  in  bs)  then  1  else  0  fi  )


By

---

Latex:
(Auto
  THEN  BagD  (-2)
  THEN  (Subst'  (\#x  in  bag-remove-repeats(eq;as))  =  (\#x  in  bag-remove-repeats(eq;bs))  0
              THENA  RepeatFor  2  ((EqCD  THEN  Auto))
              )
  THEN  ThinVar  `as'\mcdot{}
  THEN  RenameVar  `b2'  (-1))

---

Home Index