Nuprl Lemma : mFOL-subst_wf

[fmla:mFOL()]. ∀[nw,old:ℤ].  (fmla[nw/old] ∈ mFOL())


Proof




Definitions occuring in Statement :  mFOL-subst: fmla[nw/old] mFOL: mFOL() uall: [x:A]. B[x] member: t ∈ T int:
Lemmas :  mFOL-rename_wf mFOL-rename-bound-to-avoid_wf cons_wf nil_wf mFOL_wf AbstractFOFormula_wf mFOL-abstract_wf l_disjoint_wf mFOL-boundvars_wf
\mforall{}[fmla:mFOL()].  \mforall{}[nw,old:\mBbbZ{}].    (fmla[nw/old]  \mmember{}  mFOL())



Date html generated: 2015_07_17-AM-07_54_39
Last ObjectModification: 2015_01_27-AM-10_06_12

Home Index