---

Step * of Lemma same-binding-not-bound

No Annotations
∀[vs,ws:varname() List].
  ∀v,w:varname().
    ((↑same-binding(vs;ws;v;w)) ⇒ (¬(v ∈ vs)) ⇒ {(¬(w ∈ ws)) ∧ (w = v ∈ varname()) ∧ (||vs|| = ||ws|| ∈ ℤ)})
BY
{ (Unfold `guard` 0
   THEN RepeatFor 2 (InductionOnList)
   THEN Unfold `same-binding` 0
   THEN Reduce 0
   THEN Try (Complete ((RW assert_pushdownC 0 THEN Auto)))
   THEN RepeatFor 2 (Intro)) }

1
1. u : varname()
2. v : varname() List
3. ∀[ws:varname() List]
     ∀v@0,w:varname().
       ((↑same-binding(v;ws;v@0;w)) ⇒ (¬(v@0 ∈ v)) ⇒ ((¬(w ∈ ws)) ∧ (w = v@0 ∈ varname()) ∧ (||v|| = ||ws|| ∈ ℤ)))
4. u1 : varname()
5. v1 : varname() List
6. ∀v@0,w:varname().
     ((↑same-binding([u / v];v1;v@0;w))
     ⇒ (¬(v@0 ∈ [u / v]))
     ⇒ ((¬(w ∈ v1)) ∧ (w = v@0 ∈ varname()) ∧ (||[u / v]|| = ||v1|| ∈ ℤ)))
7. v@0 : varname()
8. w : varname()
⊢ (↑case eq_var(u;v@0) of inl(_) => eq_var(u1;w) | inr(_) => (¬beq_var(u1;w)) ∧b same-binding(v;v1;v@0;w))
⇒ (¬(v@0 ∈ [u / v]))
⇒ ((¬(w ∈ [u1 / v1])) ∧ (w = v@0 ∈ varname()) ∧ ((||v|| + 1) = (||v1|| + 1) ∈ ℤ))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[vs,ws:varname()  List].
    \mforall{}v,w:varname().
        ((\muparrow{}same-binding(vs;ws;v;w))  {}\mRightarrow{}  (\mneg{}(v  \mmember{}  vs))  {}\mRightarrow{}  \{(\mneg{}(w  \mmember{}  ws))  \mwedge{}  (w  =  v)  \mwedge{}  (||vs||  =  ||ws||)\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  RepeatFor  2  (InductionOnList)
  THEN  Unfold  `same-binding`  0
  THEN  Reduce  0
  THEN  Try  (Complete  ((RW  assert\_pushdownC  0  THEN  Auto)))
  THEN  RepeatFor  2  (Intro))

---

Home Index