---

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


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. j : ℤ
5. 0 < j
6. j ≤ ||count-repeats(L,eq)||
7. 0 < j
8. v1 : T
9. v2 : ℕ+
10. count-repeats(L,eq)[j - 1] = <v1, v2> ∈ (T × ℕ+)
11. v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ
12. ¬(v1 ∈ firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))))
⊢ (||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq)));L)|| + ||filter(λy.(eq y v1);L)||)
= ||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))) @ [v1];L)||
∈ ℤ
BY
{ (MoveToConcl (-1) THEN (GenConclAtAddrType ⌜T List⌝ [1;1;2]⋅ THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. j : ℤ
5. 0 < j
6. j ≤ ||count-repeats(L,eq)||
7. 0 < j
8. v1 : T
9. v2 : ℕ+
10. count-repeats(L,eq)[j - 1] = <v1, v2> ∈ (T × ℕ+)
11. v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ
12. v : T List
13. firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))) = v ∈ (T List)
⊢ (¬(v1 ∈ v)) ⇒ ((||filter(λx.x ∈b v;L)|| + ||filter(λy.(eq y v1);L)||) = ||filter(λx.x ∈b v @ [v1];L)|| ∈ ℤ)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  j  :  \mBbbZ{}
5.  0  <  j
6.  j  \mleq{}  ||count-repeats(L,eq)||
7.  0  <  j
8.  v1  :  T
9.  v2  :  \mBbbN{}\msupplus{}
10.  count-repeats(L,eq)[j  -  1]  =  <v1,  v2>
11.  v2  =  ||filter(\mlambda{}y.(eq  y  v1);L)||
12.  \mneg{}(v1  \mmember{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq))))
\mvdash{}  (||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||
+  ||filter(\mlambda{}y.(eq  y  v1);L)||)
=  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq)))  @  [v1];L)||


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConclAtAddrType  \mkleeneopen{}T  List\mkleeneclose{}  [1;1;2]\mcdot{}  THENA  Auto))

---

Home Index