---

Step * 3 1 1 2 1 2 1 2 of Lemma mFOL-bound-rename


1. aa : 0 = 0 ∈ ℤ
2. z : ℤ
3. L : ℤ List
4. (z ∈ L)
5. fmla' : mFOL()
6. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
7. z' : ℤ
8. ¬(z' ∈ L)
9. ¬(z' ∈ mFOL-boundvars(fmla'))
10. ¬(z' ∈ mFOL-freevars(fmla'))
11. Dom : Type
12. S : FOStruct(Dom)
13. a : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(fmla')),Dom)
14. v : Dom
15. filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
⊢ Dom,S,a[z' := v] |= mFOL-abstract(mFOL-rename(fmla';z;z')) = Dom,S,a[z := v] |= mFOL-abstract(fmla') ∈ ℙ
BY
{ Subst ⌜Dom,S,a[z := v] |= mFOL-abstract(fmla') = Dom,S,a[z' := v][z := v] |= mFOL-abstract(fmla') ∈ ℙ⌝ 0⋅ }

1
.....equality..... 
1. aa : 0 = 0 ∈ ℤ
2. z : ℤ
3. L : ℤ List
4. (z ∈ L)
5. fmla' : mFOL()
6. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
7. z' : ℤ
8. ¬(z' ∈ L)
9. ¬(z' ∈ mFOL-boundvars(fmla'))
10. ¬(z' ∈ mFOL-freevars(fmla'))
11. Dom : Type
12. S : FOStruct(Dom)
13. a : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(fmla')),Dom)
14. v : Dom
15. filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
⊢ Dom,S,a[z := v] |= mFOL-abstract(fmla') = Dom,S,a[z' := v][z := v] |= mFOL-abstract(fmla') ∈ ℙ

2
1. aa : 0 = 0 ∈ ℤ
2. z : ℤ
3. L : ℤ List
4. (z ∈ L)
5. fmla' : mFOL()
6. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
7. z' : ℤ
8. ¬(z' ∈ L)
9. ¬(z' ∈ mFOL-boundvars(fmla'))
10. ¬(z' ∈ mFOL-freevars(fmla'))
11. Dom : Type
12. S : FOStruct(Dom)
13. a : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(fmla')),Dom)
14. v : Dom
15. filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
⊢ Dom,S,a[z' := v] |= mFOL-abstract(mFOL-rename(fmla';z;z')) = Dom,S,a[z' := v][z := v] |= mFOL-abstract(fmla') ∈ ℙ

3
.....wf..... 
1. aa : 0 = 0 ∈ ℤ
2. z : ℤ
3. L : ℤ List
4. (z ∈ L)
5. fmla' : mFOL()
6. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
7. z' : ℤ
8. ¬(z' ∈ L)
9. ¬(z' ∈ mFOL-boundvars(fmla'))
10. ¬(z' ∈ mFOL-freevars(fmla'))
11. Dom : Type
12. S : FOStruct(Dom)
13. a : FOAssignment(filter(λx.(¬b(x =z z));mFOL-freevars(fmla')),Dom)
14. v : Dom
15. filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
16. z1 : ℙ
⊢ Dom,S,a[z' := v] |= mFOL-abstract(mFOL-rename(fmla';z;z')) = z1 ∈ ℙ ∈ ℙ'

---

Latex:

---

Latex:

1.  aa  :  0  =  0
2.  z  :  \mBbbZ{}
3.  L  :  \mBbbZ{}  List
4.  (z  \mmember{}  L)
5.  fmla'  :  mFOL()
6.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))
7.  z'  :  \mBbbZ{}
8.  \mneg{}(z'  \mmember{}  L)
9.  \mneg{}(z'  \mmember{}  mFOL-boundvars(fmla'))
10.  \mneg{}(z'  \mmember{}  mFOL-freevars(fmla'))
11.  Dom  :  Type
12.  S  :  FOStruct(Dom)
13.  a  :  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(fmla')),Dom)
14.  v  :  Dom
15.  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z'));mFOL-freevars(mFOL-rename(fmla';z;z')))
        \msubseteq{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  z));mFOL-freevars(fmla'))
\mvdash{}  Dom,S,a[z'  :=  v]  |=  mFOL-abstract(mFOL-rename(fmla';z;z'))
=  Dom,S,a[z  :=  v]  |=  mFOL-abstract(fmla')


By

---

Latex:
Subst  \mkleeneopen{}Dom,S,a[z  :=  v]  |=  mFOL-abstract(fmla')  =  Dom,S,a[z'  :=  v][z  :=  v]  |=  mFOL-abstract(fmla')\mkleeneclose{}  0
\mcdot{}

---

Home Index