Step
*
2
1
1
of Lemma
no-repeats-iff-count
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
⊢ 2 ≤ ||filter(eq L[i];L)||
BY
{ (Decide ⌜i < j⌝⋅ THENA Auto) }
1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
11. i < j
⊢ 2 ≤ ||filter(eq L[i];L)||
2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
11. ¬i < j
⊢ 2 ≤ ||filter(eq L[i];L)||
Latex:
Latex:
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. \mforall{}[x:T]. uiff(1 \mleq{} ||filter(eq x;L)||;||filter(eq x;L)|| = 1)
5. i : \mBbbN{}
6. j : \mBbbN{}
7. i < ||L||
8. j < ||L||
9. \mneg{}(i = j)
10. L[i] = L[j]
\mvdash{} 2 \mleq{} ||filter(eq L[i];L)||
By
Latex:
(Decide \mkleeneopen{}i < j\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index