---

Step * 1 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 × ℕ+)
9. let x,n = count-repeats(L,eq)[i] 
   in n = ||filter(λy.(eq y x);L)|| ∈ ℤ
⊢ n = ||filter(λy.(eq y x);L)|| ∈ ℤ
BY
{ ((RevHypSubst' (-2) (-1) THENA Auto) THEN Reduce (-1)) }

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. 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]
9.  let  x,n  =  count-repeats(L,eq)[i] 
      in  n  =  ||filter(\mlambda{}y.(eq  y  x);L)||
\mvdash{}  n  =  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
((RevHypSubst'  (-2)  (-1)  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index