---

Step * 2 1 of Lemma remove-nat-missing_wf


1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
⊢ l-ordered(ℕ;x,y.x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1))
BY
{ (RWO "l-ordered-is-sorted-by" 0 THENA Auto) }

1
1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
⊢ sorted-by(λx,y. x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1))

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  \mneg{}m  <  i
4.  i  \mneq{}  m
5.  (-1)  \mleq{}  m
6.  s1  :  \mBbbN{}  List
7.  l-ordered(\mBbbN{};x,y.x  <  y;s1)
8.  (\mforall{}x\mmember{}s1.x  <  m)
\mvdash{}  l-ordered(\mBbbN{};x,y.x  <  y;insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;i;s1))


By

---

Latex:
(RWO  "l-ordered-is-sorted-by"  0  THENA  Auto)

---

Home Index