---

Step * 2 of Lemma freevars-mFOL-subst


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

---

Latex:

---

Latex:

1.  fmla  :  mFOL()
2.  nw  :  \mBbbZ{}
3.  old  :  \mBbbZ{}
4.  x  :  \mBbbZ{}
5.  v  :  \{fmla':mFOL()| 
                (mFOL-freevars(fmla')  =  mFOL-freevars(fmla))
                \mwedge{}  (mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
                \mwedge{}  l\_disjoint(\mBbbZ{};[nw];mFOL-boundvars(fmla'))\} 
6.  mFOL-rename-bound-to-avoid(fmla;[nw])  =  v
7.  -any  :  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(fmla)))  \mvee{}  ((x  =  nw)  \mwedge{}  (old  \mmember{}  mFOL-freevars(fmla)))
8.  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(v)))  \mvee{}  ((x  =  nw)  \mwedge{}  (old  \mmember{}  mFOL-freevars(v)))
9.  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(fmla)))  \mvee{}  ((x  =  nw)  \mwedge{}  (old  \mmember{}  mFOL-freevars(fmla)))
\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