---

Step * 1 2 1 1 1 2 1 1 2 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])
⊢ (||filter(λx.x ∈b v;v2)|| + ||filter(λy.(eq y v1);v2)||) = ||[u / filter(λx.x ∈b v @ [v1];v2)]|| ∈ ℤ
BY
{ (GenListD (-1) THEN D -1 THEN Try (Trivial) THEN GenListD (-1)) }

---

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.  \mneg{}(u  \mmember{}  v)
10.  \mneg{}(u  =  v1)
11.  (u  \mmember{}  v  @  [v1])
\mvdash{}  (||filter(\mlambda{}x.x  \mmember{}\msubb{}  v;v2)||  +  ||filter(\mlambda{}y.(eq  y  v1);v2)||)  =  ||[u  /  filter(\mlambda{}x.x  \mmember{}\msubb{}  v  @  [v1];v2)]||


By

---

Latex:
(GenListD  (-1)  THEN  D  -1  THEN  Try  (Trivial)  THEN  GenListD  (-1))

---

Home Index