Nuprl Definition : mFOL-freevars

mFOL-freevars(fmla) ==
  mFOL_ind(fmla;
           mFOatomic(R,vars)⇒ remove-repeats(IntDeq;vars);
           mFOconnect(knd,a,b)⇒ fvsa,fvsb.val-union(IntDeq;fvsa;fvsb);
           mFOquant(isall,z,body)⇒ fvsbody.filter(λx.(¬b(x =z z));fvsbody)) 


Definitions occuring in Statement :  mFOL_ind: mFOL_ind,  remove-repeats: remove-repeats(eq;L),  val-union: val-union(eq;as;bs),  int-deq: IntDeq,  filter: filter(P;l),  bnot: ¬bb,  eq_int: (i =z j),  lambda: λx.A[x]
FDL editor aliases :  mFOL-freevars
mFOL-freevars(fmla)  ==
    mFOL\_ind(fmla;
                      mFOatomic(R,vars){}\mRightarrow{}  remove-repeats(IntDeq;vars);
                      mFOconnect(knd,a,b){}\mRightarrow{}  fvsa,fvsb.val-union(IntDeq;fvsa;fvsb);
                      mFOquant(isall,z,body){}\mRightarrow{}  fvsbody.filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));fvsbody)) 


Date html generated: 2015_07_17-AM-07_54_12
Last ObjectModification: 2013_04_21-PM-07_46_01

Home Index