Nuprl Lemma : length-data-stream
∀[L:Top List]. ∀[P:Top]. (||data-stream(P;L)|| ~ ||L||)
Proof
Definitions occuring in Statement :
data-stream: data-stream(P;L),
length: ||as||,
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
length-map,
int_seg_wf,
length_wf,
upto_wf,
length_upto,
length_wf_nat,
top_wf,
list_wf
Latex:
\mforall{}[L:Top List]. \mforall{}[P:Top]. (||data-stream(P;L)|| \msim{} ||L||)
Date html generated:
2015_07_23-AM-11_06_03
Last ObjectModification:
2015_01_29-AM-00_11_21
Home
Index