{ 
[as1,as2:Top List]. [P:Top].
(data-stream(P;as1 @ as2) ~ data-stream(P;as1) @ data-stream(P*(as1);as2)) }
{ Proof }
Definitions occuring in Statement :
data-stream: data-stream(P;L),
iterate-dataflow: P*(inputs),
append: as @ bs,
uall: [x:A]. B[x],
top: Top,
list: type List,
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
append: as @ bs,
member: t 
T,
top: Top,
guard: {T}
Lemmas :
top_wf,
append_wf,
data-stream-cons
\mforall{}[as1,as2:Top List]. \mforall{}[P:Top].
(data-stream(P;as1 @ as2) \msim{} data-stream(P;as1) @ data-stream(P*(as1);as2))
Date html generated:
2011_08_10-AM-08_14_44
Last ObjectModification:
2011_06_18-AM-08_30_08
Home
Index