Nuprl Definition : bag-parts'
bag-parts'(eq;bs;x) ==
if bag-null(bs)
then {[bs]}
else let pts ⟵ bag-parts(eq;bs)
in bag-map(λL.[{} / L];pts) + [L∈pts|((#x in hd(L)) =z 0)]
fi
Definitions occuring in Statement :
bag-parts: bag-parts(eq;bs),
bag-count: (#x in bs),
bag-null: bag-null(bs),
bag-filter: [x∈b|p[x]],
bag-append: as + bs,
bag-map: bag-map(f;bs),
single-bag: {x},
empty-bag: {},
hd: hd(l),
cons: [a / b],
nil: [],
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
bag-null: bag-null(bs),
single-bag: {x},
nil: [],
callbyvalueall: callbyvalueall,
bag-parts: bag-parts(eq;bs),
bag-append: as + bs,
bag-map: bag-map(f;bs),
lambda: λx.A[x],
cons: [a / b],
empty-bag: {},
bag-filter: [x∈b|p[x]],
eq_int: (i =z j),
bag-count: (#x in bs),
hd: hd(l),
natural_number: $n
FDL editor aliases :
bag-parts'
Latex:
bag-parts'(eq;bs;x) ==
if bag-null(bs)
then \{[bs]\}
else let pts \mleftarrow{}{} bag-parts(eq;bs)
in bag-map(\mlambda{}L.[\{\} / L];pts) + [L\mmember{}pts|((\#x in hd(L)) =\msubz{} 0)]
fi
Date html generated:
2016_05_15-PM-08_07_33
Last ObjectModification:
2015_09_23-AM-08_20_55
Theory : bags_2
Home
Index