---

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


1. T : Type
2. L : T List
3. eq : EqDecider(T)
4. bs : bag(T)
5. L = bs ∈ bag(T)
6. no_repeats(T;L)
7. x : T
8. 1 ≤ ||filter(λy.(eq x y);L)||
9. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
10. no_repeats(T;L)
11. 1 ≤ ||filter(eq x;L)|| supposing ||filter(eq x;L)|| = 1 ∈ ℤ
12. ||filter(eq x;L)|| = 1 ∈ ℤ
⊢ ||filter(λy.(eq x y);L)|| = 1 ∈ ℤ
BY
{ (Subst' filter(λy.(eq x y);L) = filter(eq x;L) ∈ (T List) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  eq  :  EqDecider(T)
4.  bs  :  bag(T)
5.  L  =  bs
6.  no\_repeats(T;L)
7.  x  :  T
8.  1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);L)||
9.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;L)||;||filter(eq  x;L)||  =  1)
10.  no\_repeats(T;L)
11.  1  \mleq{}  ||filter(eq  x;L)||  supposing  ||filter(eq  x;L)||  =  1
12.  ||filter(eq  x;L)||  =  1
\mvdash{}  ||filter(\mlambda{}y.(eq  x  y);L)||  =  1


By

---

Latex:
(Subst'  filter(\mlambda{}y.(eq  x  y);L)  =  filter(eq  x;L)  0  THEN  Auto)

---

Home Index