Nuprl Lemma : mk-set-nat-missing_wf
mk-set-nat-missing() ∈ set-sig{i:l}(ℕ)
Proof
Definitions occuring in Statement :
mk-set-nat-missing: mk-set-nat-missing(),
set-sig: set-sig{i:l}(Item),
nat: ℕ,
member: t ∈ T
Lemmas :
mk-set_wf,
nat_wf,
product-valueall-type,
le_wf,
list_wf,
l-ordered_wf,
less_than_wf,
l_all_wf2,
l_member_wf,
set-valueall-type,
int-valueall-type,
list-valueall-type,
set_wf,
valueall-type_wf,
nat-missing-type_wf,
member-nat-missing_wf,
empty-nat-missing-prop,
assert_wf,
empty-nat-missing_wf,
all_wf,
not_wf,
isEmpty-nat-missing-prop,
iff_wf,
singleton-nat-missing-prop,
singleton-nat-missing_wf,
equal_wf,
add-nat-missing-prop,
add-nat-missing_wf,
or_wf,
union-nat-missing-prop,
remove-nat-missing-prop,
remove-nat-missing_wf
mk-set-nat-missing() \mmember{} set-sig\{i:l\}(\mBbbN{})
Date html generated:
2015_07_17-AM-08_21_58
Last ObjectModification:
2015_04_02-PM-05_43_29
Home
Index