---

Step * 2 of Lemma insert-int-lex


1. u : ℤ
2. v : ℤ List
3. ∀bs:ℤ List. ∀x:ℤ.  ((↑v ≤_lex bs) ⇒ (↑insert-int(x;v) ≤_lex insert-int(x;bs)))
4. x : ℤ
5. ↑[u / v] ≤_lex []
6. u < x
⊢ ↑[u / insert-int(x;v)] ≤_lex [x]
BY
{ ((FLemma `intlex-length` [-2] THENA Auto) THEN Reduce (-1) THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((FLemma  `intlex-length`  [-2]  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto')

---

Home Index