Nuprl Definition : mFOL-rename

mFOL-rename(fmla;old;new) ==
  mFOL_ind(fmla;
           mFOatomic(R,vars)⇒ R(map(λv.if (v =z old) then new else v fi ;vars));
           mFOconnect(knd,a,b)⇒ a',b'.mFOconnect(knd;a';b');
           mFOquant(isall,x,body)⇒ body'.mFOquant(isall;x;if (x =z old) then body else body' fi )) 


Definitions occuring in Statement :  mFOL_ind: mFOL_ind,  mFOquant: mFOquant(isall;var;body),  mFOconnect: mFOconnect(knd;left;right),  mFOatomic: name(vars),  map: map(f;as),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  lambda: λx.A[x]
FDL editor aliases :  mFOL-rename
mFOL-rename(fmla;old;new)  ==
    mFOL\_ind(fmla;
                      mFOatomic(R,vars){}\mRightarrow{}  R(map(\mlambda{}v.if  (v  =\msubz{}  old)  then  new  else  v  fi  ;vars));
                      mFOconnect(knd,a,b){}\mRightarrow{}  a',b'.mFOconnect(knd;a';b');
                      mFOquant(isall,x,body){}\mRightarrow{}  body'.mFOquant(isall;x;if  (x  =\msubz{}  old)  then  body  else  body'  fi  )) 


Date html generated: 2015_07_17-AM-07_54_19
Last ObjectModification: 2012_09_06-PM-10_42_20

Home Index