---

flow-state-compression(S;T;F;H;start;c) ==
  i,j:Id.
    ((i  S)
     (j  S)
     (s:{s:T List| 0 < ||s||} 
          ((F i j s) = (H i j list_accum(sofar,x.c sofar x;start i;s)))))

---

Definitions :  implies: P  Q,  l_member: (x  l),  Id: Id,  all: x:A. B[x],  set: {x:A| B[x]} ,  list: type List,  less_than: a < b,  natural_number: $n,  length: ||as||,  equal: s = t,  union: left + right,  top: Top,  list_accum: list_accum(x,a.f[x; a];y;l),  apply: f a
FDL editor aliases :  flow-state-compression

---

flow-state-compression(S;T;F;H;start;c)  ==
    \mforall{}i,j:Id.
        ((i  \mmember{}  S)
        {}\mRightarrow{}  (j  \mmember{}  S)
        {}\mRightarrow{}  (\mforall{}s:\{s:T  List|  0  <  ||s||\}  .  ((F  i  j  s)  =  (H  i  j  list\_accum(sofar,x.c  sofar  x;start  i;s)))))


Date html generated: 2010_08_27-AM-09_36_19
Last ObjectModification: 2009_12_16-AM-08_22_07

Home Index