---

Step * 1 1 of Lemma same-binding-not-bound


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()
9. u = v@0 ∈ varname()
⊢ (u1 = w ∈ varname())
⇒ (¬(v@0 ∈ [u / v]))
⇒ ((¬(w ∈ [u1 / v1])) ∧ (w = v@0 ∈ varname()) ∧ ((||v|| + 1) = (||v1|| + 1) ∈ ℤ))
BY
{ (RepeatFor 2 (Intro) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  varname()
2.  v  :  varname()  List
3.  \mforall{}[ws:varname()  List]
          \mforall{}v@0,w:varname().
              ((\muparrow{}same-binding(v;ws;v@0;w))  {}\mRightarrow{}  (\mneg{}(v@0  \mmember{}  v))  {}\mRightarrow{}  ((\mneg{}(w  \mmember{}  ws))  \mwedge{}  (w  =  v@0)  \mwedge{}  (||v||  =  ||ws||)))
4.  u1  :  varname()
5.  v1  :  varname()  List
6.  \mforall{}v@0,w:varname().
          ((\muparrow{}same-binding([u  /  v];v1;v@0;w))
          {}\mRightarrow{}  (\mneg{}(v@0  \mmember{}  [u  /  v]))
          {}\mRightarrow{}  ((\mneg{}(w  \mmember{}  v1))  \mwedge{}  (w  =  v@0)  \mwedge{}  (||[u  /  v]||  =  ||v1||)))
7.  v@0  :  varname()
8.  w  :  varname()
9.  u  =  v@0
\mvdash{}  (u1  =  w)  {}\mRightarrow{}  (\mneg{}(v@0  \mmember{}  [u  /  v]))  {}\mRightarrow{}  ((\mneg{}(w  \mmember{}  [u1  /  v1]))  \mwedge{}  (w  =  v@0)  \mwedge{}  ((||v||  +  1)  =  (||v1||  +  1)))


By

---

Latex:
(RepeatFor  2  (Intro)  THEN  D  -1  THEN  Auto)

---

Home Index