---

Step * of Lemma mFOL-freevars-of-rename

No Annotations
∀fmla:mFOL(). ∀old,new:ℤ.
  ∀x:ℤ
    ((x ∈ mFOL-freevars(mFOL-rename(fmla;old;new)))
    ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(fmla))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(fmla)))) 
  supposing ¬(new ∈ mFOL-boundvars(fmla))
BY
{ ((BLemma `mFOL-induction` THENA Auto)
   THEN RepUR ``mFOL-freevars mFOL-boundvars mFOL-rename`` 0
   THEN Try (Fold `mFOL-rename` 0)
   THEN Try (Fold `mFOL-freevars` 0)
   THEN Try (Fold `mFOL-boundvars` 0)
   THEN (UnivCD THENA Auto)) }

1
1. name : Atom
2. vars : ℤ List
3. old : ℤ
4. new : ℤ
5. ¬(new ∈ [])
6. x : ℤ
⊢ (x ∈ remove-repeats(IntDeq;map(λv.if (v =z old) then new else v fi ;vars)))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ remove-repeats(IntDeq;vars))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ remove-repeats(IntDeq;vars)))

2
1. knd : Atom
2. left : mFOL()
3. right : mFOL()
4. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(left;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(left))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(left)))) 
     supposing ¬(new ∈ mFOL-boundvars(left))
5. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(right;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(right))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(right)))) 
     supposing ¬(new ∈ mFOL-boundvars(right))
6. old : ℤ
7. new : ℤ
8. ¬(new ∈ mFOL-boundvars(left) ⋃ mFOL-boundvars(right))
9. x : ℤ
⊢ (x ∈ val-union(IntDeq;mFOL-freevars(mFOL-rename(left;old;new));mFOL-freevars(mFOL-rename(right;old;new))))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right))))
    ∨ ((x = new ∈ ℤ) ∧ (old ∈ val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right))))

3
1. isall : 𝔹
2. var : ℤ
3. body : mFOL()
4. ∀old,new:ℤ.
     ∀x:ℤ
       ((x ∈ mFOL-freevars(mFOL-rename(body;old;new)))
       ⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(body))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(body)))) 
     supposing ¬(new ∈ mFOL-boundvars(body))
5. old : ℤ
6. new : ℤ
7. ¬(new ∈ insert(var;mFOL-boundvars(body)))
8. x : ℤ
⊢ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(if (var =z old) then body else mFOL-rename(body;old;new) fi )))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ (x ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))
    ∨ ((x = new ∈ ℤ) ∧ (old ∈ filter(λx.(¬b(x =z var));mFOL-freevars(body))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}fmla:mFOL().  \mforall{}old,new:\mBbbZ{}.
    \mforall{}x:\mBbbZ{}
        ((x  \mmember{}  mFOL-freevars(mFOL-rename(fmla;old;new)))
        \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(fmla)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(fmla)))) 
    supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(fmla))


By

---

Latex:
((BLemma  `mFOL-induction`  THENA  Auto)
  THEN  RepUR  ``mFOL-freevars  mFOL-boundvars  mFOL-rename``  0
  THEN  Try  (Fold  `mFOL-rename`  0)
  THEN  Try  (Fold  `mFOL-freevars`  0)
  THEN  Try  (Fold  `mFOL-boundvars`  0)
  THEN  (UnivCD  THENA  Auto))

---

Home Index