---

Step * 2 of Lemma mFOL-freevars-of-rename


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))))
BY
{ ((RWW "val-union-l-union member-union" 0 THENA Auto)
   THEN (Assert (¬(new ∈ mFOL-boundvars(left))) ∧ (¬(new ∈ mFOL-boundvars(right))) BY
               (D 0 THEN ParallelOp -2 THEN RWO "member-union" 0 THEN Auto))
   THEN (RWO "4 5" 0 THENA Auto)) }

1
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 : ℤ
10. (¬(new ∈ mFOL-boundvars(left))) ∧ (¬(new ∈ mFOL-boundvars(right)))
⊢ (((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(left))) ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(left))))
  ∨ ((¬(x = old ∈ ℤ)) ∧ (x ∈ mFOL-freevars(right)))
  ∨ ((x = new ∈ ℤ) ∧ (old ∈ mFOL-freevars(right)))
⇐⇒ ((¬(x = old ∈ ℤ)) ∧ ((x ∈ mFOL-freevars(left)) ∨ (x ∈ mFOL-freevars(right))))
    ∨ ((x = new ∈ ℤ) ∧ ((old ∈ mFOL-freevars(left)) ∨ (old ∈ mFOL-freevars(right))))

---

Latex:

---

Latex:

1.  knd  :  Atom
2.  left  :  mFOL()
3.  right  :  mFOL()
4.  \mforall{}old,new:\mBbbZ{}.
          \mforall{}x:\mBbbZ{}
              ((x  \mmember{}  mFOL-freevars(mFOL-rename(left;old;new)))
              \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(left)))  \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(left)))) 
          supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(left))
5.  \mforall{}old,new:\mBbbZ{}.
          \mforall{}x:\mBbbZ{}
              ((x  \mmember{}  mFOL-freevars(mFOL-rename(right;old;new)))
              \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  mFOL-freevars(right)))
                      \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  mFOL-freevars(right)))) 
          supposing  \mneg{}(new  \mmember{}  mFOL-boundvars(right))
6.  old  :  \mBbbZ{}
7.  new  :  \mBbbZ{}
8.  \mneg{}(new  \mmember{}  mFOL-boundvars(left)  \mcup{}  mFOL-boundvars(right))
9.  x  :  \mBbbZ{}
\mvdash{}  (x
        \mmember{}  val-union(IntDeq;mFOL-freevars(mFOL-rename(left;old;new));mFOL-freevars(...)))
\mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(x  =  old))  \mwedge{}  (x  \mmember{}  val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right))))
        \mvee{}  ((x  =  new)  \mwedge{}  (old  \mmember{}  val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right))))


By

---

Latex:
((RWW  "val-union-l-union  member-union"  0  THENA  Auto)
  THEN  (Assert  (\mneg{}(new  \mmember{}  mFOL-boundvars(left)))  \mwedge{}  (\mneg{}(new  \mmember{}  mFOL-boundvars(right)))  BY
                          (D  0  THEN  ParallelOp  -2  THEN  RWO  "member-union"  0  THEN  Auto))
  THEN  (RWO  "4  5"  0  THENA  Auto))

---

Home Index