---

{ [Info:Type]. [A,S,T:{S:Type| valueall-type(S)} ]. [sx:S]. [sy:T].
  [nxtx:S  Info  (S?  bag(A))]. [nxty:T  Info  (T?  bag(Top))].
    (until-prog(A;S;T;sx;sy;nxtx;nxty)  DataflowProgram(Info)) }

{ Proof }

---

Definitions occuring in Statement :  until-prog: until-prog(A;S;T;sx;sy;nxtx;nxty),  dataflow-program: DataflowProgram(A),  uall: [x:A]. B[x],  top: Top,  unit: Unit,  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  universe: Type,  bag: bag(T),  valueall-type: valueall-type(T)
Definitions :  CollapseTHEN: Error :CollapseTHEN,  Unfold: Error :Unfold,  member: t  T,  isect: x:A. B[x],  uall: [x:A]. B[x],  set: {x:A| B[x]} ,  universe: Type,  valueall-type: valueall-type(T),  equal: s = t,  dataflow-program: DataflowProgram(A),  function: x:A  B[x],  product: x:A  B[x],  bag: bag(T),  union: left + right,  unit: Unit,  top: Top,  until-prog: until-prog(A;S;T;sx;sy;nxtx;nxty),  axiom: Ax,  all: x:A. B[x],  bool: ,  pair: <a, b>,  subtype_rel: A r B,  uiff: uiff(P;Q),  and: P  Q,  uimplies: b supposing a,  less_than: a < b,  not: A,  ge: i  j ,  le: A  B,  strong-subtype: strong-subtype(A;B),  subtype: S  T,  inl: inl x ,  lambda: x.A[x],  evalall: evalall(t),  spread: spread def,  apply: f a,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  empty-bag: {},  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  inr: inr x ,  it: ,  fpf: a:A fp-> B[a],  eclass: EClass(A[eo; e]),  list: type List,  implies: P  Q,  so_lambda: x.t[x],  b-union: A  B,  tunion: x:A.B[x],  quotient: x,y:A//B[x; y],  rec: rec(x.A[x]),  atom: Atom,  int: ,  atom: Atom$n,  natural_number: $n,  assert: b,  l_member: (x  l),  guard: {T},  or: P  Q,  so_apply: x[s]
Lemmas :  bag-valueall-type,  equal-valueall-type,  union-valueall-type,  product-valueall-type,  subtype_rel_wf,  member_wf,  it_wf,  bag-null_wf,  ifthenelse_wf,  empty-bag_wf,  evalall_wf,  top_wf,  unit_wf,  bag_wf,  valueall-type_wf

---

\mforall{}[Info:Type].  \mforall{}[A,S,T:\{S:Type|  valueall-type(S)\}  ].  \mforall{}[sx:S].  \mforall{}[sy:T].  \mforall{}[nxtx:S
                                                                                                                                                        {}\mrightarrow{}  Info
                                                                                                                                                        {}\mrightarrow{}  (S?  \mtimes{}  bag(A))].
\mforall{}[nxty:T  {}\mrightarrow{}  Info  {}\mrightarrow{}  (T?  \mtimes{}  bag(Top))].
    (until-prog(A;S;T;sx;sy;nxtx;nxty)  \mmember{}  DataflowProgram(Info))


Date html generated: 2011_08_16-PM-06_16_59
Last ObjectModification: 2011_06_16-PM-03_42_29

Home Index