---

Step * of Lemma mFOL-rename-bound-to-avoid_wf

No Annotations
∀fmla:mFOL(). ∀L:ℤ List.
  (mFOL-rename-bound-to-avoid(fmla;L) ∈ {fmla':mFOL()| 
                                         (mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
                                         ∧ (mFOL-abstract(fmla')
                                           = mFOL-abstract(fmla)
                                           ∈ AbstractFOFormula(mFOL-freevars(fmla)))
                                         ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} )
BY
{ (Auto
   THEN RW  (AddrC [2] UnfoldTopAbC) 0
   THEN Subst ⌜TERMOF{mFOL-bound-rename:o, 1:l, 1:l} ~ TERMOF{mFOL-bound-rename:o, 1:l, i:l}⌝ 0⋅) }

1
.....equality..... 
1. fmla : mFOL()
2. L : ℤ List
⊢ TERMOF{mFOL-bound-rename:o, 1:l, 1:l} ~ TERMOF{mFOL-bound-rename:o, 1:l, i:l}

2
1. fmla : mFOL()
2. L : ℤ List
⊢ TERMOF{mFOL-bound-rename:o, 1:l, i:l} fmla L ∈ {fmla':mFOL()| 
                                                  (mFOL-freevars(fmla') = mFOL-freevars(fmla) ∈ (ℤ List))
                                                  ∧ (mFOL-abstract(fmla')
                                                    = mFOL-abstract(fmla)
                                                    ∈ AbstractFOFormula(mFOL-freevars(fmla)))
                                                  ∧ l_disjoint(ℤ;L;mFOL-boundvars(fmla'))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}fmla:mFOL().  \mforall{}L:\mBbbZ{}  List.
    (mFOL-rename-bound-to-avoid(fmla;L)  \mmember{}  \{fmla':mFOL()| 
                                                                                  (mFOL-freevars(fmla')  =  mFOL-freevars(fmla))
                                                                                  \mwedge{}  (mFOL-abstract(fmla')  =  mFOL-abstract(fmla))
                                                                                  \mwedge{}  l\_disjoint(\mBbbZ{};L;mFOL-boundvars(fmla'))\}  )


By

---

Latex:
(Auto
  THEN  RW    (AddrC  [2]  UnfoldTopAbC)  0
  THEN  Subst  \mkleeneopen{}TERMOF\{mFOL-bound-rename:o,  1:l,  1:l\}  \msim{}  TERMOF\{mFOL-bound-rename:o,  1:l,  i:l\}\mkleeneclose{}  0\mcdot{})

---

Home Index