Nuprl Lemma : data_stream_nil_lemma
∀P:Top. (data-stream(P;[]) ~ [])
Proof
Definitions occuring in Statement :
data-stream: data-stream(P;L),
nil: [],
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions :
select: L[n],
nil: [],
it: ⋅
Lemmas :
top_wf,
list_ind_nil_lemma,
stuck-spread,
base_wf,
length_of_nil_lemma,
iter_df_nil_lemma,
map_nil_lemma
Latex:
\mforall{}P:Top. (data-stream(P;[]) \msim{} [])
Date html generated:
2015_07_23-AM-11_05_58
Last ObjectModification:
2015_01_29-AM-00_11_31
Home
Index