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: []
Definitions occuring in definition :
mFOL-rename: mFOL-rename(fmla;old;new),
mFOL-rename-bound-to-avoid: mFOL-rename-bound-to-avoid(fmla;L),
cons: [a / b],
nil: []
FDL editor aliases :
mFOL-subst
Latex:
fmla[nw/old] == mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[nw]);old;nw)
Date html generated:
2016_07_08-PM-05_20_29
Last ObjectModification:
2015_09_23-AM-08_23_21
Theory : minimal-first-order-logic
Home
Index