---

Step * of Lemma insert-int-sorted

No Annotations
∀[T:Type]. ∀[x:T]. ∀[l:T List].  sorted(insert-int(x;l)) supposing sorted(l) supposing T ⊆r ℤ
BY
{ InductionOnList }

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

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[l:T  List].    sorted(insert-int(x;l))  supposing  sorted(l)  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
InductionOnList

---

Home Index