---

Step * 1 of Lemma select-last-in-nat-missing_wf


1. max : ℤ
2. missing : ℕ List
3. l-ordered(ℕ;x,y.x < y;missing)
⊢ if in-missing(0;missing) then -1 else 0 fi  ∈ {x:ℤ| 
                                                 ((-1) ≤ x)
                                                 ∧ (x ≤ 0)
                                                 ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
                                                 ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < 0 ⇒ (y ≤ x)))
                                                 ∧ (∀y:ℕ. (y < 0 ⇒ x < y ⇒ (y ∈ missing)))} 
BY
{ (AutoSplit THEN MemTypeCD THEN Auto THEN All(RWO "assert-in-missing-nat-iff") THEN Auto) }

---

Latex:

---

Latex:

1.  max  :  \mBbbZ{}
2.  missing  :  \mBbbN{}  List
3.  l-ordered(\mBbbN{};x,y.x  <  y;missing)
\mvdash{}  if  in-missing(0;missing)  then  -1  else  0  fi    \mmember{}  \{x:\mBbbZ{}| 
                                                                                                  ((-1)  \mleq{}  x)
                                                                                                  \mwedge{}  (x  \mleq{}  0)
                                                                                                  \mwedge{}  ((0  \mleq{}  x)  {}\mRightarrow{}  (\mneg{}(x  \mmember{}  missing)))
                                                                                                  \mwedge{}  (\mforall{}y:\mBbbN{}.  ((\mneg{}(y  \mmember{}  missing))  {}\mRightarrow{}  y  <  0  {}\mRightarrow{}  (y  \mleq{}  x)))
                                                                                                  \mwedge{}  (\mforall{}y:\mBbbN{}.  (y  <  0  {}\mRightarrow{}  x  <  y  {}\mRightarrow{}  (y  \mmember{}  missing)))\} 


By

---

Latex:
(AutoSplit  THEN  MemTypeCD  THEN  Auto  THEN  All(RWO  "assert-in-missing-nat-iff")  THEN  Auto)

---

Home Index