Nuprl Lemma : mFOL-rename_wf
∀[fmla:mFOL()]. ∀[old,new:ℤ]. (mFOL-rename(fmla;old;new) ∈ mFOL())
Proof
Definitions occuring in Statement :
mFOL-rename: mFOL-rename(fmla;old;new),
mFOL: mFOL(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
Lemmas :
mFOL_ind_wf_simple,
mFOL_wf,
mFOatomic_wf,
map_wf,
eq_int_wf,
bool_wf,
list_wf,
mFOconnect_wf,
mFOquant_wf
\mforall{}[fmla:mFOL()]. \mforall{}[old,new:\mBbbZ{}]. (mFOL-rename(fmla;old;new) \mmember{} mFOL())
Date html generated:
2015_07_17-AM-07_54_20
Last ObjectModification:
2015_01_27-AM-10_06_33
Home
Index