Nuprl Definition : mFO-dest-quantifier

let v,b = dest-if isall then all else exists(fmla); in
 F[v; b] ==
  if mFOquant?(fmla) ∧b mFOquant-isall(fmla) =b isall then F[mFOquant-var(fmla); mFOquant-body(fmla)] else inr ⋅  fi 


Definitions occuring in Statement :  mFOquant-body: mFOquant-body(v),  mFOquant-var: mFOquant-var(v),  mFOquant-isall: mFOquant-isall(v),  mFOquant?: mFOquant?(v),  eq_bool: p =b q,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  it: ⋅,  inr: inr x 
FDL editor aliases :  mFO-dest-quantifier
let  v,b  =  dest-if  isall  then  all  else  exists(fmla);  in
  F[v;  b]  ==
    if  mFOquant?(fmla)  \mwedge{}\msubb{}  mFOquant-isall(fmla)  =b  isall
    then  F[mFOquant-var(fmla);  mFOquant-body(fmla)]
    else  inr  \mcdot{} 
    fi 


Date html generated: 2015_07_17-AM-07_54_02
Last ObjectModification: 2012_09_04-AM-00_27_05

Home Index