---

Step * 1 2 1 1 1 2 1 1 1 of Lemma sum-count-repeats

.....truecase..... 
1. T : Type
2. eq : EqDecider(T)
3. v1 : T
4. v : T List
5. ¬(v1 ∈ v)
6. u : T
7. v2 : T List
8. (||filter(λx.x ∈b v;v2)|| + ||filter(λy.(eq y v1);v2)||) = ||filter(λx.x ∈b v @ [v1];v2)|| ∈ ℤ
9. (u ∈ v)
10. u = v1 ∈ T
11. (u ∈ v @ [v1])
⊢ (||[u / filter(λx.x ∈b v;v2)]|| + ||[u / filter(λy.(eq y v1);v2)]||) = ||[u / filter(λx.x ∈b v @ [v1];v2)]|| ∈ ℤ
BY
{ (D 5 THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  v1  :  T
4.  v  :  T  List
5.  \mneg{}(v1  \mmember{}  v)
6.  u  :  T
7.  v2  :  T  List
8.  (||filter(\mlambda{}x.x  \mmember{}\msubb{}  v;v2)||  +  ||filter(\mlambda{}y.(eq  y  v1);v2)||)  =  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  v  @  [v1];v2)||
9.  (u  \mmember{}  v)
10.  u  =  v1
11.  (u  \mmember{}  v  @  [v1])
\mvdash{}  (||[u  /  filter(\mlambda{}x.x  \mmember{}\msubb{}  v;v2)]||  +  ||[u  /  filter(\mlambda{}y.(eq  y  v1);v2)]||)
=  ||[u  /  filter(\mlambda{}x.x  \mmember{}\msubb{}  v  @  [v1];v2)]||


By

---

Latex:
(D  5  THEN  Auto)

---

Home Index