Step
*
of Lemma
no_repeats_iff
No Annotations
∀[T:Type]. ∀[l:T List]. uiff(no_repeats(T;l);∀[x,y:T]. ¬(x = y ∈ T) supposing x before y ∈ l)
BY
{ ((Unfolds ``no_repeats l_before`` 0 THEN Unfold `sublist` 0) THEN Auto') }
1
1. T : Type
2. l : T List
3. ∀[i,j:ℕ]. (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
4. x : T
5. y : T
6. ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
⊢ ¬(x = y ∈ T)
2
1. T : Type
2. l : T List
3. ∀[x,y:T].
¬(x = y ∈ T)
supposing ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
⊢ ¬(l[i] = l[j] ∈ T)
Latex:
Latex:
No Annotations
\mforall{}[T:Type]. \mforall{}[l:T List]. uiff(no\_repeats(T;l);\mforall{}[x,y:T]. \mneg{}(x = y) supposing x before y \mmember{} l)
By
Latex:
((Unfolds ``no\_repeats l\_before`` 0 THEN Unfold `sublist` 0) THEN Auto')
Home
Index