---

Step * 4 1 2 of Lemma remove-nat-missing-prop


1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
7. l-ordered(ℕ;x,y.x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;y;s1))
⊢ (∀x∈insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;y;s1).x < m)
BY
{ ((DVarSets THEN Auto)
   THEN (All(RWO "l_all_iff") THEN Auto)
   THEN (FLemma `member-insert-combine` [-1] THENA Auto)
   THEN DProdsAndUnions
   THEN Try (Complete (Auto'))
   THEN Try ((Reduce (-1) THEN (RWO "l_exists_iff" (-1) THENA Auto) THEN ExRepD THEN Auto'))
   THEN All(RWO "l_all_iff")
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index