Nuprl Definition : cWObar
cWObar() == λn,s. (0 < n ∧ (↑isr(s (n - 1))))
Definitions occuring in Statement :
assert: ↑b,
isr: isr(x),
less_than: a < b,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
and: P ∧ Q,
less_than: a < b,
assert: ↑b,
isr: isr(x),
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
cWObar
Latex:
cWObar() == \mlambda{}n,s. (0 < n \mwedge{} (\muparrow{}isr(s (n - 1))))
Date html generated:
2016_05_13-PM-03_52_11
Last ObjectModification:
2015_09_22-PM-05_45_27
Theory : bar-induction
Home
Index