---

Step * 1 of Lemma ml_insert_int-sq

.....eq aux..... 
1. x : ℤ
⊢ ml_insert_int(x;[]) ~ insert-int(x;[])
BY
{ (RepUR ``ml_insert_int ml_apply`` 0
   THEN (CallByValueReduceOn ⌜x⌝ 0⋅ THENA Auto)
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  x  :  \mBbbZ{}
\mvdash{}  ml\_insert\_int(x;[])  \msim{}  insert-int(x;[])


By

---

Latex:
(RepUR  ``ml\_insert\_int  ml\_apply``  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index