---

Step * of Lemma assert-member-nat-missing

∀[i:ℕ]. ∀[s:nat-missing-type()].  (↑member-nat-missing(i;s) ⇐⇒ (i ≤ (fst(s))) ∧ (¬(i ∈ snd(s))))
BY
{ (RepUR ``nat-missing-type member-nat-missing`` 0
   THEN Auto
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Repeat (AllPushDown)
   THEN Auto
   THEN All(RWO "assert-in-missing-nat-iff")
   THEN Auto) }

---

Latex:


\mforall{}[i:\mBbbN{}].  \mforall{}[s:nat-missing-type()].    (\muparrow{}member-nat-missing(i;s)  \mLeftarrow{}{}\mRightarrow{}  (i  \mleq{}  (fst(s)))  \mwedge{}  (\mneg{}(i  \mmember{}  snd(s))))


By

(RepUR  ``nat-missing-type  member-nat-missing``  0
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Repeat  (AllPushDown)
  THEN  Auto
  THEN  All(RWO  "assert-in-missing-nat-iff")
  THEN  Auto)

---

Home Index