Step
*
1
1
2
1
1
1
1
2
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. ¬(u1 = v ∈ varname())
7. v2 : varname() List
8. (||v2|| = ||[u / v1]|| ∈ ℤ) 
⇒ (¬(v ∈ [u / v1])) 
⇒ (¬(v ∈ v2)) 
⇒ (↑same-binding(v2;[u / v1];v;v))
9. (||v2|| + 1) = (||v1|| + 1) ∈ ℤ
10. ¬(v ∈ [u / v1])
11. ¬(v ∈ [u1 / v2])
12. 0 ≤ ||v1||
13. u = v ∈ varname()
⊢ False
BY
{ (D -4 THEN 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.  \mneg{}(u1  =  v)
7.  v2  :  varname()  List
8.  (||v2||  =  ||[u  /  v1]||)  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  [u  /  v1]))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  v2))  {}\mRightarrow{}  (\muparrow{}same-binding(v2;[u  /  v1];v;v))
9.  (||v2||  +  1)  =  (||v1||  +  1)
10.  \mneg{}(v  \mmember{}  [u  /  v1])
11.  \mneg{}(v  \mmember{}  [u1  /  v2])
12.  0  \mleq{}  ||v1||
13.  u  =  v
\mvdash{}  False
By
Latex:
(D  -4  THEN  Auto)
Home
Index