---

Step * 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] ≤_lex [u / insert-int(x;v)]
BY
{ (BLemma `intlex-by-length` THEN Auto) }

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

---

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{}  \muparrow{}[x]  \mleq{}\_lex  [u  /  insert-int(x;v)]


By

---

Latex:
(BLemma  `intlex-by-length`  THEN  Auto)

---

Home Index