---

Step * 1 1 2 1 1 1 1 1 of Lemma alpha-rename-equivalent


1. v : varname()
2. u : varname()
3. v1 : varname() List
4. ∀L:varname() List. ((||L|| = ||v1|| ∈ ℤ) ⇒ (¬(v ∈ v1)) ⇒ (¬(v ∈ L)) ⇒ (↑same-binding(L;v1;v;v)))
5. u1 : varname()
6. v2 : varname() List
7. (||v2|| = ||[u / v1]|| ∈ ℤ) ⇒ (¬(v ∈ [u / v1])) ⇒ (¬(v ∈ v2)) ⇒ (↑same-binding(v2;[u / v1];v;v))
8. (||v2|| + 1) = (||v1|| + 1) ∈ ℤ
9. ¬(v ∈ [u / v1])
10. ¬(v ∈ [u1 / v2])
11. 0 ≤ ||v1||
12. u = v ∈ varname()
13. u1 = v ∈ varname()
⊢ True
BY
{ Auto }

---

Latex:

---

Latex:

1.  v  :  varname()
2.  u  :  varname()
3.  v1  :  varname()  List
4.  \mforall{}L:varname()  List.  ((||L||  =  ||v1||)  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  v1))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  L))  {}\mRightarrow{}  (\muparrow{}same-binding(L;v1;v;v)))
5.  u1  :  varname()
6.  v2  :  varname()  List
7.  (||v2||  =  ||[u  /  v1]||)  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  [u  /  v1]))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  v2))  {}\mRightarrow{}  (\muparrow{}same-binding(v2;[u  /  v1];v;v))
8.  (||v2||  +  1)  =  (||v1||  +  1)
9.  \mneg{}(v  \mmember{}  [u  /  v1])
10.  \mneg{}(v  \mmember{}  [u1  /  v2])
11.  0  \mleq{}  ||v1||
12.  u  =  v
13.  u1  =  v
\mvdash{}  True


By

---

Latex:
Auto

---

Home Index