Nuprl Lemma : empty-nat-missing-prop
∀x:ℕ. (¬↑member-nat-missing(x;empty-nat-missing()))
Proof
Definitions occuring in Statement :
empty-nat-missing: empty-nat-missing(),
member-nat-missing: member-nat-missing(i;s),
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A
Lemmas :
sq_stable__le,
add_functionality_wrt_le,
add-zero,
le-add-cancel-alt,
le_wf,
not_wf,
assert_wf,
in-missing_wf,
nil_wf,
iff_transitivity,
bnot_wf,
iff_weakening_uiff,
assert_of_band,
assert_of_le_int,
assert_of_bnot,
le_int_wf,
bool_wf,
eqtt_to_assert,
nat_wf
\mforall{}x:\mBbbN{}. (\mneg{}\muparrow{}member-nat-missing(x;empty-nat-missing()))
Date html generated:
2015_07_17-AM-08_21_25
Last ObjectModification:
2015_04_02-PM-05_43_11
Home
Index