Nuprl Definition : mFO-dest-atomic

let a,b = dest-atomic(fmla) in
F[a; b] ==
  if mFOatomic?(fmla) then F[mFOatomic-name(fmla); mFOatomic-vars(fmla)] else inr ⋅  fi 


Definitions occuring in Statement :  mFOatomic-vars: mFOatomic-vars(v),  mFOatomic-name: mFOatomic-name(v),  mFOatomic?: mFOatomic?(v),  ifthenelse: if b then t else f fi ,  it: ⋅,  inr: inr x 
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  mFOatomic?: mFOatomic?(v),  mFOatomic-name: mFOatomic-name(v),  mFOatomic-vars: mFOatomic-vars(v),  inr: inr x ,  it: ⋅
FDL editor aliases :  mFO-dest-atomic
Latex:
let  a,b  =  dest-atomic(fmla)  in
F[a;  b]  ==
    if  mFOatomic?(fmla)  then  F[mFOatomic-name(fmla);  mFOatomic-vars(fmla)]  else  inr  \mcdot{}    fi 


Date html generated: 2016_05_15-PM-10_14_10
Last ObjectModification: 2015_09_23-AM-08_23_05

Theory : minimal-first-order-logic


Home Index