---

{ [L:Top List]. [ds,F:Top].
    (parallel-dataflow(
     ds;
     F)*(L) ~ parallel-dataflow(
              if null(L) then ds else k.ds k*(L) fi ;
              F)) }

{ Proof }

---

Definitions occuring in Statement :  parallel-dataflow: parallel-dataflow,  iterate-dataflow: P*(inputs),  null: null(as),  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  top: Top,  apply: f a,  lambda: x.A[x],  list: type List,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  parallel-dataflow: parallel-dataflow,  ifthenelse: if b then t else f fi ,  null: null(as),  pi1: fst(t),  member: t  T,  btrue: tt,  bfalse: ff,  top: Top,  all: x:A. B[x],  implies: P  Q,  prop: ,  false: False,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  it:
Lemmas :  top_wf,  null_wf3,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_null,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\mforall{}[L:Top  List].  \mforall{}[ds,F:Top].
    (parallel-dataflow(
      ds;
      F)*(L)  \msim{}  parallel-dataflow(
                        if  null(L)  then  ds  else  \mlambda{}k.ds  k*(L)  fi  ;
                        F))


Date html generated: 2011_08_10-AM-08_15_45
Last ObjectModification: 2011_06_18-AM-08_30_38

Home Index