---

Step * 1 2 of Lemma sum-count-repeats

.....upcase..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. j : ℤ
5. 0 < j
6. ((j - 1) ≤ ||count-repeats(L,eq)||)
⇒ (Σ(snd(count-repeats(L,eq)[i]) | i < j - 1)
   = ||filter(λx.x ∈b firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq)));L)||
   ∈ ℤ)
⊢ (j ≤ ||count-repeats(L,eq)||)
⇒ (Σ(snd(count-repeats(L,eq)[i]) | i < j) = ||filter(λx.x ∈b firstn(j;map(λp.(fst(p));count-repeats(L,eq)));L)|| ∈ ℤ)
BY
{ ((ParallelLast THENA Auto')
   THEN (RWO "sum-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN HypSubst' (-2) 0
   THEN (InstLemma `firstn_decomp` [⌜T⌝;⌜j⌝;⌜map(λp.(fst(p));count-repeats(L,eq))⌝]⋅ THENA (Auto THEN Auto))
   THEN RevHypSubst (-1) 0
   THEN Thin (-1)
   THEN Thin (-2)) }

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))) @ [map(λp.(fst(p));count-repeats(L,eq))[j - 1]];
           L)||
∈ ℤ

---

Latex:

---

Latex:
.....upcase..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  j  :  \mBbbZ{}
5.  0  <  j
6.  ((j  -  1)  \mleq{}  ||count-repeats(L,eq)||)
{}\mRightarrow{}  (\mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  j  -  1)
      =  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||)
\mvdash{}  (j  \mleq{}  ||count-repeats(L,eq)||)
{}\mRightarrow{}  (\mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  j)
      =  ||filter(\mlambda{}x.x  \mmember{}\msubb{}  firstn(j;map(\mlambda{}p.(fst(p));count-repeats(L,eq)));L)||)


By

---

Latex:
((ParallelLast  THENA  Auto')
  THEN  (RWO  "sum-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  HypSubst'  (-2)  0
  THEN  (InstLemma  `firstn\_decomp`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}map(\mlambda{}p.(fst(p));count-repeats(L,eq))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Auto)
              )
  THEN  RevHypSubst  (-1)  0
  THEN  Thin  (-1)
  THEN  Thin  (-2))

---

Home Index