{ 
[A,B,C:Type]. [P:dataflow(A;B)]. [Q:dataflow(B;C)].
(seq-dataflow(P;Q) 
dataflow(A;C)) }
{ Proof }
Definitions occuring in Statement :
seq-dataflow: seq-dataflow(P;Q),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
seq-dataflow: seq-dataflow(P;Q),
so_lambda: 
x y.t[x; y],
so_apply: x[s1;s2]
Lemmas :
rec-dataflow_wf,
dataflow-ap_wf,
dataflow_wf
\mforall{}[A,B,C:Type]. \mforall{}[P:dataflow(A;B)]. \mforall{}[Q:dataflow(B;C)]. (seq-dataflow(P;Q) \mmember{} dataflow(A;C))
Date html generated:
2011_08_10-AM-08_16_44
Last ObjectModification:
2011_06_18-AM-08_31_08
Home
Index