---

Step * of Lemma isEmpty-nat-missing-prop

∀s:nat-missing-type(). (↑isEmpty-nat-missing(s) ⇐⇒ ∀x:ℕ. (¬↑member-nat-missing(x;s)))
BY
{ (Auto
   THEN (All(RWO "assert-member-nat-missing") THENA Auto)
   THEN All(RepUR ``isEmpty-nat-missing nat-missing-type``)
   THEN Try ((DNot 0 THENA Auto))
   THEN DProdsAndUnions
   THEN DVarSets
   THEN Try ((Unhide THENA Auto))
   THEN AllReduce
   THEN Repeat AllPushDown
   THEN Auto) }

1
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
⊢ m < 0

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

---

Latex:


\mforall{}s:nat-missing-type().  (\muparrow{}isEmpty-nat-missing(s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:\mBbbN{}.  (\mneg{}\muparrow{}member-nat-missing(x;s)))


By

(Auto
  THEN  (All(RWO  "assert-member-nat-missing")  THENA  Auto)
  THEN  All(RepUR  ``isEmpty-nat-missing  nat-missing-type``)
  THEN  Try  ((DNot  0  THENA  Auto))
  THEN  DProdsAndUnions
  THEN  DVarSets
  THEN  Try  ((Unhide  THENA  Auto))
  THEN  AllReduce
  THEN  Repeat  AllPushDown
  THEN  Auto)

---

Home Index