Nuprl Lemma : df-opt-prog_wf
[A:Type]. [dfp:DataflowProgram(A)]. [b:bag(df-program-type(dfp))]. (df-opt-prog(dfp;b) 
DataflowProgram(A))
Proof not projected
Definitions occuring in Statement :
df-opt-prog: df-opt-prog(dfp;b),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
uall: [x:A]. B[x],
member: t T,
universe: Type,
bag: bag(T)
Definitions :
true: True,
squash: 
T,
spreadn: spread4,
unit: Unit,
df-opt-prog: df-opt-prog(dfp;b),
member: t T,
dataflow-program: DataflowProgram(A),
uall: [x:A]. B[x],
all: x:A. B[x],
sq_stable: SqStable(P),
implies: P 
Q,
pi1: fst(t),
df-program-type: df-program-type(dfp)
Lemmas :
dataflow-program_wf,
df-program-type_wf,
bag_wf,
bag-null_wf,
ifthenelse_wf,
valueall-type_wf,
equal-valueall-type,
sq_stable__valueall-type,
union-valueall-type,
unit_wf2
\mforall{}[A:Type]. \mforall{}[dfp:DataflowProgram(A)]. \mforall{}[b:bag(df-program-type(dfp))].
(df-opt-prog(dfp;b) \mmember{} DataflowProgram(A))
Date html generated:
2012_01_23-AM-11_58_26
Last ObjectModification:
2011_12_12-PM-06_56_53
Home
Index