---

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


1. s1 : nat-missing-type()@i
2. m : {m:ℤ| (-1) ≤ m} @i
3. ¬(0 ≤ m)
4. s3 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
5. x : ℕ@i
⊢ ↑member-nat-missing(x;s1) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;<m, s3>))
BY
{ (Auto
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN DVarSets
   THEN (Unhide THENA Auto)
   THEN RWO "assert-member-nat-missing" (-1)
   THEN AllReduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  s1  :  nat-missing-type()@i
2.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\}  @i
3.  \mneg{}(0  \mleq{}  m)
4.  s3  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\}  @i
5.  x  :  \mBbbN{}@i
\mvdash{}  \muparrow{}member-nat-missing(x;s1)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  (\muparrow{}member-nat-missing(x;<m,  s3>))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  DVarSets
  THEN  (Unhide  THENA  Auto)
  THEN  RWO  "assert-member-nat-missing"  (-1)
  THEN  AllReduce
  THEN  Auto)

---

Home Index