---

Step * of Lemma s-insert-sorted

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

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

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

---

Latex:

---

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


By

---

Latex:
InductionOnList\mcdot{}

---

Home Index