---

{ [A,B,S:Type]. [next:S  A  (S  bag(B))]. [F:S  A  (S?  bag(B))].
  [s:S].
    rec-dataflow(s;s,a.next[s;a])
    = rec-dataflow(inl s ;s,a.case s of inl(s1) => F s1 a | inr(x) => <s, {}>) 
    supposing s:S. a:A.
                let hs,out = F s a 
                in let s2,bs = next s a 
                   in (out = bs)
                       case hs
                        of inl(s') =>
                         s' = s2
                         | inr(z) =>
                         rec-dataflow-halt-state(A;B;s2;s,a.next[s;a]) }

{ Proof }

---

Definitions occuring in Statement :  rec-dataflow-halt-state: rec-dataflow-halt-state(A;B;s0;s,a.next[s; a]),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  dataflow: dataflow(A;B),  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  all: x:A. B[x],  and: P  Q,  unit: Unit,  apply: f a,  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x ,  union: left + right,  universe: Type,  equal: s = t
Definitions :  list: type List,  pi1: fst(t),  corec: corec(T.F[T]),  so_lambda: x.t[x],  pi2: snd(t),  implies: P  Q,  lambda: x.A[x],  limited-type: LimitedType,  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  uiff: uiff(P;Q),  subtype_rel: A r B,  axiom: Ax,  empty-bag: Error :empty-bag,  pair: <a, b>,  inl: inl x ,  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  prop: ,  and: P  Q,  apply: f a,  spread: spread def,  all: x:A. B[x],  uimplies: b supposing a,  universe: Type,  product: x:A  B[x],  function: x:A  B[x],  isect: x:A. B[x],  member: t  T,  uall: [x:A]. B[x],  Auto: Error :Auto,  Complete: Error :Complete,  bag: Error :bag,  dataflow: dataflow(A;B),  CollapseTHEN: Error :CollapseTHEN,  Try: Error :Try,  D: Error :D,  CollapseTHENA: Error :CollapseTHENA,  RepeatFor: Error :RepeatFor,  so_apply: x[s1;s2],  rec-dataflow-halt-state: rec-dataflow-halt-state(A;B;s0;s,a.next[s; a]),  equal: s = t,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  so_lambda: x y.t[x; y],  unit: Unit,  union: left + right,  sq_type: SQType(T),  RepUR: Error :RepUR,  iterate-dataflow: P*(inputs),  dataflow-ap: df(a),  iter_df_nil: iter_df_nil{iter_df_nil_compseq_tag_def:o}(P),  rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def,  nil: [],  void: Void,  subtype: S  T,  top: Top,  let: let,  quotient: x,y:A//B[x; y],  iter_df_cons: iter_df_cons{iter_df_cons_compseq_tag_def:o}(as; a; P),  cons: [car / cdr],  ParallelOp: Error :ParallelOp
Lemmas :  iterate-dataflow_wf,  rec-dataflow_wf,  dataflow-ap_wf,  top_wf,  pi1_wf_top,  subtype_base_sq,  dataflow_wf,  Error :bag_wf,  member_wf,  pi2_wf,  unit_wf,  rec-dataflow-halt-state_wf,  Error :empty-bag_wf,  rec-dataflow-equal,  subtype_rel_wf,  pi1_wf

---

\mforall{}[A,B,S:Type].  \mforall{}[next:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  bag(B))].  \mforall{}[F:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S?  \mtimes{}  bag(B))].  \mforall{}[s:S].
    rec-dataflow(s;s,a.next[s;a])
    =  rec-dataflow(inl  s  ;s,a.case  s  of  inl(s1)  =>  F  s1  a  |  inr(x)  =>  <s,  \{\}>) 
    supposing  \mforall{}s:S.  \mforall{}a:A.
                            let  hs,out  =  F  s  a 
                            in  let  s2,bs  =  next  s  a 
                                  in  (out  =  bs)
                                        \mwedge{}  case  hs
                                            of  inl(s')  =>
                                              s'  =  s2
                                              |  inr(z)  =>
                                              rec-dataflow-halt-state(A;B;s2;s,a.next[s;a])


Date html generated: 2011_08_10-AM-08_20_09
Last ObjectModification: 2011_05_03-PM-02_32_49

Home Index