Nuprl Definition : mFOL-rename-bound-to-avoid

A renaming operator on mFOL() formulas.
It renames the bound variables to be disjoint from the given list
and produces a formula (alpha-equivalent) with the same abstract meaning.⋅
mFOL-rename-bound-to-avoid(fmla;L) ==  TERMOF{mFOL-bound-rename:o, 1:l, 1:l} fmla L


Definitions occuring in Statement :  apply: f a
FDL editor aliases :  mFOL-rename-bound-to-avoid
mFOL-rename-bound-to-avoid(fmla;L)  ==    TERMOF\{mFOL-bound-rename:o,  1:l,  1:l\}  fmla  L


Date html generated: 2015_07_17-AM-07_54_36
Last ObjectModification: 2012_09_11-PM-05_41_21

Home Index