Nuprl Definition : flow-state-compression

flow-state-compression(S;T;F;H;start;c) ==
    ((i ∈ S)
     (j ∈ S)
     (∀s:{s:T List| 0 < ||s||} 
          ((F s)
          (H accumulate (with value sofar and list item x): 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: List less_than: a < b top: Top all: x:A. B[x] implies:  Q set: {x:A| B[x]}  apply: a union: left right natural_number: $n equal: t ∈ T
FDL editor aliases :  flow-state-compression flow-state-compression
flow-state-compression(S;T;F;H;start;c)  ==
        ((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:
                          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