Nuprl Lemma : feedback-df-prog1_wf
[A:
']. [dfp:DataflowProgram(A)]. [C:Type]. [G:bag(df-program-type(dfp)) 
bag(C) bag(C)]. [P:bag(C) 
].
[buf:bag(C)].
feedback-df-prog1(C;G;P;buf;dfp) 
DataflowProgram(A) supposing valueall-type(C)
Proof not projected
Definitions occuring in Statement :
feedback-df-prog1: feedback-df-prog1(B;G;P;buf;dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
bool: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
so_apply: x[s],
so_apply: x[s1;s2],
true: True,
squash: 
T,
so_lambda: 
x.t[x],
all: x:A. B[x],
pi1: fst(t),
spreadn: spread4,
unit: Unit,
feedback-df-prog1: feedback-df-prog1(B;G;P;buf;dfp),
member: t T,
uimplies: b supposing a,
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
uall: [x:A]. B[x],
sq_stable: SqStable(P),
implies: P 
Q
Lemmas :
it_wf,
ifthenelse_wf,
evalall_wf,
equal-valueall-type,
union-valueall-type,
unit_wf2,
bag-valueall-type,
sq_stable__valueall-type,
product-valueall-type,
df-program-type_wf,
dataflow-program_wf,
bool_wf,
bag_wf,
valueall-type_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[dfp:DataflowProgram(A)]. \mforall{}[C:Type]. \mforall{}[G:bag(df-program-type(dfp)) {}\mrightarrow{} bag(C) {}\mrightarrow{} bag(C)].
\mforall{}[P:bag(C) {}\mrightarrow{} \mBbbB{}]. \mforall{}[buf:bag(C)].
feedback-df-prog1(C;G;P;buf;dfp) \mmember{} DataflowProgram(A) supposing valueall-type(C)
Date html generated:
2012_01_23-PM-12_00_12
Last ObjectModification:
2011_12_14-PM-05_29_59
Home
Index