Step
*
1
of Lemma
no_repeats_mu_index
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||L||
5. no_repeats(T;L)
6. L[i] = L[i] ∈ T
7. y : ℕ||L||@i
8. L[i] = L[y] ∈ T
⊢ y = i ∈ ℤ
BY
{ Assert ⌜(L[i] ∈! L)⌝⋅ }
1
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||L||
5. no_repeats(T;L)
6. L[i] = L[i] ∈ T
7. y : ℕ||L||@i
8. L[i] = L[y] ∈ T
⊢ (L[i] ∈! L)
2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||L||
5. no_repeats(T;L)
6. L[i] = L[i] ∈ T
7. y : ℕ||L||@i
8. L[i] = L[y] ∈ T
9. (L[i] ∈! L)
⊢ y = i ∈ ℤ
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : \mBbbN{}||L||
5. no\_repeats(T;L)
6. L[i] = L[i]
7. y : \mBbbN{}||L||@i
8. L[i] = L[y]
\mvdash{} y = i
By
Latex:
Assert \mkleeneopen{}(L[i] \mmember{}! L)\mkleeneclose{}\mcdot{}
Home
Index