Nuprl Definition : WCPD
WCPD(F;H;f;G) == mu(λn.(F f =b F (G (n + 1)) ∧b H f =b H (G (n + 1)))) + 1
Definitions occuring in Statement :
mu: mu(f),
eq_bool: p =b q,
band: p ∧b q,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
add: n + m,
apply: f a,
eq_bool: p =b q,
band: p ∧b q,
lambda: λx.A[x],
mu: mu(f)
FDL editor aliases :
WCPD
Latex:
WCPD(F;H;f;G) == mu(\mlambda{}n.(F f =b F (G (n + 1)) \mwedge{}\msubb{} H f =b H (G (n + 1)))) + 1
Date html generated:
2017_09_29-PM-06_06_31
Last ObjectModification:
2017_09_12-PM-02_15_06
Theory : continuity
Home
Index