Nuprl Lemma : standard-ds_wf
StandardDS ∈ DS({1..6-})
Proof
Definitions occuring in Statement :
standard-ds: StandardDS,
discrete_struct: DS(A),
int_seg: {i..j-},
member: t ∈ T,
natural_number: $n
Lemmas :
eq_int_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
IdLnk_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
Id_wf,
int_seg_wf,
idlnk-deq_wf,
deq_wf,
id-deq_wf
StandardDS \mmember{} DS(\{1..6\msupminus{}\})
Date html generated:
2015_07_17-AM-09_13_49
Last ObjectModification:
2015_01_28-AM-07_55_01
Home
Index