Nuprl Definition : rmaximum
rmaximum(n;m;k.x[k]) == primrec(m - n;x[n];λi,s. rmax(s;x[n + i + 1]))
Definitions occuring in Statement :
rmax: rmax(x;y),
primrec: primrec(n;b;c),
lambda: λx.A[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
subtract: n - m,
lambda: λx.A[x],
rmax: rmax(x;y),
add: n + m,
natural_number: $n
FDL editor aliases :
rmaximum
rmaximum
Latex:
rmaximum(n;m;k.x[k]) == primrec(m - n;x[n];\mlambda{}i,s. rmax(s;x[n + i + 1]))
Date html generated:
2016_05_18-AM-07_49_41
Last ObjectModification:
2015_09_23-AM-09_02_50
Theory : reals
Home
Index