Nuprl Definition : mFOL-boundvars
mFOL-boundvars(fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ [];
mFOconnect(knd,a,b)⇒ bvsa,bvsb.bvsa ∪ bvsb;
mFOquant(isall,z,body)⇒ bvsbody.insert(z;bvsbody))
Definitions occuring in Statement :
mFOL_ind: mFOL_ind,
l-union: as ∪ bs,
insert: insert(a;L),
int-deq: IntDeq,
nil: []
FDL editor aliases :
mFOL-boundvars
mFOL-boundvars(fmla) ==
mFOL\_ind(fmla;
mFOatomic(R,vars){}\mRightarrow{} [];
mFOconnect(knd,a,b){}\mRightarrow{} bvsa,bvsb.bvsa \mcup{} bvsb;
mFOquant(isall,z,body){}\mRightarrow{} bvsbody.insert(z;bvsbody))
Date html generated:
2015_07_17-AM-07_54_15
Last ObjectModification:
2012_09_06-PM-10_41_35
Home
Index