---

Step * of Lemma sort-int-trivial

∀T:Type. ∀bs:T List.  ((T ⊆r ℤ) ⇒ sorted(bs) ⇒ (sort-int(bs) = bs ∈ (T List)))
BY
{ (Unfold `sort-int` 0
   THEN InductionOnList
   THEN Auto
   THEN Unfold `merge-int` 0
   THEN Reduce 0
   THEN Try (Fold `merge-int` 0)
   THEN Auto
   THEN ∀h:hyp. ((RWO "sorted-cons" h THENA Auto) THEN D h) 
   THEN ThinTrivial
   THEN HypSubst' (-1) 0) }

1
1. T : Type
2. u : T
3. v : T List
4. T ⊆r ℤ
5. sorted(v)
6. (∀z∈v.u ≤ z)
7. merge-int([];v) = v ∈ (T List)
⊢ insert-int(u;v) = [u / v] ∈ (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}bs:T  List.    ((T  \msubseteq{}r  \mBbbZ{})  {}\mRightarrow{}  sorted(bs)  {}\mRightarrow{}  (sort-int(bs)  =  bs))


By

---

Latex:
(Unfold  `sort-int`  0
  THEN  InductionOnList
  THEN  Auto
  THEN  Unfold  `merge-int`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `merge-int`  0)
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((RWO  "sorted-cons"  h  THENA  Auto)  THEN  D  h) 
  THEN  ThinTrivial
  THEN  HypSubst'  (-1)  0)

---

Home Index