---

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


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. v1 : T
5. v : T List
⊢ (¬(v1 ∈ v)) ⇒ ((||filter(λx.x ∈b v;L)|| + ||filter(λy.(eq y v1);L)||) = ||filter(λx.x ∈b v @ [v1];L)|| ∈ ℤ)
BY
{ ((D 0 THENA Auto)
   THEN ListInd 3
   THEN Reduce 0
   THEN ((Fold `member` 0 THEN Auto)
   ORELSE (RepeatFor 3 ((SplitOnConclITE THENA Auto))
           THEN Try ((DNot (-1) THEN Complete (Auto)))
           THEN Try ((Reduce 0 THEN BetterArith)))
   )) }

1
.....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)]|| ∈ ℤ

2
.....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)]|| ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  v1  :  T
5.  v  :  T  List
\mvdash{}  (\mneg{}(v1  \mmember{}  v))
{}\mRightarrow{}  ((||filter(\mlambda{}x.x  \mmember{}\msubb{}  v;L)||  +  ||filter(\mlambda{}y.(eq  y  v1);L)||)  =  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  v  @  [v1];L)||)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  ListInd  3
  THEN  Reduce  0
  THEN  ((Fold  `member`  0  THEN  Auto)
  ORELSE  (RepeatFor  3  ((SplitOnConclITE  THENA  Auto))
                  THEN  Try  ((DNot  (-1)  THEN  Complete  (Auto)))
                  THEN  Try  ((Reduce  0  THEN  BetterArith)))
  ))

---

Home Index