{ 
[A,B,C:Type]. [ms:A List]. [P:dataflow(A;B)]. [Q:dataflow(B;C)].
(data-stream(seq-dataflow(P;Q);ms) ~ data-stream(Q;data-stream(P;ms))) }
{ Proof }
Definitions occuring in Statement :
seq-dataflow: seq-dataflow(P;Q),
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
list: type List,
universe: Type,
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
member: t 
T,
all: x:A. B[x],
implies: P 
Q,
guard: {T},
top: Top,
subtype: S 
T,
prop: 
,
le: A 
B,
not: 
A,
false: False,
ge: i 
j ,
uimplies: b supposing a,
nat: 
,
last: last(L),
length: ||as||,
data-stream: data-stream(P;L),
map: map(f;as),
ycomb: Y,
upto: upto(n),
from-upto: [n, m),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
seq-dataflow: seq-dataflow(P;Q),
pi2: snd(t),
decidable: Dec(P),
or: P 
Q,
uiff: uiff(P;Q),
and: P 
Q
Lemmas :
nat_wf,
length_wf_nat,
top_wf,
length_wf1,
dataflow_wf,
le_wf,
decidable__lt,
nat_properties,
ge_wf,
firstn_decomp,
firstn_all,
firstn_wf,
data-stream-append,
data-stream_wf,
subtype_rel_list,
non_neg_length,
length_firstn,
data-stream-cons,
iterate-seq-dataflow,
dataflow-ap_wf,
iterate-dataflow_wf,
last_wf,
pos_length2,
length_cons
\mforall{}[A,B,C:Type]. \mforall{}[ms:A List]. \mforall{}[P:dataflow(A;B)]. \mforall{}[Q:dataflow(B;C)].
(data-stream(seq-dataflow(P;Q);ms) \msim{} data-stream(Q;data-stream(P;ms)))
Date html generated:
2011_08_10-AM-08_16_54
Last ObjectModification:
2011_06_18-AM-08_31_14
Home
Index