Nuprl Lemma : null-data-stream
[L:Top List]. [P:Top]. (null(data-stream(P;L)) ~ null(L))
Proof not projected
Definitions occuring in Statement :
data-stream: data-stream(P;L),
null: null(as),
uall: [x:A]. B[x],
top: Top,
list: type List,
sqequal: s ~ t
Definitions :
subtype: S 
T,
all: x:A. B[x],
from-upto: [n, m),
bfalse: ff,
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
ycomb: Y,
length: ||as||,
upto: upto(n),
firstn: firstn(n;as),
map: map(f;as),
member: t 
T,
data-stream: data-stream(P;L),
null: null(as),
top: Top,
uall: [x:A]. B[x],
guard: {T},
implies: P 
Q,
uimplies: b supposing a,
sq_type: SQType(T)
Lemmas :
bfalse_wf,
null_wf3,
band_ff_simp,
nat_wf,
map_wf,
null_append,
int_seg_wf,
length_wf,
upto_wf,
map_append_sq,
top_wf,
length_wf_nat,
upto_add_1,
btrue_wf,
bool_subtype_base,
bool_wf,
subtype_base_sq
\mforall{}[L:Top List]. \mforall{}[P:Top]. (null(data-stream(P;L)) \msim{} null(L))
Date html generated:
2012_01_23-AM-11_56_40
Last ObjectModification:
2011_12_03-PM-03_23_22
Home
Index