Nuprl Definition : fps-Pascal
fps-Pascal(r;x;y;f) == ∀b:bag(Atom). (f[({x} + {y}) + b] = (f[{x} + b] +r f[{y} + b]) ∈ |r|)
Definitions occuring in Statement :
fps-coeff: f[b],
bag-append: as + bs,
single-bag: {x},
bag: bag(T),
infix_ap: x f y,
all: ∀x:A. B[x],
atom: Atom,
equal: s = t ∈ T,
rng_plus: +r,
rng_car: |r|
Definitions occuring in definition :
all: ∀x:A. B[x],
bag: bag(T),
atom: Atom,
equal: s = t ∈ T,
rng_car: |r|,
infix_ap: x f y,
rng_plus: +r,
fps-coeff: f[b],
bag-append: as + bs,
single-bag: {x}
FDL editor aliases :
fps-Pascal
Latex:
fps-Pascal(r;x;y;f) == \mforall{}b:bag(Atom). (f[(\{x\} + \{y\}) + b] = (f[\{x\} + b] +r f[\{y\} + b]))
Date html generated:
2016_05_15-PM-09_58_22
Last ObjectModification:
2015_09_23-AM-08_21_31
Theory : power!series
Home
Index