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