---

Step * of Lemma s-insert-no-repeats

∀[T:Type]. ∀[x:T]. ∀[L:T List].  (no_repeats(T;s-insert(x;L))) supposing (no_repeats(T;L) and sorted(L)) supposing T ⊆r \000Cℤ
BY
{ InductionOnList⋅ }

1
1. T : Type
2. T ⊆r ℤ
3. x : T
⊢ (no_repeats(T;s-insert(x;[]))) supposing (no_repeats(T;[]) and sorted([]))

2
1. T : Type
2. T ⊆r ℤ
3. x : T
4. u : T
5. v : T List
6. (no_repeats(T;s-insert(x;v))) supposing (no_repeats(T;v) and sorted(v))
⊢ (no_repeats(T;s-insert(x;[u / v]))) supposing (no_repeats(T;[u / v]) and sorted([u / v]))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[x:T].  \mforall{}[L:T  List].    (no\_repeats(T;s-insert(x;L)))  supposing  (no\_repeats(T;L)  and  sorted(L)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
InductionOnList\mcdot{}

---

Home Index