---

Step * of Lemma FOL-subst-trivial

∀nw,old:ℤ. ∀fmla:mFOL().
  ((¬(old ∈ mFOL-freevars(fmla)))
  ⇒ (FOL-abstract(fmla[nw/old]) = FOL-abstract(fmla) ∈ AbstractFOFormula+(mFOL-freevars(fmla))))
BY
{ (Auto
   THEN Unfold `FOL-subst` 0
   THEN (GenConclTerm ⌜FOL-rename-bound-to-avoid(fmla;[nw])⌝⋅ THENA Auto)
   THEN D -2
   THEN Auto
   THEN InstLemma `trivial-mFOL-rename` []
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `FOL-subst`  0
  THEN  (GenConclTerm  \mkleeneopen{}FOL-rename-bound-to-avoid(fmla;[nw])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Auto
  THEN  InstLemma  `trivial-mFOL-rename`  []
  THEN  Auto)

---

Home Index