---

Step * 1 of Lemma member-count-repeats3


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. n : ℕ+
6. i : ℕ
7. i < ||count-repeats(L,eq)||
8. <x, n> = count-repeats(L,eq)[i] ∈ (T × ℕ+)
⊢ n = ||filter(λy.(eq y x);L)|| ∈ ℤ
BY
{ (InstLemma `member-count-repeats2` [⌜T⌝;⌜eq⌝;⌜L⌝;⌜i⌝]⋅ THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. n : ℕ+
6. i : ℕ
7. i < ||count-repeats(L,eq)||
8. <x, n> = count-repeats(L,eq)[i] ∈ (T × ℕ+)
9. let x,n = count-repeats(L,eq)[i] 
   in n = ||filter(λy.(eq y x);L)|| ∈ ℤ
⊢ n = ||filter(λy.(eq y x);L)|| ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  n  :  \mBbbN{}\msupplus{}
6.  i  :  \mBbbN{}
7.  i  <  ||count-repeats(L,eq)||
8.  <x,  n>  =  count-repeats(L,eq)[i]
\mvdash{}  n  =  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
(InstLemma  `member-count-repeats2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index