---

Step * 2 2 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)
9. l-ordered(ℕ;x,y.x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1))
⊢ (∀x∈insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1).x < m)
BY
{ ((BLemma `l_all_iff` THEN Auto)
   THEN FLemma `member-insert-combine` [-1]
   THEN Auto
   THEN Reduce (-1)
   THEN DProdsAndUnions
   THEN Auto
   THEN Try (Complete ((RWO "l_all_iff" (-5) THEN Auto)))
   THEN RWO "l_exists_iff" (-1)
   THEN ExRepD
   THEN Auto) }

---

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)
9.  l-ordered(\mBbbN{};x,y.x  <  y;insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;i;s1))
\mvdash{}  (\mforall{}x\mmember{}insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;i;s1).x  <  m)


By

---

Latex:
((BLemma  `l\_all\_iff`  THEN  Auto)
  THEN  FLemma  `member-insert-combine`  [-1]
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  DProdsAndUnions
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "l\_all\_iff"  (-5)  THEN  Auto)))
  THEN  RWO  "l\_exists\_iff"  (-1)
  THEN  ExRepD
  THEN  Auto)

---

Home Index