---

Step * 1 of Lemma merge-int-accum-sq


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)
BY
{ Thin (-2) }

1
1. u : ℤ
2. v : ℤ List
3. as : ℤ List
⊢ merge-int(insert-int(u;as);v) = insert-int(u;merge-int(as;v)) ∈ (ℤ List)

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[as:\mBbbZ{}  List].  (merge-int-accum(as;v)  \msim{}  merge-int(as;v))
4.  as  :  \mBbbZ{}  List
\mvdash{}  merge-int(insert-int(u;as);v)  =  insert-int(u;merge-int(as;v))


By

---

Latex:
Thin  (-2)

---

Home Index