Nuprl Lemma : df-program-meaning_wf
[A:
']. [dfp:DataflowProgram(A)]. (df-program-meaning(dfp) 
dataflow(A;bag(df-program-type(dfp))))
Proof not projected
Definitions occuring in Statement :
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
member: t T,
universe: Type,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
member: t T,
df-program-type: df-program-type(dfp),
df-program-meaning: df-program-meaning(dfp),
pi1: fst(t),
spreadn: spread4,
so_lambda: 
x y.t[x; y],
dataflow-program: DataflowProgram(A),
so_apply: x[s1;s2]
Lemmas :
rec-dataflow_wf,
unit_wf2,
bag_wf,
empty-bag_wf,
dataflow-program_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[dfp:DataflowProgram(A)].
(df-program-meaning(dfp) \mmember{} dataflow(A;bag(df-program-type(dfp))))
Date html generated:
2012_01_23-AM-11_58_22
Last ObjectModification:
2011_12_28-PM-12_25_40
Home
Index