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),  filter: filter(P;l),  int-deq: IntDeq,  bnot: ¬bb,  eq_int: (i =z j),  lambda: λx.A[x]
Definitions occuring in definition :  mFOL_ind: mFOL_ind,  remove-repeats: remove-repeats(eq;L),  val-union: val-union(eq;as;bs),  int-deq: IntDeq,  filter: filter(P;l),  lambda: λx.A[x],  bnot: ¬bb,  eq_int: (i =z j)
FDL editor aliases :  mFOL-freevars
Latex:
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: 2016_05_15-PM-10_14_35
Last ObjectModification: 2015_09_23-AM-08_23_11

Theory : minimal-first-order-logic


Home Index