Nuprl Definition : model-fun-update2
M[n,k := m.F[m]] ==
  λx.if x is a pair then let y,z = x 
                         in if y=n  then if z=k  then F[M]  else (M x)  else (M x) otherwise M x
Definitions occuring in Statement : 
ispair: if z is a pair then a otherwise b
, 
int_eq: if a=b  then c  else d
, 
apply: f a
, 
lambda: λx.A[x]
, 
spread: spread def
Definitions occuring in definition : 
apply: f a
, 
int_eq: if a=b  then c  else d
, 
spread: spread def, 
ispair: if z is a pair then a otherwise b
, 
lambda: λx.A[x]
FDL editor aliases : 
model-fun-update2
Latex:
M[n,k  :=  m.F[m]]  ==
    \mlambda{}x.if  x  is  a  pair  then  let  y,z  =  x 
                                                  in  if  y=n    then  if  z=k    then  F[M]    else  (M  x)    else  (M  x)  otherwise  M  x
Date html generated:
2017_01_19-PM-02_32_06
Last ObjectModification:
2017_01_18-PM-06_11_10
Theory : minimal-first-order-logic
Home
Index