---

Step * of Lemma merge-int-accum-sq

∀[bs,as:ℤ List].  (merge-int-accum(as;bs) ~ merge-int(as;bs))
BY
{ (InductionOnList
   THEN RepUR ``merge-int-accum merge-int`` 0
   THEN RecUnfold `eager-accum` 0
   THEN Reduce 0
   THEN Auto
   THEN Fold `merge-int-accum` 0
   THEN Fold `merge-int` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RWO "3" 0 THENA Auto)) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[as:ℤ List]. (merge-int-accum(as;v) ~ merge-int(as;v))
4. as : ℤ List
⊢ merge-int(insert-int(u;as);v) = insert-int(u;merge-int(as;v)) ∈ (ℤ List)

---

Latex:

---

Latex:
\mforall{}[bs,as:\mBbbZ{}  List].    (merge-int-accum(as;bs)  \msim{}  merge-int(as;bs))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``merge-int-accum  merge-int``  0
  THEN  RecUnfold  `eager-accum`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Fold  `merge-int-accum`  0
  THEN  Fold  `merge-int`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RWO  "3"  0  THENA  Auto))

---

Home Index