Nuprl Definition : WCP
WCP(F;f;G) == mu(λn.F f =b F (G (n + 1))) + 1
Definitions occuring in Statement :
mu: mu(f),
eq_bool: p =b q,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
mu: mu(f),
lambda: λx.A[x],
eq_bool: p =b q,
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
WCP
Latex:
WCP(F;f;G) == mu(\mlambda{}n.F f =b F (G (n + 1))) + 1
Date html generated:
2017_09_29-PM-06_06_27
Last ObjectModification:
2017_07_08-PM-00_18_07
Theory : continuity
Home
Index