---

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


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)
6. (x ∈ b2)
7. no_repeats(T;list-to-set(eq;b2))
⊢ ||filter(eq x;list-to-set(eq;b2))|| = 1 ∈ ℕ
BY
{ (InstLemma `no-repeats-iff-count` [⌜T⌝;⌜eq⌝]⋅ 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)
6. (x ∈ b2)
7. no_repeats(T;list-to-set(eq;b2))
8. ∀[L:T List]. uiff(no_repeats(T;L);∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ))
⊢ ||filter(eq x;list-to-set(eq;b2))|| = 1 ∈ ℕ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  b2  :  T  List
5.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;b2))||  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  b2)
6.  (x  \mmember{}  b2)
7.  no\_repeats(T;list-to-set(eq;b2))
\mvdash{}  ||filter(eq  x;list-to-set(eq;b2))||  =  1


By

---

Latex:
(InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index