Nuprl Definition : accum_filter_rel

accum(z,x.f[z; x],a,{x∈X|P[x]}) ==
  ∀L:T List
    ((L ⊆ X ∧ (∀x:T. ((x ∈ L) ⇐⇒ (x ∈ X) ∧ P[x])))
     (b accumulate (with value and list item x): f[z; x]over list:  Lwith starting value: a) ∈ A))

Definitions occuring in Statement :  sublist: L1 ⊆ L2 l_member: (x ∈ l) list_accum: list_accum list: List all: x:A. B[x] iff: ⇐⇒ Q implies:  Q and: P ∧ Q equal: t ∈ T
Definitions occuring in definition :  list: List implies:  Q sublist: L1 ⊆ L2 all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q l_member: (x ∈ l) equal: t ∈ T list_accum: list_accum
FDL editor aliases :  accum_filter_rel

b  =  accum(z,x.f[z;  x],a,\{x\mmember{}X|P[x]\})  ==
    \mforall{}L:T  List
        ((L  \msubseteq{}  X  \mwedge{}  (\mforall{}x:T.  ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  X)  \mwedge{}  P[x])))
        {}\mRightarrow{}  (b  =  accumulate  (with  value  z  and  list  item  x):  f[z;  x]over  list:    Lwith  starting  value:  a)))

Date html generated: 2016_05_15-PM-04_32_47
Last ObjectModification: 2015_09_23-AM-07_49_10

Theory : general

Home Index