---

Step * 1 of Lemma count-bag-remove-repeats


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  ∈ ℕ
BY
{ ((RWO "bag-count-sqequal" 0 THENA Auto)
   THEN RepUR ``bag-filter bag-remove-repeats bag-size`` 0
   THEN (RWO "deq-member-length-filter2<" 0 THENA Auto)
   THEN (InstLemma `l_member-iff-length-filter` [⌜T⌝;⌜eq⌝;⌜list-to-set(eq;b2)⌝;⌜x⌝]⋅ THENA Auto)
   THEN (RWO "member-list-to-set" (-1) THENA Auto))⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b2 : T List
5. 1 ≤ ||filter(eq x;list-to-set(eq;b2))|| ⇐⇒ (x ∈ b2)
⊢ ||filter(λy.(eq x y);list-to-set(eq;b2))|| = if x ∈b b2 then 1 else 0 fi  ∈ ℕ

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "bag-count-sqequal"  0  THENA  Auto)
  THEN  RepUR  ``bag-filter  bag-remove-repeats  bag-size``  0
  THEN  (RWO  "deq-member-length-filter2<"  0  THENA  Auto)
  THEN  (InstLemma  `l\_member-iff-length-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}list-to-set(eq;b2)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "member-list-to-set"  (-1)  THENA  Auto))\mcdot{}

---

Home Index