{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [ds:k:n dataflow(A;B[k])].
[F:k:n B[k] C C]. [s:C]. [P:C 
].
(better-feedback-dataflow(n;ds;F;s;x.P[x]) 
dataflow(A;C)) }
{ Proof }
Definitions occuring in Statement :
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
dataflow: dataflow(A;B),
bool: ,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
nat: ,
so_apply: x[s1;s2]
Lemmas :
rec-dataflow_wf,
eval-parallel-dataflow_wf,
int_seg_wf,
ifthenelse_wf,
bool_wf,
dataflow_wf,
nat_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C].
\mforall{}[s:C]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}].
(better-feedback-dataflow(n;ds;F;s;x.P[x]) \mmember{} dataflow(A;C))
Date html generated:
2011_08_10-AM-08_18_38
Last ObjectModification:
2011_06_18-AM-08_31_45
Home
Index