---

Step * 1 2 1 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
⊢ (||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq)));L)|| + (snd(count-repeats(L,eq)[j - 1])))
= ||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))) @ [map(λp.(fst(p));count-repeats(L,eq))[j - 1]];
           L)||
∈ ℤ
BY
{ TACTIC:(RWO "select-map" 0 THEN Auto THEN Reduce 0) }

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
⊢ (||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq)));L)|| + (snd(count-repeats(L,eq)[j - 1])))
= ||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))) @ [fst(count-repeats(L,eq)[j - 1])];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
\mvdash{}  (||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||
+  (snd(count-repeats(L,eq)[j  -  1])))
=  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq)))
                                @  [map(\mlambda{}p.(fst(p));count-repeats(L,eq))[j  -  1]];L)||


By

---

Latex:
TACTIC:(RWO  "select-map"  0  THEN  Auto  THEN  Reduce  0)

---

Home Index