Nuprl Definition : model-fun-update1
M[n:= m.F[m]] == λx.if x is an integer then if x=n then F[M] else (M x) else M x
Definitions occuring in Statement :
isint: isint def,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
apply: f a,
int_eq: if a=b then c else d,
isint: isint def,
lambda: λx.A[x]
FDL editor aliases :
model-fun-update1
Latex:
M[n:= m.F[m]] == \mlambda{}x.if x is an integer then if x=n then F[M] else (M x) else M x
Date html generated:
2017_01_19-PM-02_31_56
Last ObjectModification:
2017_01_18-PM-06_07_08
Theory : minimal-first-order-logic
Home
Index