---

Step * of Lemma mFOL-subst-abstract

∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:mFOL()]. ∀[x,y:ℤ].
  (Dom,S,a |= mFOL-abstract(fmla[x/y]) = Dom,S,a[y := a x] |= mFOL-abstract(fmla) ∈ ℙ)
BY
{ (Auto THEN Unfold `mFOL-subst` 0) }

1
1. Dom : Type
2. S : FOStruct(Dom)
3. a : FOAssignment(Dom)
4. fmla : mFOL()
5. x : ℤ
6. y : ℤ
⊢ Dom,S,a |= mFOL-abstract(mFOL-rename(mFOL-rename-bound-to-avoid(fmla;[x]);y;x))
= Dom,S,a[y := a x] |= mFOL-abstract(fmla)
∈ ℙ

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].  \mforall{}[a:FOAssignment(Dom)].  \mforall{}[fmla:mFOL()].  \mforall{}[x,y:\mBbbZ{}].
    (Dom,S,a  |=  mFOL-abstract(fmla[x/y])  =  Dom,S,a[y  :=  a  x]  |=  mFOL-abstract(fmla))


By

(Auto  THEN  Unfold  `mFOL-subst`  0)

---

Home Index