Nuprl Definition : rpolydiv
rpolydiv(n;a;z) == λi.primrec(n - 1 - i;a n;λj,r. ((a (n - j + 1)) + (z * r)))
Definitions occuring in Statement :
rmul: a * b,
radd: a + b,
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
radd: a + b,
apply: f a,
subtract: n - m,
add: n + m,
natural_number: $n,
rmul: a * b
FDL editor aliases :
rpolydiv
Latex:
rpolydiv(n;a;z) == \mlambda{}i.primrec(n - 1 - i;a n;\mlambda{}j,r. ((a (n - j + 1)) + (z * r)))
Date html generated:
2019_10_29-AM-10_14_57
Last ObjectModification:
2019_01_14-PM-09_30_44
Theory : reals
Home
Index