---

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


1. v : varname()
2. bnds : varname() List
3. L : varname() List
⊢ (||L|| = ||bnds|| ∈ ℤ) ⇒ (¬(v ∈ bnds)) ⇒ (¬(v ∈ L)) ⇒ (↑same-binding(L;bnds;v;v))
BY
{ ((MoveToConcl (-1) THEN ListInd (-1))
   THEN InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN Try (((Assert 0 ≤ ||v1|| BY Auto) THEN Auto))
   THEN (Unfold `same-binding` 0 THEN Reduce 0)
   THEN 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||
⊢ ↑case eq_var(u1;v) of inl(_) => eq_var(u;v) | inr(_) => (¬beq_var(u;v)) ∧b same-binding(v2;v1;v;v)

---

Latex:

---

Latex:

1.  v  :  varname()
2.  bnds  :  varname()  List
3.  L  :  varname()  List
\mvdash{}  (||L||  =  ||bnds||)  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  bnds))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  L))  {}\mRightarrow{}  (\muparrow{}same-binding(L;bnds;v;v))


By

---

Latex:
((MoveToConcl  (-1)  THEN  ListInd  (-1))
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (((Assert  0  \mleq{}  ||v1||  BY  Auto)  THEN  Auto))
  THEN  (Unfold  `same-binding`  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index