---

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


1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. bag-no-repeats(T;bs)
5. x : T
6. 1 ≤ #([y∈bs|eq x y])
⊢ #([y∈bs|eq x y]) = 1 ∈ ℤ
BY
{ (D (-3) THEN ExRepD THEN Eliminate ⌜bs⌝⋅ THEN Auto THEN All (RepUR ``bag-count bag-filter bag-size``)) }

1
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)||
⊢ ||filter(λy.(eq x y);L)|| = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  bag-no-repeats(T;bs)
5.  x  :  T
6.  1  \mleq{}  \#([y\mmember{}bs|eq  x  y])
\mvdash{}  \#([y\mmember{}bs|eq  x  y])  =  1


By

---

Latex:
(D  (-3)
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}bs\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  All  (RepUR  ``bag-count  bag-filter  bag-size``))

---

Home Index