Nuprl Definition : d-conv
d-conv(r;f;g) == λn.Σ(p∈two-factorizations(n)). * (f (fst(p))) (g (snd(p)))
Definitions occuring in Statement :
two-factorizations: two-factorizations(n),
bag-summation: Σ(x∈b). f[x],
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
rng_times: *,
rng_zero: 0,
rng_plus: +r
Definitions occuring in definition :
lambda: λx.A[x],
bag-summation: Σ(x∈b). f[x],
rng_zero: 0,
rng_plus: +r,
two-factorizations: two-factorizations(n),
rng_times: *,
pi1: fst(t),
apply: f a,
pi2: snd(t)
FDL editor aliases :
d-conv
Latex:
d-conv(r;f;g) == \mlambda{}n.\mSigma{}(p\mmember{}two-factorizations(n)). * (f (fst(p))) (g (snd(p)))
Date html generated:
2016_05_15-PM-07_54_08
Last ObjectModification:
2015_09_23-AM-08_19_45
Theory : general
Home
Index