---

Step * 2 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 : ℤ
⊢ 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)
BY
{ (SplitOnConclITE THEN Auto THEN (Decide ⌜u < x⌝⋅ THENA Auto) THEN Reduce 0 THEN Auto) }

1
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)

---

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{}
\mvdash{}  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]]


By

---

Latex:
(SplitOnConclITE  THEN  Auto  THEN  (Decide  \mkleeneopen{}u  <  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index