Nuprl Definition : ni-iterated-min
ni-iterated-min(n;f) == primrec(n;∞;λm,s. ni-min(f m;s))
Definitions occuring in Statement :
ni-min: ni-min(f;g),
nat-inf-infinity: ∞,
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
nat-inf-infinity: ∞,
lambda: λx.A[x],
ni-min: ni-min(f;g),
apply: f a
FDL editor aliases :
ni-iterated-min
Latex:
ni-iterated-min(n;f) == primrec(n;\minfty{};\mlambda{}m,s. ni-min(f m;s))
Date html generated:
2016_05_15-PM-01_48_46
Last ObjectModification:
2015_09_23-AM-07_37_13
Theory : basic
Home
Index