---

Step * 2 of Lemma isEmpty-nat-missing-prop


1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. (∀x∈s1.x < m)@i
6. ∀x:ℕ. (¬((x ≤ m) ∧ (¬(x ∈ s1))))@i
7. m < 0
⊢ s1 = [] ∈ (ℕ List)
BY
{ ((Decide ⌈↑null(s1)⌉⋅ THENA Auto)
   THEN AllPushDown
   THEN (FLemma `member_exists` [-1] THENA Auto)
   THEN ExRepD
   THEN (RWO "l_all_iff" (-6) THENA Auto)
   THEN InstHyp [⌈x⌉] (-6)⋅
   THEN Auto) }

---

Latex:



1.  m  :  \mBbbZ{}@i
2.  (-1)  \mleq{}  m@i
3.  s1  :  \mBbbN{}  List@i
4.  l-ordered(\mBbbN{};x,y.x  <  y;s1)@i
5.  (\mforall{}x\mmember{}s1.x  <  m)@i
6.  \mforall{}x:\mBbbN{}.  (\mneg{}((x  \mleq{}  m)  \mwedge{}  (\mneg{}(x  \mmember{}  s1))))@i
7.  m  <  0
\mvdash{}  s1  =  []


By

((Decide  \mkleeneopen{}\muparrow{}null(s1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  AllPushDown
  THEN  (FLemma  `member\_exists`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "l\_all\_iff"  (-6)  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-6)\mcdot{}
  THEN  Auto)

---

Home Index