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. Type
2. T ⊆r ℤ
3. T
⊢ sorted(insert-int(x;[])) supposing sorted([])

2
1. Type
2. T ⊆r ℤ
3. T
4. T
5. 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