---

Step * of Lemma assert-in-missing-nat-iff

∀i:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} .  (↑in-missing(i;missing) ⇐⇒ (i ∈ missing))
BY
{ (Auto
   THEN Try ((BLemma `assert-in-missing-nat` THEN Auto))
   THEN DVarSets
   THEN (Unhide THENA Auto)
   THEN ListInd 2
   THEN RW ListC 0
   THEN Auto
   THEN RepUR ``in-missing`` 0
   THEN Fold `in-missing` 0
   THEN AllPushDown
   THEN DProdsAndUnions
   THEN Auto
   THEN Try ((InstHyp [⌈i⌉] (-2)⋅ THEN Auto))
   THEN OrRight
   THEN Auto) }

---

Latex:


\mforall{}i:\mBbbN{}.  \mforall{}missing:\{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  .    (\muparrow{}in-missing(i;missing)  \mLeftarrow{}{}\mRightarrow{}  (i  \mmember{}  missing))


By

(Auto
  THEN  Try  ((BLemma  `assert-in-missing-nat`  THEN  Auto))
  THEN  DVarSets
  THEN  (Unhide  THENA  Auto)
  THEN  ListInd  2
  THEN  RW  ListC  0
  THEN  Auto
  THEN  RepUR  ``in-missing``  0
  THEN  Fold  `in-missing`  0
  THEN  AllPushDown
  THEN  DProdsAndUnions
  THEN  Auto
  THEN  Try  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto))
  THEN  OrRight
  THEN  Auto)

---

Home Index