---

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


1. T : Type
2. eq : EqDecider(T)
3. bs : T List
4. ∀[x:T]. uiff(1 ≤ count(eq x;bs);count(eq x;bs) = 1 ∈ ℤ)
5. ∀[x:T]. uiff(1 ≤ ||filter(λy.(eq x y);bs)||;||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ)
6. bs = bs ∈ bag(T)
⊢ no_repeats(T;bs)
BY
{ TACTIC:(UsingVars [`eq'] (BLemma `no-repeats-iff-count`) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : T List
4. ∀[x:T]. uiff(1 ≤ count(eq x;bs);count(eq x;bs) = 1 ∈ ℤ)
5. ∀[x:T]. uiff(1 ≤ ||filter(λy.(eq x y);bs)||;||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ)
6. bs = bs ∈ bag(T)
7. x : T
8. 1 ≤ ||filter(eq x;bs)||
⊢ ||filter(eq x;bs)|| = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  T  List
4.  \mforall{}[x:T].  uiff(1  \mleq{}  count(eq  x;bs);count(eq  x;bs)  =  1)
5.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);bs)||;||filter(\mlambda{}y.(eq  x  y);bs)||  =  1)
6.  bs  =  bs
\mvdash{}  no\_repeats(T;bs)


By

---

Latex:
TACTIC:(UsingVars  [`eq']  (BLemma  `no-repeats-iff-count`)  THEN  Auto)

---

Home Index