Nuprl Definition : bag-diff
bag-diff(eq;bs;as) == bag-accum(r,a.case r of inl(b) => bag-remove1(eq;b;a) | inr(z) => r;inl bs;as)
Definitions occuring in Statement :
bag-remove1: bag-remove1(eq;bs;a),
bag-accum: bag-accum(v,x.f[v; x];init;bs),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x
Definitions occuring in definition :
bag-accum: bag-accum(v,x.f[v; x];init;bs),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
bag-remove1: bag-remove1(eq;bs;a),
inl: inl x
FDL editor aliases :
bag-diff
Latex:
bag-diff(eq;bs;as) ==
bag-accum(r,a.case r of inl(b) => bag-remove1(eq;b;a) | inr(z) => r;inl bs;as)
Date html generated:
2016_05_15-PM-08_04_54
Last ObjectModification:
2015_09_23-AM-08_20_49
Theory : bags_2
Home
Index