---

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


1. isall : 𝔹@i'
2. z : ℤ@i'
3. body : mFOL()@i'
4. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
5. L : ℤ List@i'
6. (z ∈ L)
7. fmla' : mFOL()
8. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula
9. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
10. z' : ℤ
11. ¬(z' ∈ L)
12. ¬(z' ∈ mFOL-boundvars(fmla'))
13. ¬(z' ∈ mFOL-freevars(fmla'))
⊢ (FOQuantifier(isall) z' mFOL-abstract(mFOL-rename(fmla';z;z')))
= (FOQuantifier(isall) z mFOL-abstract(body))
∈ AbstractFOFormula
BY
{ (RepUR ``FOQuantifier AbstractFOFormula`` 0 THEN RepeatFor 3 ((EqCD THEN Auto)) THEN AutoSplit) }

1
1. isall : 𝔹@i'
2. z : ℤ@i'
3. body : mFOL()@i'
4. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
5. L : ℤ List@i'
6. (z ∈ L)
7. fmla' : mFOL()
8. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula
9. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
10. z' : ℤ
11. ¬(z' ∈ L)
12. ¬(z' ∈ mFOL-boundvars(fmla'))
13. ¬(z' ∈ mFOL-freevars(fmla'))
14. Dom : Type@i'
15. S : FOStruct(Dom)@i'
16. a : FOAssignment(Dom)@i
17. ↑isall
⊢ (∀v:Dom. Dom,S,a[z' := v] |= mFOL-abstract(mFOL-rename(fmla';z;z')))
= (∀v:Dom. Dom,S,a[z := v] |= mFOL-abstract(body))
∈ ℙ

2
1. isall : 𝔹@i'
2. ¬↑isall
3. z : ℤ@i'
4. body : mFOL()@i'
5. ∀L:ℤ List
     (∃fmla':{mFOL()| ((mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula)
                      ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))})@i'
6. L : ℤ List@i'
7. (z ∈ L)
8. fmla' : mFOL()
9. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
11. z' : ℤ
12. ¬(z' ∈ L)
13. ¬(z' ∈ mFOL-boundvars(fmla'))
14. ¬(z' ∈ mFOL-freevars(fmla'))
15. Dom : Type@i'
16. S : FOStruct(Dom)@i'
17. a : FOAssignment(Dom)@i
⊢ (∃v:Dom. Dom,S,a[z' := v] |= mFOL-abstract(mFOL-rename(fmla';z;z')))
= (∃v:Dom. Dom,S,a[z := v] |= mFOL-abstract(body))
∈ ℙ

---

Latex:



1.  isall  :  \mBbbB{}@i'
2.  z  :  \mBbbZ{}@i'
3.  body  :  mFOL()@i'
4.  \mforall{}L:\mBbbZ{}  List
          (\mexists{}fmla':\{mFOL()|  ((mFOL-abstract(fmla')  =  mFOL-abstract(body))
                                            \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla')))\})@i'
5.  L  :  \mBbbZ{}  List@i'
6.  (z  \mmember{}  L)
7.  fmla'  :  mFOL()
8.  mFOL-abstract(fmla')  =  mFOL-abstract(body)
9.  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))
10.  z'  :  \mBbbZ{}
11.  \mneg{}(z'  \mmember{}  L)
12.  \mneg{}(z'  \mmember{}  mFOL-boundvars(fmla'))
13.  \mneg{}(z'  \mmember{}  mFOL-freevars(fmla'))
\mvdash{}  (FOQuantifier(isall)  z'  mFOL-abstract(mFOL-rename(fmla';z;z')))
=  (FOQuantifier(isall)  z  mFOL-abstract(body))


By

(RepUR  ``FOQuantifier  AbstractFOFormula``  0  THEN  RepeatFor  3  ((EqCD  THEN  Auto))  THEN  AutoSplit)

---

Home Index