{ 
[A:
']. [dfp:DataflowProgram(A)].
(delay-dataflow(df-program-meaning(dfp))
= df-program-meaning(delay-df-program(dfp))) }
{ Proof }
Definitions occuring in Statement :
delay-df-program: delay-df-program(dfp),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
delay-dataflow: delay-dataflow(P),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
universe: Type,
equal: s = t,
bag: bag(T)
Lemmas :
df-program-type_wf,
empty-bag_wf,
dataflow-program_wf,
dataflow_wf,
bag_wf,
uall_wf,
delay-program-meaning
\mforall{}[A:\mBbbU{}']. \mforall{}[dfp:DataflowProgram(A)].
(delay-dataflow(df-program-meaning(dfp)) = df-program-meaning(delay-df-program(dfp)))
Date html generated:
2011_08_16-AM-09_47_50
Last ObjectModification:
2011_06_29-PM-03_32_46
Home
Index