Nuprl Definition : reg-less
reg-less(x;y) == eval x' = x in eval y' = y in find-ge(λn.(x n) + 4 <z y n;1)
Definitions occuring in Statement :
find-ge: find-ge(f;n),
callbyvalue: callbyvalue,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
find-ge: find-ge(f;n),
lambda: λx.A[x],
lt_int: i <z j,
add: n + m,
apply: f a,
natural_number: $n
FDL editor aliases :
reg-less
Latex:
reg-less(x;y) == eval x' = x in eval y' = y in find-ge(\mlambda{}n.(x n) + 4 <z y n;1)
Date html generated:
2016_05_18-AM-06_47_48
Last ObjectModification:
2015_09_23-AM-09_00_37
Theory : reals
Home
Index