Nuprl Lemma : null-data-stream
∀[L:Top List]. ∀[P:Top]. (null(data-stream(P;L)) ~ null(L))
Proof
Definitions occuring in Statement :
data-stream: data-stream(P;L),
null: null(as),
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
top_wf,
list-cases,
list_ind_nil_lemma,
stuck-spread,
base_wf,
length_of_nil_lemma,
null_nil_lemma,
iter_df_nil_lemma,
map_nil_lemma,
product_subtype_list,
length_of_cons_lemma,
null_cons_lemma,
null_wf3,
map_wf,
int_seg_wf,
upto_wf,
bfalse_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
list_wf,
upto_add_1,
map_append_sq,
null_append,
map_cons_lemma,
band_ff_simp,
iff_weakening_equal
Latex:
\mforall{}[L:Top List]. \mforall{}[P:Top]. (null(data-stream(P;L)) \msim{} null(L))
Date html generated:
2015_07_23-AM-11_06_05
Last ObjectModification:
2015_02_04-PM-04_49_27
Home
Index