---

{ [A,B,C:Type]. [ms:A List]. [P:dataflow(A;B)]. [Q:dataflow(B;C)].
    (seq-dataflow(P;Q)*(ms) ~ seq-dataflow(P*(ms);Q*(data-stream(P;ms)))) }

{ Proof }

---

Definitions occuring in Statement :  seq-dataflow: seq-dataflow(P;Q),  data-stream: data-stream(P;L),  iterate-dataflow: P*(inputs),  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),  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  seq-dataflow: seq-dataflow(P;Q),  pi1: fst(t),  pi2: snd(t),  decidable: Dec(P),  or: P  Q,  uiff: uiff(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,  iterate-dataflow-append,  data-stream-append,  data-stream_wf,  subtype_rel_list,  data-stream-cons,  length_firstn,  iterate-dataflow_wf,  dataflow-ap_wf,  last_wf,  pos_length2,  non_neg_length,  length_cons

---

\mforall{}[A,B,C:Type].  \mforall{}[ms:A  List].  \mforall{}[P:dataflow(A;B)].  \mforall{}[Q:dataflow(B;C)].
    (seq-dataflow(P;Q)*(ms)  \msim{}  seq-dataflow(P*(ms);Q*(data-stream(P;ms))))


Date html generated: 2011_08_10-AM-08_16_49
Last ObjectModification: 2011_06_18-AM-08_31_11

Home Index