Nuprl Definition : mFO-dest-connective

let a,b = dest-knd(fmla) in
F[a; b] ==
  if mFOconnect?(fmla) ∧b mFOconnect-knd(fmla) =a knd
  then F[mFOconnect-left(fmla); mFOconnect-right(fmla)]
  else inr ⋅ 
  fi 


Definitions occuring in Statement :  mFOconnect-right: mFOconnect-right(v),  mFOconnect-left: mFOconnect-left(v),  mFOconnect-knd: mFOconnect-knd(v),  mFOconnect?: mFOconnect?(v),  band: p ∧b q,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  it: ⋅,  inr: inr x 
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  band: p ∧b q,  mFOconnect?: mFOconnect?(v),  eq_atom: x =a y,  mFOconnect-knd: mFOconnect-knd(v),  mFOconnect-left: mFOconnect-left(v),  mFOconnect-right: mFOconnect-right(v),  inr: inr x ,  it: ⋅
FDL editor aliases :  mFO-dest-connective
Latex:
let  a,b  =  dest-knd(fmla)  in
F[a;  b]  ==
    if  mFOconnect?(fmla)  \mwedge{}\msubb{}  mFOconnect-knd(fmla)  =a  knd
    then  F[mFOconnect-left(fmla);  mFOconnect-right(fmla)]
    else  inr  \mcdot{} 
    fi 


Date html generated: 2016_05_15-PM-10_14_14
Last ObjectModification: 2015_09_23-AM-08_23_06

Theory : minimal-first-order-logic


Home Index