Nuprl Definition : bag-all
bag-all(x.p[x];bs) == bag-reduce(x,y.x ∧b y;tt;bag-map(λx.p[x];bs))
Definitions occuring in Statement :
bag-reduce: bag-reduce(x,y.f[x; y];zero;bs)
,
bag-map: bag-map(f;bs)
,
band: p ∧b q
,
btrue: tt
,
lambda: λx.A[x]
Definitions occuring in definition :
bag-reduce: bag-reduce(x,y.f[x; y];zero;bs)
,
band: p ∧b q
,
btrue: tt
,
bag-map: bag-map(f;bs)
,
lambda: λx.A[x]
FDL editor aliases :
bag-all
Latex:
bag-all(x.p[x];bs) == bag-reduce(x,y.x \mwedge{}\msubb{} y;tt;bag-map(\mlambda{}x.p[x];bs))
Date html generated:
2016_05_15-PM-02_34_24
Last ObjectModification:
2015_09_23-AM-07_39_37
Theory : bags
Home
Index