---

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


1. isall : 𝔹
2. z : ℤ
3. body : mFOL()
4. ∀L:ℤ List
     (∃fmla':mFOL() [((mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List))
                    ∧ (mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula(mFOL-freevars(body)))
                    ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla')))])
5. L : ℤ List
6. (z ∈ L)
7. fmla' : mFOL()
8. mFOL-freevars(fmla') = mFOL-freevars(body) ∈ (ℤ List)
9. mFOL-abstract(fmla') = mFOL-abstract(body) ∈ AbstractFOFormula(mFOL-freevars(body))
10. l_disjoint(ℤ;L;mFOL-boundvars(fmla'))
11. z' : ℤ
12. ¬(z' ∈ L)
13. ¬(z' ∈ mFOL-boundvars(fmla'))
14. ¬(z' ∈ mFOL-freevars(fmla'))
15. mFOL-freevars(mFOquant(isall;z';mFOL-rename(fmla';z;z'))) = mFOL-freevars(mFOquant(isall;z;body)) ∈ (ℤ List)
⊢ (FOQuantifier(isall) z' mFOL-abstract(mFOL-rename(fmla';z;z')))
= (FOQuantifier(isall) z mFOL-abstract(body))
∈ AbstractFOFormula(mFOL-freevars(mFOquant(isall;z;body)))
BY
{ (((((D 1 THEN RenameVar `aa' 1) THEN D 1)
     THEN All (Fold `it`)
     THEN All (Folds ``btrue bfalse``)
     THEN RepUR ``FOQuantifier AbstractFOFormula`` 0
     THEN RepeatFor 4 ((EqCD THEN Auto))
     THEN RepUR ``mFOL-freevars`` -2
     THEN Fold `mFOL-freevars` (-2)
     THEN (Assert ⌜filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z')))
                   ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(body))⌝⋅
           THENL [(RevHypSubst' 8 0 THEN ThinVar `a')
                 ; ((RWO "9<" 0 THENA Auto) THEN RevHypSubst' 8 (-3) THEN RevHypSubst' 8 (-1))]
     ))
    THEN ThinVar `body'
    )
   THEN Id
   ) }

1
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. v : Dom
⊢ filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(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] |= mFOL-abstract(fmla') ∈ ℙ

---

Latex:

---

Latex:

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


By

---

Latex:
(((((D  1  THEN  RenameVar  `aa'  1)  THEN  D  1)
      THEN  All  (Fold  `it`)
      THEN  All  (Folds  ``btrue  bfalse``)
      THEN  RepUR  ``FOQuantifier  AbstractFOFormula``  0
      THEN  RepeatFor  4  ((EqCD  THEN  Auto))
      THEN  RepUR  ``mFOL-freevars``  -2
      THEN  Fold  `mFOL-freevars`  (-2)
      THEN  (Assert  \mkleeneopen{}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(body))\mkleeneclose{}\mcdot{}
                  THENL  [(RevHypSubst'  8  0  THEN  ThinVar  `a')
                              ;  ((RWO  "9<"  0  THENA  Auto)  THEN  RevHypSubst'  8  (-3)  THEN  RevHypSubst'  8  (-1))]
      ))
    THEN  ThinVar  `body'
    )
  THEN  Id
  )

---

Home Index