---

Step * 1 2 1 1 of Lemma member-count-repeats2


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||count-repeats(L,eq)||
5. v1 : T
6. v2 : ℕ+
7. count-repeats(L,eq)[i] = <v1, v2> ∈ (T × ℕ+)
8. apply-alist(eq;count-repeats(L,eq);v1) = (inr ⋅ ) ∈ (ℕ+?)
9. i < ||map(λp.(fst(p));count-repeats(L,eq))||
⊢ v1 = map(λp.(fst(p));count-repeats(L,eq))[i] ∈ T
BY
{ (Assert λp.(fst(p)) ∈ (T × ℕ) ⟶ T BY
         Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||count-repeats(L,eq)||
5. v1 : T
6. v2 : ℕ+
7. count-repeats(L,eq)[i] = <v1, v2> ∈ (T × ℕ+)
8. apply-alist(eq;count-repeats(L,eq);v1) = (inr ⋅ ) ∈ (ℕ+?)
9. i < ||map(λp.(fst(p));count-repeats(L,eq))||
10. λp.(fst(p)) ∈ (T × ℕ) ⟶ T
⊢ v1 = map(λp.(fst(p));count-repeats(L,eq))[i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  i  :  \mBbbN{}||count-repeats(L,eq)||
5.  v1  :  T
6.  v2  :  \mBbbN{}\msupplus{}
7.  count-repeats(L,eq)[i]  =  <v1,  v2>
8.  apply-alist(eq;count-repeats(L,eq);v1)  =  (inr  \mcdot{}  )
9.  i  <  ||map(\mlambda{}p.(fst(p));count-repeats(L,eq))||
\mvdash{}  v1  =  map(\mlambda{}p.(fst(p));count-repeats(L,eq))[i]


By

---

Latex:
(Assert  \mlambda{}p.(fst(p))  \mmember{}  (T  \mtimes{}  \mBbbN{})  {}\mrightarrow{}  T  BY
              Auto)

---

Home Index