---

Step * of Lemma freevars-FOL-subst

∀fmla:mFOL(). ∀nw,old,x:ℤ.
  ((x ∈ mFOL-freevars(fmla[nw/old]))
  ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla))))
BY
{ (((UnivCD THENA Auto) THEN Unfold `FOL-subst` 0)
   THEN (GenConclTerm ⌜FOL-rename-bound-to-avoid(fmla;[nw])⌝⋅ THENA Auto)
   THEN RWO "mFOL-freevars-of-rename" 0
   THEN Auto) }

1
.....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))

2
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 = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla)))
8. ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(v))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(v)))
9. ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = nw ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla)))
⊢ ¬(nw ∈ mFOL-boundvars(v))

---

Latex:

---

Latex:
\mforall{}fmla:mFOL().  \mforall{}nw,old,x:\mBbbZ{}.
    ((x  \mmember{}  mFOL-freevars(fmla[nw/old]))
    \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(fmla)))  \mvee{}  ((x  =  nw)  \mwedge{}  (old  \mmember{}  mFOL-freevars(fmla))))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `FOL-subst`  0)
  THEN  (GenConclTerm  \mkleeneopen{}FOL-rename-bound-to-avoid(fmla;[nw])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RWO  "mFOL-freevars-of-rename"  0
  THEN  Auto)

---

Home Index