---

Step * 1 1 2 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||
⊢ ↑case eq_var(u1;v) of inl(_) => eq_var(u;v) | inr(_) => (¬beq_var(u;v)) ∧b same-binding(v2;v1;v;v)
BY
{ ((BoolCase ⌜eq_var(u;v)⌝⋅ THENA Auto) THEN (BoolCase ⌜eq_var(u1;v)⌝⋅ THENA Auto)) }

1
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

2
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

3
1. v : varname()
2. u : varname()
3. ¬(u = v ∈ varname())
4. v1 : varname() List
5. ∀L:varname() List. ((||L|| = ||v1|| ∈ ℤ) ⇒ (¬(v ∈ v1)) ⇒ (¬(v ∈ L)) ⇒ (↑same-binding(L;v1;v;v)))
6. u1 : 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. u1 = v ∈ varname()
⊢ False

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

---

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||
\mvdash{}  \muparrow{}case  eq\_var(u1;v)  of  inl($_{}$)  =>  eq\_var(u;v)  |  inr($_{}\mbackslash{}ff2\000C4)  =>  (\mneg{}\msubb{}eq\_var(u;v))  \mwedge{}\msubb{}  same-binding(v2;v1;v;v)


By

---

Latex:
((BoolCase  \mkleeneopen{}eq\_var(u;v)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (BoolCase  \mkleeneopen{}eq\_var(u1;v)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index