---

Step * 3 1 1 2 1 2 1 1 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. v : Dom
⊢ filter(λx.(¬b(x =z z'));mFOL-freevars(mFOL-rename(fmla';z;z'))) ⊆ filter(λx.(¬b(x =z z));mFOL-freevars(fmla'))
BY
{ (Unfold `l_contains` 0
   THEN RWW  "l_all_iff member_filter mFOL-freevars-of-rename" 0
   THEN Auto
   THEN All Reduce
   THEN SplitOrHyps
   THEN Auto) }

---

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.  v  :  Dom
\mvdash{}  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'))


By

---

Latex:
(Unfold  `l\_contains`  0
  THEN  RWW    "l\_all\_iff  member\_filter  mFOL-freevars-of-rename"  0
  THEN  Auto
  THEN  All  Reduce
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index