Nuprl Definition : mFOL_case
case(fmla)
P(vars) => atomic[P; vars];
A knd B => connect[knd; A; B];
isall v.body => quant[isall; v; body] ==
if mFOatomic?(fmla) then atomic[mFOatomic-name(fmla); mFOatomic-vars(fmla)]
if mFOconnect?(fmla) then connect[mFOconnect-knd(fmla); mFOconnect-left(fmla); mFOconnect-right(fmla)]
else quant[mFOquant-isall(fmla); mFOquant-var(fmla); mFOquant-body(fmla)]
fi
Definitions occuring in Statement :
mFOquant-body: mFOquant-body(v),
mFOquant-var: mFOquant-var(v),
mFOquant-isall: mFOquant-isall(v),
mFOconnect-right: mFOconnect-right(v),
mFOconnect-left: mFOconnect-left(v),
mFOconnect-knd: mFOconnect-knd(v),
mFOconnect?: mFOconnect?(v),
mFOatomic-vars: mFOatomic-vars(v),
mFOatomic-name: mFOatomic-name(v),
mFOatomic?: mFOatomic?(v),
ifthenelse: if b then t else f fi
Definitions occuring in definition :
mFOatomic?: mFOatomic?(v),
mFOatomic-name: mFOatomic-name(v),
mFOatomic-vars: mFOatomic-vars(v),
ifthenelse: if b then t else f fi ,
mFOconnect?: mFOconnect?(v),
mFOconnect-knd: mFOconnect-knd(v),
mFOconnect-left: mFOconnect-left(v),
mFOconnect-right: mFOconnect-right(v),
mFOquant-isall: mFOquant-isall(v),
mFOquant-var: mFOquant-var(v),
mFOquant-body: mFOquant-body(v)
FDL editor aliases :
mFOL_case
Latex:
case(fmla)
P(vars) => atomic[P; vars];
A knd B => connect[knd; A; B];
isall v.body => quant[isall; v; body] ==
if mFOatomic?(fmla) then atomic[mFOatomic-name(fmla); mFOatomic-vars(fmla)]
if mFOconnect?(fmla)
then connect[mFOconnect-knd(fmla); mFOconnect-left(fmla); mFOconnect-right(fmla)]
else quant[mFOquant-isall(fmla); mFOquant-var(fmla); mFOquant-body(fmla)]
fi
Date html generated:
2017_02_20-AM-10_56_53
Last ObjectModification:
2017_01_19-PM-04_38_00
Theory : minimal-first-order-logic
Home
Index