### Nuprl Lemma : mFOL-rename-bound-to-avoid_wf

`∀fmla:mFOL(). ∀L:ℤ List.`
`  (mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()| `
`                                         (mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula)`
`                                         ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )`

Proof

Definitions occuring in Statement :  mFOL-rename-bound-to-avoid: `mFOL-rename-bound-to-avoid(fmla;L)` mFOL-abstract: `mFOL-abstract(fmla)` mFOL-boundvars: `mFOL-boundvars(fmla)` mFOL: `mFOL()` AbstractFOFormula: `AbstractFOFormula` l_disjoint: `l_disjoint(T;l1;l2)` list: `T List` all: `∀x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` int: `ℤ` equal: `s = t ∈ T`
Lemmas :  lifting-strict-spread has-value_wf_base base_wf is-exception_wf lifting-strict-decide top_wf mFOL-boundvars_wf l_disjoint_wf mFOL-abstract_wf AbstractFOFormula_wf sq_exists_wf list_wf mFOL_wf all_wf sq_exists_subtype_rel subtype_rel_self
\mforall{}fmla:mFOL().  \mforall{}L:\mBbbZ{}  List.
(mFOL-rename-bound-to-avoid(fmla;L)  \mmember{}  \{fmla':mFOL()|
(mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
\mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))\}  )

Date html generated: 2015_07_17-AM-07_54_38
Last ObjectModification: 2015_06_19-PM-01_31_27

Home Index