---

Step * 2 1 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)
7. x : T
8. 1 ≤ ||filter(eq x;bs)||
⊢ ||filter(eq x;bs)|| = 1 ∈ ℤ
BY
{ ((InstHyp [⌜x⌝] (-4)⋅ THENA Auto) THEN D -1 THEN D -2) }

1
.....antecedent..... 
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)||
9. 1 ≤ ||filter(λy.(eq x y);bs)|| supposing ||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ
⊢ 1 ≤ ||filter(λy.(eq x y);bs)||

2
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)||
9. 1 ≤ ||filter(λy.(eq x y);bs)|| supposing ||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ
10. ||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ
⊢ ||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
7.  x  :  T
8.  1  \mleq{}  ||filter(eq  x;bs)||
\mvdash{}  ||filter(eq  x;bs)||  =  1


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  D  -2)

---

Home Index