Nuprl Definition : fix
f**(x) == Y (λfix,x. if eqof(eq) x (f x) then x else fix (f x) fi ) x
Wellformedness Lemmas :
fix_wf1,
fix_wf_corec_partial_nat,
fix_wf_corec-partial1,
fix_wf_corec_3parameter,
fix_wf_corec_parameter3,
fix_wf_corec_parameter2,
fix_wf_corec_parameter,
fix_wf_corec-alt-proof,
fix_wf_corec_system,
fix_wf_corec,
fix_wf_corec2,
fix_wf_corec2',
fix_wf_corec1,
fix_wf_partial
Definitions occuring in Statement :
eqof: eqof(d),
ifthenelse: if b then t else f fi ,
ycomb: Y,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eqof: eqof(d),
apply: f a
FDL editor aliases :
fixx
Latex:
f**(x) == Y (\mlambda{}fix,x. if eqof(eq) x (f x) then x else fix (f x) fi ) x
Date html generated:
2016_05_15-PM-05_06_10
Last ObjectModification:
2015_09_23-AM-07_51_27
Theory : general
Home
Index