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