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),
nil: [],
int-deq: IntDeq
Definitions occuring in definition :
mFOL_ind: mFOL_ind,
nil: [],
l-union: as ⋃ bs,
insert: insert(a;L),
int-deq: IntDeq
FDL editor aliases :
mFOL-boundvars
Latex:
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:
2016_05_15-PM-10_14_47
Last ObjectModification:
2015_09_23-AM-08_23_12
Theory : minimal-first-order-logic
Home
Index