---

Step * 1 2 1 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))) @ [fst(count-repeats(L,eq)[j - 1])];L)||
∈ ℤ
BY
{ ((InstLemma `member-count-repeats2` [⌜T⌝;⌜eq⌝;⌜L⌝;⌜j - 1⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN D -2
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN HypSubst' (-1) 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
8. v1 : T
9. v2 : ℕ+
10. count-repeats(L,eq)[j - 1] = <v1, v2> ∈ (T × ℕ+)
11. v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ
⊢ (||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)||
∈ ℤ

---

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)))
                                @  [fst(count-repeats(L,eq)[j  -  1])];L)||


By

---

Latex:
((InstLemma  `member-count-repeats2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}j  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  HypSubst'  (-1)  0)

---

Home Index