Nuprl Definition : bag-separate
bag-separate(bs) == <bag-mapfilter(λt.outl(t);λt.isl(t);bs), bag-mapfilter(λt.outr(t);λt.(¬bisl(t));bs)>
Definitions occuring in Statement :
bag-mapfilter: bag-mapfilter(f;P;bs),
outr: outr(x),
outl: outl(x),
bnot: ¬bb,
isl: isl(x),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
outl: outl(x),
bag-mapfilter: bag-mapfilter(f;P;bs),
outr: outr(x),
lambda: λx.A[x],
bnot: ¬bb,
isl: isl(x)
FDL editor aliases :
bag-separate
Latex:
bag-separate(bs) ==
<bag-mapfilter(\mlambda{}t.outl(t);\mlambda{}t.isl(t);bs), bag-mapfilter(\mlambda{}t.outr(t);\mlambda{}t.(\mneg{}\msubb{}isl(t));bs)>
Date html generated:
2016_05_15-PM-02_35_27
Last ObjectModification:
2015_09_23-AM-07_39_48
Theory : bags
Home
Index