Nuprl Definition : update-fun

update-fun(M;A;hnum) ==  if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= m.λi.(m <hnum, i>)] else M fi 


Definitions occuring in Statement :  model-fun-update1: M[n:= m.F[m]],  mFOLisAll: mFOLisAll(A),  mFOLisImp: mFOLisImp(A),  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  pair: <a, b>,  apply: f a,  lambda: λx.A[x],  model-fun-update1: M[n:= m.F[m]],  mFOLisAll: mFOLisAll(A),  mFOLisImp: mFOLisImp(A),  bor: p ∨bq,  ifthenelse: if b then t else f fi 
FDL editor aliases :  update-fun
Latex:
update-fun(M;A;hnum)  ==    if  mFOLisImp(A)  \mvee{}\msubb{}mFOLisAll(A)  then  M[hnum:=  m.\mlambda{}i.(m  <hnum,  i>)]  else  M  fi 


Date html generated: 2017_01_19-PM-02_32_01
Last ObjectModification: 2017_01_18-PM-06_21_51

Theory : minimal-first-order-logic


Home Index