---

Step * 1 2 of Lemma trivial-mFOL-rename

.....subterm..... T:t
2:n
1. x : ℤ
2. y : ℤ
3. knd : Atom
4. left : mFOL()
5. right : mFOL()
6. (¬(y ∈ mFOL-freevars(left))) ⇒ (left = mFOL-rename(left;y;x) ∈ mFOL())
7. (¬(y ∈ mFOL-freevars(right))) ⇒ (right = mFOL-rename(right;y;x) ∈ mFOL())
8. ¬(y ∈ val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)))
⊢ left = mFOL-rename(left;y;x) ∈ mFOL()
BY
{ ((BackThruSomeHyp THEN ParallelLast) THEN RWO "val-union-l-union" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  knd  :  Atom
4.  left  :  mFOL()
5.  right  :  mFOL()
6.  (\mneg{}(y  \mmember{}  mFOL-freevars(left)))  {}\mRightarrow{}  (left  =  mFOL-rename(left;y;x))
7.  (\mneg{}(y  \mmember{}  mFOL-freevars(right)))  {}\mRightarrow{}  (right  =  mFOL-rename(right;y;x))
8.  \mneg{}(y  \mmember{}  val-union(IntDeq;mFOL-freevars(left);mFOL-freevars(right)))
\mvdash{}  left  =  mFOL-rename(left;y;x)


By

---

Latex:
((BackThruSomeHyp  THEN  ParallelLast)  THEN  RWO  "val-union-l-union"  0  THEN  EAuto  1)

---

Home Index