---

Step * 1 of Lemma freevars-FOL-subst

.....rewrite subgoal..... 
1. fmla : mFOL()
2. nw : ℤ
3. old : ℤ
4. x : ℤ
5. v : {fmla':mFOL()| 
        (mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
        ∧ (FOL-abstract(fmla') = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)))
        ∧ l_disjoint(ℤ;[nw];mFOL-boundvars(fmla'))} 
6. FOL-rename-bound-to-avoid(fmla;[nw])
= v
∈ {fmla':mFOL()| 
   (mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
   ∧ (FOL-abstract(fmla') = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla)))
   ∧ l_disjoint(ℤ;[nw];mFOL-boundvars(fmla'))} 
7. -any : (x ∈ mFOL-freevars(mFOL-rename(v;old;nw)))
⊢ ¬(nw ∈ mFOL-boundvars(v))
BY
{ (D 0 THEN Auto THEN DVar `v' THEN Auto THEN With ⌜nw⌝ (D 8)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  fmla  :  mFOL()
2.  nw  :  \mBbbZ{}
3.  old  :  \mBbbZ{}
4.  x  :  \mBbbZ{}
5.  v  :  \{fmla':mFOL()| 
                (mFOL-freevars(fmla')  =  mFOL-freevars(fmla))
                \mwedge{}  (FOL-abstract(fmla')  =  FOL-abstract(fmla))
                \mwedge{}  l\_disjoint(\mBbbZ{};[nw];mFOL-boundvars(fmla'))\} 
6.  FOL-rename-bound-to-avoid(fmla;[nw])  =  v
7.  -any  :  (x  \mmember{}  mFOL-freevars(mFOL-rename(v;old;nw)))
\mvdash{}  \mneg{}(nw  \mmember{}  mFOL-boundvars(v))


By

---

Latex:
(D  0  THEN  Auto  THEN  DVar  `v'  THEN  Auto  THEN  With  \mkleeneopen{}nw\mkleeneclose{}  (D  8)\mcdot{}  THEN  Auto)

---

Home Index