Nuprl Definition : bar-diverges
x↑ == ∀n:ℕ. (¬↑isl(bar-val(n;x)))
Definitions occuring in Statement :
bar-val: bar-val(n;x),
nat: ℕ,
assert: ↑b,
isl: isl(x),
all: ∀x:A. B[x],
not: ¬A
Definitions occuring in definition :
all: ∀x:A. B[x],
nat: ℕ,
not: ¬A,
assert: ↑b,
isl: isl(x),
bar-val: bar-val(n;x)
FDL editor aliases :
bar-diverges
Latex:
x\muparrow{} == \mforall{}n:\mBbbN{}. (\mneg{}\muparrow{}isl(bar-val(n;x)))
Date html generated:
2016_05_14-AM-06_20_17
Last ObjectModification:
2015_09_22-PM-05_47_39
Theory : co-recursion
Home
Index