Nuprl Definition : note-is-function
note-is-function(A;hnum;M) ==  if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi 
Definitions occuring in Statement : 
modelAdd: M[n:= lbl,i,j]
, 
mFOLisAll: mFOLisAll(A)
, 
mFOLisImp: mFOLisImp(A)
, 
bor: p ∨bq
, 
ifthenelse: if b then t else f fi 
, 
natural_number: $n
, 
token: "$token"
Definitions occuring in definition : 
ifthenelse: if b then t else f fi 
, 
bor: p ∨bq
, 
mFOLisImp: mFOLisImp(A)
, 
mFOLisAll: mFOLisAll(A)
, 
modelAdd: M[n:= lbl,i,j]
, 
token: "$token"
, 
natural_number: $n
FDL editor aliases : 
note-is-function
Latex:
note-is-function(A;hnum;M)  ==    if  mFOLisImp(A)  \mvee{}\msubb{}mFOLisAll(A)  then  M[hnum:=  `function`]  else  M  fi 
Date html generated:
2016_05_15-PM-10_32_40
Last ObjectModification:
2015_09_23-AM-08_26_28
Theory : minimal-first-order-logic
Home
Index