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