{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [P:C 
].
[F:k:n B[k] C C]. [L:A List]. [ds:k:n dataflow(A;B[k])].
[s:C].
(data-stream(better-feedback-dataflow(n;ds;F;s;x.P[x]);L)
= data-stream(feedback-dataflow(ds;
F;s;x.P[x]);L)) }
{ Proof }
Definitions occuring in Statement :
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
feedback-dataflow: feedback-dataflow,
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
bool: ,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
member: t 
T,
all: x:A. B[x],
top: Top,
subtype: S 
T,
better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),
feedback-dataflow: feedback-dataflow,
pi2: snd(t),
let: let,
implies: P 
Q,
so_lambda: 
x.t[x],
prop: 
,
and: P 
Q,
pi1: fst(t),
so_lambda: x y.t[x; y],
squash: 
T,
true: True,
rev_implies: P 
Q,
iff: P Q,
nat: ,
so_apply: x[s1;s2]
Lemmas :
int_seg_wf,
dataflow_wf,
bool_wf,
nat_wf,
top_wf,
data-stream-cons,
eval-parallel-dataflow-property,
eval-parallel-dataflow_wf,
pi1_wf_top,
dataflow-ap_wf,
dataflow-out_wf,
nat_properties,
pi2_wf,
rec-dataflow_wf,
squash_wf,
true_wf,
ifthenelse_wf,
data-stream_wf,
feedback-dataflow_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[P:C {}\mrightarrow{} \mBbbB{}]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[L:A List].
\mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[s:C].
(data-stream(better-feedback-dataflow(n;ds;F;s;x.P[x]);L)
= data-stream(feedback-dataflow(ds;
F;s;x.P[x]);L))
Date html generated:
2011_08_10-AM-08_18_52
Last ObjectModification:
2011_06_18-AM-08_31_51
Home
Index