Step
*
1
2
1
1
of Lemma
mFOL-subst-abstract
1. Dom : Type
2. S : FOStruct(Dom)
3. a : FOAssignment(Dom)
4. fmla : mFOL()
5. x : ℤ
6. y : ℤ
7. v : mFOL()@i'
8. mFOL-abstract(v) = mFOL-abstract(fmla) ∈ AbstractFOFormula@i'
9. l_disjoint(ℤ;[x];mFOL-boundvars(v))@i'
10. mFOL-rename-bound-to-avoid(fmla;[x])
= v
∈ {fmla':mFOL()|
(mFOL-abstract(fmla') = mFOL-abstract(fmla) ∈ AbstractFOFormula) ∧ l_disjoint(ℤ;[x];mFOL-boundvars(fmla'))} @i'
⊢ ¬(x ∈ mFOL-boundvars(v))
BY
{ (With ⌈x⌉ (D (-2))⋅ THEN Auto) }
Latex:
1. Dom : Type
2. S : FOStruct(Dom)
3. a : FOAssignment(Dom)
4. fmla : mFOL()
5. x : \mBbbZ{}
6. y : \mBbbZ{}
7. v : mFOL()@i'
8. mFOL-abstract(v) = mFOL-abstract(fmla)@i'
9. l\_disjoint(\mBbbZ{};[x];mFOL-boundvars(v))@i'
10. mFOL-rename-bound-to-avoid(fmla;[x]) = v@i'
\mvdash{} \mneg{}(x \mmember{} mFOL-boundvars(v))
By
(With \mkleeneopen{}x\mkleeneclose{} (D (-2))\mcdot{} THEN Auto)
Home
Index