Nuprl Definition : flow-state-compression

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 accumulate (with value sofar and list item x): c sofar xover list:  swith starting value: start i))
          ∈ (T + Top))))


Definitions occuring in Statement :  Id: Id,  l_member: (x ∈ l),  length: ||as||,  list_accum: list_accum,  list: T List,  less_than: a < b,  top: Top,  all: ∀x:A. B[x],  implies: P ⇒ Q,  set: {x:A| B[x]} ,  apply: f a,  union: left + right,  natural_number: $n,  equal: s = t ∈ T
FDL editor aliases :  flow-state-compression 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 
                          accumulate  (with  value  sofar  and  list  item  x):
                            c  sofar  x
                          over  list:
                              s
                          with  starting  value:
                            start  i)))))


Date html generated: 2015_07_17-AM-08_58_19
Last ObjectModification: 2013_03_25-PM-01_54_20

Home Index