{ 
[A,B:Type]. [f:A 
B]. (stateless-dataflow(m.f[m]) 
dataflow(A;B)) }
{ Proof }
Definitions occuring in Statement :
stateless-dataflow: stateless-dataflow(m.f[m]),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
stateless-dataflow: stateless-dataflow(m.f[m]),
so_apply: x[s]
Lemmas :
ycomb_wf_dataflow
\mforall{}[A,B:Type]. \mforall{}[f:A {}\mrightarrow{} B]. (stateless-dataflow(m.f[m]) \mmember{} dataflow(A;B))
Date html generated:
2011_08_10-AM-08_13_47
Last ObjectModification:
2011_06_18-AM-08_29_33
Home
Index