Nuprl Lemma : base-prc_wf
hdr:Name. T:{T:Type| valueall-type(T)} . (base-prc(hdr;T) 
NormalLProgrammable'(T;Base(hdr;T)))
Proof not projected
Definitions occuring in Statement :
base-prc: base-prc(hdr;typ),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
name: Name,
all: x:A. B[x],
member: t T,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Definitions :
so_lambda: 
x.t[x],
sq_exists: 
x:{A| B[x]},
base-prc: base-prc(hdr;typ),
normal-locally-programmable: NormalLProgrammable(A;X),
member: t T,
all: x:A. B[x],
implies: P 
Q,
prop: 
,
vatype: ValueAllType,
dataflow-program: DataflowProgram(A),
spreadn: spread4,
pi1: fst(t),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
and: P 
Q,
base-prog: base-prog(T;hdr),
base-headers-msg-val: Base(hdr;typ),
local-program-at: local-program-at{i:l}(Info;A;X;dfp;x),
ycomb: Y,
subtype: S 
T,
top: Top,
es-le-before: 
loc(e),
map: map(f;as),
so_lambda: x y.t[x; y],
ifthenelse: if b then t else f fi ,
bfalse: ff,
null: null(as),
assert: 
b,
not: 
A,
btrue: tt,
lt_int: i <z j,
bnot: 
b,
le_int: i z j,
length: ||as||,
select: l[i],
pi2: snd(t),
last: last(L),
so_apply: x[s],
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s1;s2]
Lemmas :
name_wf,
valueall-type_wf,
base-headers-msg-val_wf,
Message_wf,
local-program-at_wf,
all_wf,
Id_wf,
subtype_rel_self,
subtype_rel_sets,
bag_wf,
unit_wf2,
subtype_rel_product,
base-prog_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc,
es-loc_wf,
equal_wf,
last_append,
es-before_wf,
map_wf,
data-stream-append,
es-locl_wf,
top_wf,
es-before_wf3,
map_append_sq,
dataflow_subtype,
empty-bag_wf,
cond-msg-body_wf,
it_wf,
rec-dataflow_wf,
es-info_wf,
data-stream_wf,
iterate-dataflow_wf,
false_wf,
null-data-stream,
data-stream-cons
\mforall{}hdr:Name. \mforall{}T:\{T:Type| valueall-type(T)\} . (base-prc(hdr;T) \mmember{} NormalLProgrammable'(T;Base(hdr;T)))
Date html generated:
2012_01_23-PM-12_46_58
Last ObjectModification:
2011_12_14-AM-00_22_27
Home
Index