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
Definitions occuring in definition :  apply: f a
TermOfs occuring in Definition :  mFOL-bound-rename
FDL editor aliases :  mFOL-rename-bound-to-avoid
Latex:
mFOL-rename-bound-to-avoid(fmla;L)  ==    TERMOF\{mFOL-bound-rename:o,  1:l,  1:l\}  fmla  L


Date html generated: 2016_07_08-PM-05_20_16
Last ObjectModification: 2015_09_23-AM-08_23_17

Theory : minimal-first-order-logic


Home Index