Nuprl Definition : mFOL-subst
Substitute variable nw for variable old in fmla.
To do that, first rename the bound variables to avoid nw
and then rename old to nw.⋅
fmla[nw/old] ==  mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Definitions occuring in Statement : 
mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L)
, 
mFOL-rename: mFOL-rename(fmla;old;new)
, 
cons: [a / b]
, 
nil: []
FDL editor aliases : 
mFOL-subst
fmla[nw/old]  ==    mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Date html generated:
2015_07_17-AM-07_54_39
Last ObjectModification:
2012_09_11-PM-05_43_12
Home
Index