Nuprl Definition : bag-parts

bag-parts(eq;bs) ==
  fix((λbag-parts,bs. let splits ⟵ bag-partitions(eq;bs)
                      in ⋃p∈splits.if bag-null(fst(p)) then {}
                         if bag-null(snd(p)) then {[fst(p)]}
                         else let parts ⟵ bag-parts (snd(p))
                              in bag-map(λL.[fst(p) / L];parts)
                         fi )) 
  bs


Definitions occuring in Statement :  bag-partitions: bag-partitions(eq;bs),  bag-combine: ⋃x∈bs.f[x],  bag-null: bag-null(bs),  bag-map: bag-map(f;bs),  single-bag: {x},  empty-bag: {},  cons: [a / b],  nil: [],  callbyvalueall: callbyvalueall,  ifthenelse: if b then t else f fi ,  pi1: fst(t),  pi2: snd(t),  apply: f a,  fix: fix(F),  lambda: λx.A[x]
Definitions occuring in definition :  fix: fix(F),  bag-partitions: bag-partitions(eq;bs),  bag-combine: ⋃x∈bs.f[x],  empty-bag: {},  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  single-bag: {x},  nil: [],  callbyvalueall: callbyvalueall,  apply: f a,  pi2: snd(t),  bag-map: bag-map(f;bs),  lambda: λx.A[x],  cons: [a / b],  pi1: fst(t)
FDL editor aliases :  bag-parts
Latex:
bag-parts(eq;bs)  ==
    fix((\mlambda{}bag-parts,bs.  let  splits  \mleftarrow{}{}  bag-partitions(eq;bs)
                                            in  \mcup{}p\mmember{}splits.if  bag-null(fst(p))  then  \{\}
                                                  if  bag-null(snd(p))  then  \{[fst(p)]\}
                                                  else  let  parts  \mleftarrow{}{}  bag-parts  (snd(p))
                                                            in  bag-map(\mlambda{}L.[fst(p)  /  L];parts)
                                                  fi  )) 
    bs


Date html generated: 2016_05_15-PM-08_06_43
Last ObjectModification: 2015_09_23-AM-08_20_54

Theory : bags_2


Home Index