---

Step * 1 1 of Lemma sum-count-repeats

.....basecase..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. j : ℤ
⊢ (0 ≤ ||count-repeats(L,eq)||)
⇒ (Σ(snd(count-repeats(L,eq)[i]) | i < 0) = ||filter(λx.x ∈b firstn(0;map(λp.(fst(p));count-repeats(L,eq)));L)|| ∈ ℤ)
BY
{ ((RWO "first0" 0 THENA Auto)
   THEN Unfold `sum` 0
   THEN Reduce 0
   THEN TACTIC:(RWO "filter_is_nil" 0 THEN RepUR ``so_apply`` 0 THEN Reduce 0 THEN Auto)) }

---

Latex:

---

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


By

---

Latex:
((RWO  "first0"  0  THENA  Auto)
  THEN  Unfold  `sum`  0
  THEN  Reduce  0
  THEN  TACTIC:(RWO  "filter\_is\_nil"  0  THEN  RepUR  ``so\_apply``  0  THEN  Reduce  0  THEN  Auto))

---

Home Index