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
FDL editor aliases :
mFO-dest-connective
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:
2015_07_17-AM-07_53_59
Last ObjectModification:
2012_09_04-AM-00_26_51
Home
Index