---

Step * 1 of Lemma remove-nat-missing-prop


1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. y = m ∈ ℤ
6. s1 = [] ∈ (ℕ List)
⊢ ↑member-nat-missing(x;<m - 1, []>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))
BY
{ (RWO "assert-member-nat-missing" 0 THEN Reduce 0 THEN Auto THEN MemTypeCD THEN Try (RW ListC 0) THEN Auto) }

---

Latex:



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


By

(RWO  "assert-member-nat-missing"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Try  (RW  ListC  0)
  THEN  Auto)

---

Home Index