### Nuprl Lemma : select-last-in-nat-missing_wf

`∀[max:ℕ]. ∀[missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} ].`
`  (select-last-in-nat-missing(max;missing) ∈ {x:ℤ| `
`                                              ((-1) ≤ x)`
`                                              ∧ (x ≤ max)`
`                                              ∧ ((0 ≤ x) `` (¬(x ∈ missing)))`
`                                              ∧ (∀y:ℕ. ((¬(y ∈ missing)) `` y < max `` (y ≤ x)))`
`                                              ∧ (∀y:ℕ. (y < max `` x < y `` (y ∈ missing)))} )`

Proof

Definitions occuring in Statement :  select-last-in-nat-missing: `select-last-in-nat-missing(max;missing)` l_member: `(x ∈ l)` list: `T List` nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` minus: `-n` natural_number: `\$n` int: `ℤ` l-ordered: `l-ordered(T;x,y.R[x; y];L)`
\mforall{}[max:\mBbbN{}].  \mforall{}[missing:\{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  ].
(select-last-in-nat-missing(max;missing)  \mmember{}  \{x:\mBbbZ{}|
((-1)  \mleq{}  x)
\mwedge{}  (x  \mleq{}  max)
\mwedge{}  ((0  \mleq{}  x)  {}\mRightarrow{}  (\mneg{}(x  \mmember{}  missing)))
\mwedge{}  (\mforall{}y:\mBbbN{}.  ((\mneg{}(y  \mmember{}  missing))  {}\mRightarrow{}  y  <  max  {}\mRightarrow{}  (y  \mleq{}  x)))
\mwedge{}  (\mforall{}y:\mBbbN{}.  (y  <  max  {}\mRightarrow{}  x  <  y  {}\mRightarrow{}  (y  \mmember{}  missing)))\}  )

Date html generated: 2015_07_17-AM-08_21_43
Last ObjectModification: 2015_04_02-PM-05_43_25

Home Index