---

Step * of Lemma insert-int-lex

No Annotations
∀as,bs:ℤ List. ∀x:ℤ.  ((↑as ≤_lex bs) ⇒ (↑insert-int(x;as) ≤_lex insert-int(x;bs)))
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Auto
   THEN Unfold `insert-int` 0
   THEN Reduce 0
   THEN Try ((Fold `insert-int` 0 THEN (CallByValueReduce 0 THENA Auto) THEN Repeat (AutoSplit)))) }

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] ≤_lex [u / insert-int(x;v)]

2
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]

3
1. u : ℤ
2. v : ℤ List
3. ∀bs:ℤ List. ∀x:ℤ.  ((↑v ≤_lex bs) ⇒ (↑insert-int(x;v) ≤_lex insert-int(x;bs)))
4. u1 : ℤ
5. v1 : ℤ List
6. ∀x:ℤ. ((↑[u / v] ≤_lex v1) ⇒ (↑insert-int(x;[u / v]) ≤_lex insert-int(x;v1)))
7. x : ℤ
8. ↑[u / v] ≤_lex [u1 / v1]
9. u < x
10. u1 < x
⊢ ↑[u / insert-int(x;v)] ≤_lex [u1 / insert-int(x;v1)]

4
1. u : ℤ
2. v : ℤ List
3. ∀bs:ℤ List. ∀x:ℤ.  ((↑v ≤_lex bs) ⇒ (↑insert-int(x;v) ≤_lex insert-int(x;bs)))
4. u1 : ℤ
5. v1 : ℤ List
6. ∀x:ℤ. ((↑[u / v] ≤_lex v1) ⇒ (↑insert-int(x;[u / v]) ≤_lex insert-int(x;v1)))
7. x : ℤ
8. ¬u1 < x
9. ↑[u / v] ≤_lex [u1 / v1]
10. u < x
⊢ ↑[u / insert-int(x;v)] ≤_lex [x; [u1 / v1]]

5
1. u : ℤ
2. v : ℤ List
3. ∀bs:ℤ List. ∀x:ℤ.  ((↑v ≤_lex bs) ⇒ (↑insert-int(x;v) ≤_lex insert-int(x;bs)))
4. u1 : ℤ
5. v1 : ℤ List
6. ∀x:ℤ. ((↑[u / v] ≤_lex v1) ⇒ (↑insert-int(x;[u / v]) ≤_lex insert-int(x;v1)))
7. x : ℤ
8. ¬u < x
9. ↑[u / v] ≤_lex [u1 / v1]
10. u1 < x
⊢ ↑[x; [u / v]] ≤_lex [u1 / insert-int(x;v1)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}as,bs:\mBbbZ{}  List.  \mforall{}x:\mBbbZ{}.    ((\muparrow{}as  \mleq{}\_lex  bs)  {}\mRightarrow{}  (\muparrow{}insert-int(x;as)  \mleq{}\_lex  insert-int(x;bs)))


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Auto
  THEN  Unfold  `insert-int`  0
  THEN  Reduce  0
  THEN  Try  ((Fold  `insert-int`  0  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  Repeat  (AutoSplit))))

---

Home Index