{ 
[A,B:Type]. [P:dataflow(A;B)]. [inputs:A List].
(P*(inputs) 
dataflow(A;B)) }
{ Proof }
Definitions occuring in Statement :
iterate-dataflow: P*(inputs),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
iterate-dataflow: P*(inputs),
so_lambda: 
x y.t[x; y],
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_apply: x[s1;s2]
Lemmas :
list_accum_wf,
pi1_wf_top,
dataflow-ap_wf,
dataflow_wf
\mforall{}[A,B:Type]. \mforall{}[P:dataflow(A;B)]. \mforall{}[inputs:A List]. (P*(inputs) \mmember{} dataflow(A;B))
Date html generated:
2011_08_10-AM-08_14_16
Last ObjectModification:
2011_06_18-AM-08_29_50
Home
Index