---

Step * 2 1 1 of Lemma ml_insert_int-sq


1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]. (ml_insert_int(x;v) ~ insert-int(x;v))
4. x : ℤ
5. (u + 1) ≤ x
6. u < x
⊢ [u / insert-int(x;v)] = eval y = insert-int(x;v) in [u / y] ∈ (ℤ List)
BY
{ (RepUR ``let`` 0 THEN CallByValueReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[x:\mBbbZ{}].  (ml\_insert\_int(x;v)  \msim{}  insert-int(x;v))
4.  x  :  \mBbbZ{}
5.  (u  +  1)  \mleq{}  x
6.  u  <  x
\mvdash{}  [u  /  insert-int(x;v)]  =  eval  y  =  insert-int(x;v)  in  [u  /  y]


By

---

Latex:
(RepUR  ``let``  0  THEN  CallByValueReduce  0  THEN  Auto)

---

Home Index