---

Step * 1 1 of Lemma insert-int-lex


1. u : ℤ
2. v : ℤ List
3. ∀x:ℤ. ((↑[] ≤_lex v) ⇒ (↑insert-int(x;[]) ≤_lex insert-int(x;v)))
4. x : ℤ
5. ↑[] ≤_lex [u / v]
6. u < x
⊢ ||[x]|| < ||[u / insert-int(x;v)]||
BY
{ (Reduce 0 THEN RWO "length-insert-int" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}x:\mBbbZ{}.  ((\muparrow{}[]  \mleq{}\_lex  v)  {}\mRightarrow{}  (\muparrow{}insert-int(x;[])  \mleq{}\_lex  insert-int(x;v)))
4.  x  :  \mBbbZ{}
5.  \muparrow{}[]  \mleq{}\_lex  [u  /  v]
6.  u  <  x
\mvdash{}  ||[x]||  <  ||[u  /  insert-int(x;v)]||


By

---

Latex:
(Reduce  0  THEN  RWO  "length-insert-int"  0  THEN  Auto)

---

Home Index