---

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

.....assertion..... 
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)|| ∈ ℤ
⊢ ¬(v1 ∈ firstn(j - 1;map(λp.(fst(p));count-repeats(L,eq))))
BY
{ ((D 0 THENA Auto)
   THEN (RWO "member_firstn" (-1) THENA Auto)
   THEN ExRepD
   THEN (InstLemma `no_repeats-count-repeats1` [⌜T⌝;⌜eq⌝;⌜L⌝]⋅ THENA Auto)
   THEN Unfold `no_repeats` -1
   THEN InstHyp [⌜i⌝;⌜j - 1⌝] (-1)
   ⋅
   THEN Auto
   THEN Thin (-2)
   THEN All (RWO "select-map" )⋅
   THEN 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. i : ℕ
13. i < j - 1
14. i < ||map(λp.(fst(p));count-repeats(L,eq))||
15. v1 = ((λp.(fst(p))) count-repeats(L,eq)[i]) ∈ T
16. ¬(((λp.(fst(p))) count-repeats(L,eq)[i]) = ((λp.(fst(p))) count-repeats(L,eq)[j - 1]) ∈ T)
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
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)||
\mvdash{}  \mneg{}(v1  \mmember{}  firstn(j  -  1;map(\mlambda{}p.(fst(p));count-repeats(L,eq))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RWO  "member\_firstn"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `no\_repeats-count-repeats1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `no\_repeats`  -1
  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j  -  1\mkleeneclose{}]  (-1)
  \mcdot{}
  THEN  Auto
  THEN  Thin  (-2)
  THEN  All  (RWO  "select-map"  )\mcdot{}
  THEN  Auto)

---

Home Index