---

Step * of Lemma sorted-merge

∀[T:Type]. ∀[bs,as:T List].  sorted(merge(as;bs)) supposing sorted(as) supposing T ⊆r ℤ
BY
{ (InductionOnList
   THEN Unfold `merge` 0
   THEN Reduce 0
   THEN Try (Fold `merge` 0)
   THEN Auto
   THEN BLemma `s-insert-sorted`
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs,as:T  List].    sorted(merge(as;bs))  supposing  sorted(as)  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(InductionOnList
  THEN  Unfold  `merge`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `merge`  0)
  THEN  Auto
  THEN  BLemma  `s-insert-sorted`
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index