Nuprl Definition : rprod
rprod(n;m;k.x[k]) == if m <z n then r1 else rprod(n;m - 1;k.x[k]) * x[m] fi
Definitions occuring in Statement :
rmul: a * b,
int-to-real: r(n),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
int-to-real: r(n),
rmul: a * b,
subtract: n - m,
natural_number: $n
FDL editor aliases :
rprod
Latex:
rprod(n;m;k.x[k]) == if m <z n then r1 else rprod(n;m - 1;k.x[k]) * x[m] fi
Date html generated:
2019_10_29-AM-10_16_14
Last ObjectModification:
2019_01_14-PM-10_35_12
Theory : reals
Home
Index