---

Step * 2 of Lemma ml_insert_int-sq

.....eq aux..... 
1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]. (ml_insert_int(x;v) ~ insert-int(x;v))
4. x : ℤ
⊢ ml_insert_int(x;[u / v]) ~ insert-int(x;[u / v])
BY
{ (RepUR ``ml_insert_int ml_apply`` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN RepUR ``spreadcons`` 0
   THEN Fold `spreadcons` 0
   THEN Unfold `insert-int` 0
   THEN Reduce 0
   THEN Fold `insert-int` 0
   THEN (CallByValueReduceOn ⌜x⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜v⌝ 0⋅ THENA Auto)
   THEN Fold `ml_apply` 0
   THEN Fold `ml_insert_int` 0
   THEN RWO "3" 0
   THEN Auto) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]. (ml_insert_int(x;v) ~ insert-int(x;v))
4. x : ℤ
⊢ if x <z u + 1 then [x; [u / v]] else [u / insert-int(x;v)] fi 
= if (u) < (x)  then eval y = insert-int(x;v) in [u / y]  else [x; [u / v]]
∈ (ℤ List)

---

Latex:

---

Latex:
.....eq  aux..... 
1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[x:\mBbbZ{}].  (ml\_insert\_int(x;v)  \msim{}  insert-int(x;v))
4.  x  :  \mBbbZ{}
\mvdash{}  ml\_insert\_int(x;[u  /  v])  \msim{}  insert-int(x;[u  /  v])


By

---

Latex:
(RepUR  ``ml\_insert\_int  ml\_apply``  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  RepUR  ``spreadcons``  0
  THEN  Fold  `spreadcons`  0
  THEN  Unfold  `insert-int`  0
  THEN  Reduce  0
  THEN  Fold  `insert-int`  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Fold  `ml\_apply`  0
  THEN  Fold  `ml\_insert\_int`  0
  THEN  RWO  "3"  0
  THEN  Auto)

---

Home Index