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

Latex:
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: 2016_05_16-AM-10_07_08 Last ObjectModification: 2013_03_25-PM-01_54_20 Theory : new!event-ordering Home Index