Step
*
1
1
1
1
of Lemma
bag-no-repeats-count
.....antecedent..... 
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 ∈ ℤ
⊢ 1 ≤ ||filter(eq x;L)||
BY
{ (Subst' filter(λy.(eq x y);L) = filter(eq x;L) ∈ (T List) -4 THEN Auto) }
Latex:
Latex:
.....antecedent..... 
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
\mvdash{}  1  \mleq{}  ||filter(eq  x;L)||
By
Latex:
(Subst'  filter(\mlambda{}y.(eq  x  y);L)  =  filter(eq  x;L)  -4  THEN  Auto)
Home
Index