---

Step * of Lemma merge-int-lex

∀cs,as,bs:ℤ List.  ((↑as ≤_lex bs) ⇒ (↑merge-int(as;cs) ≤_lex merge-int(bs;cs)))
BY
{ (InductionOnList
   THEN Unfold `merge-int` 0
   THEN Reduce 0
   THEN Try (Fold `merge-int` 0)
   THEN Auto
   THEN (FHyp 3 [-1] THENA Auto)) }

1
1. u : ℤ@i
2. v : ℤ List@i
3. ∀as,bs:ℤ List.  ((↑as ≤_lex bs) ⇒ (↑merge-int(as;v) ≤_lex merge-int(bs;v)))@i
4. as : ℤ List@i
5. bs : ℤ List@i
6. ↑as ≤_lex bs@i
7. ↑merge-int(as;v) ≤_lex merge-int(bs;v)
⊢ ↑insert-int(u;merge-int(as;v)) ≤_lex insert-int(u;merge-int(bs;v))

---

Latex:

---

Latex:
\mforall{}cs,as,bs:\mBbbZ{}  List.    ((\muparrow{}as  \mleq{}\_lex  bs)  {}\mRightarrow{}  (\muparrow{}merge-int(as;cs)  \mleq{}\_lex  merge-int(bs;cs)))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `merge-int`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `merge-int`  0)
  THEN  Auto
  THEN  (FHyp  3  [-1]  THENA  Auto))

---

Home Index