### Nuprl Lemma : union-nat-missing-pos-prop

`∀s1:nat-missing-type(). ∀max:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} . ∀x:ℕ.`
`  (↑member-nat-missing(x;union-nat-missing-pos(s1;max;missing))`
`  `⇐⇒` (↑member-nat-missing(x;s1)) ∨ ((x ≤ max) ∧ (¬(x ∈ missing))))`

Proof

Definitions occuring in Statement :  union-nat-missing-pos: `union-nat-missing-pos(s1;max;missing)` member-nat-missing: `member-nat-missing(i;s)` nat-missing-type: `nat-missing-type()` l_member: `(x ∈ l)` list: `T List` nat: `ℕ` assert: `↑b` less_than: `a < b` le: `A ≤ B` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` l-ordered: `l-ordered(T;x,y.R[x; y];L)`
Lemmas :  iff_wf assert_wf member-nat-missing_wf union-nat-missing-pos_wf decidable__le subtract_wf false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_wf or_wf not_wf l_member_wf set_wf less_than_wf primrec-wf2 nat_wf list_wf l-ordered_wf nat-missing-type_wf primrec1_lemma in-missing_wf subtype_rel_list bool_wf eqtt_to_assert assert-in-missing-nat-iff le_antisymmetry squash_wf true_wf iff_weakening_equal assert-member-nat-missing eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot sq_stable__le le_weakening equal-wf-T-base add-nat-missing-prop add-nat-missing_wf primrec-unroll-1 decidable__lt general_arith_equation1 trivial-int-eq1 le_weakening2 le-add-cancel2 decidable__equal_int int_subtype_base not-equal-2 and_wf
\mforall{}s1:nat-missing-type().  \mforall{}max:\mBbbN{}.  \mforall{}missing:\{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  .  \mforall{}x:\mBbbN{}.
(\muparrow{}member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  ((x  \mleq{}  max)  \mwedge{}  (\mneg{}(x  \mmember{}  missing))))

Date html generated: 2015_07_17-AM-08_21_35
Last ObjectModification: 2015_04_02-PM-05_43_20

Home Index