Nuprl Definition : accum_filter_rel
b = 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 z 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: T List,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
list: T List,
implies: P ⇒ Q,
sublist: L1 ⊆ L2,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
l_member: (x ∈ l),
equal: s = t ∈ T,
list_accum: list_accum
FDL editor aliases :
accum_filter_rel
Latex:
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