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


1. varname()
2. 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. 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