Nuprl Lemma : delay-program-meaning
[A:
']. [dfp:DataflowProgram(A)]. [init:bag(df-program-type(dfp))].
(seq-dataflow(df-program-meaning(dfp);buffer-dataflow(init;x.0 <z bag-size(x)))
= df-program-meaning(Prior dfp
init: init))
Proof not projected
Definitions occuring in Statement :
delay-program: delay-program,
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
buffer-dataflow: buffer-dataflow(s;x.P[x]),
seq-dataflow: seq-dataflow(P;Q),
dataflow: dataflow(A;B),
lt_int: i <z j,
uall: [x:A]. B[x],
natural_number: $n,
universe: Type,
equal: s = t,
bag-size: bag-size(bs),
bag: bag(T)
Definitions :
all: x:A. B[x],
so_lambda: 
x.t[x],
spreadn: spread4,
true: True,
squash: 
T,
so_lambda: x y.t[x; y],
pi1: fst(t),
unit: Unit,
member: t 
T,
delay-program: delay-program,
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
uall: [x:A]. B[x],
bfalse: ff,
btrue: tt,
assert: 
b,
outl: outl(x),
subtype: S 
T,
top: Top,
and: P 
Q,
pi2: snd(t),
implies: P 
Q,
prop: 
,
isl: isl(x),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
bnot: 
b,
band: p q,
let: let,
guard: {T},
exposed-bfalse: exposed-bfalse,
sq_stable: SqStable(P),
nat: 
,
so_apply: x[s],
uimplies: b supposing a,
so_apply: x[s1;s2],
dataflow-program: DataflowProgram(A),
uiff: uiff(P;Q),
bool: 
,
it: 
Lemmas :
dataflow-program_wf,
df-program-type_wf,
bag-valueall-type,
equal-valueall-type,
sq_stable__valueall-type,
union-valueall-type,
product-valueall-type,
lt_int_wf,
it_wf,
nat_wf,
bag-size_wf,
eq_int_wf,
isl_wf,
bnot_wf,
band_wf,
ifthenelse_wf,
let_wf,
evalall-equal,
rec-dataflow_wf,
bag_wf,
dataflow_wf,
true_wf,
squash_wf,
equal_wf,
empty-bag_wf,
unit_wf2,
delay-equiv1,
assert_wf,
outl_wf,
pi2_wf,
pi1_wf_top,
rec-dataflow-equal,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
le_wf,
le_int_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
assert_of_eq_int,
assert_of_lt_int,
eqtt_to_assert,
less_than_wf,
uiff_transitivity,
bool_wf,
equal-unit
\mforall{}[A:\mBbbU{}']. \mforall{}[dfp:DataflowProgram(A)]. \mforall{}[init:bag(df-program-type(dfp))].
(seq-dataflow(df-program-meaning(dfp);buffer-dataflow(init;x.0 <z bag-size(x)))
= df-program-meaning(Prior dfp
init: init))
Date html generated:
2012_01_23-PM-12_00_57
Last ObjectModification:
2011_12_13-AM-10_34_16
Home
Index