Nuprl Definition : rminimum
rminimum(n;m;k.x[k]) == primrec(m - n;x[n];λi,s. rmin(s;x[n + i + 1]))
Definitions occuring in Statement :
rmin: rmin(x;y),
primrec: primrec(n;b;c),
lambda: λx.A[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
add: n + m,
rmin: rmin(x;y),
lambda: λx.A[x],
subtract: n - m,
primrec: primrec(n;b;c)
FDL editor aliases :
rminimum
Latex:
rminimum(n;m;k.x[k]) == primrec(m - n;x[n];\mlambda{}i,s. rmin(s;x[n + i + 1]))
Date html generated:
2019_11_06-PM-00_29_06
Last ObjectModification:
2019_11_05-AM-11_53_47
Theory : reals
Home
Index