---

Step * 1 2 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. ¬(u = v@0 ∈ varname())
9. w : varname()
10. ¬(u1 = w ∈ varname())
11. ↑same-binding(v;v1;v@0;w)
12. ¬(v@0 ∈ [u / v])
13. ¬(v@0 ∈ v)
14. w = v@0 ∈ varname()
15. ||v|| = ||v1|| ∈ ℤ
16. (w ∈ [u1 / v1])
⊢ (w ∈ v1)
BY
{ (GenListD (-1) 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.  \mneg{}(u  =  v@0)
9.  w  :  varname()
10.  \mneg{}(u1  =  w)
11.  \muparrow{}same-binding(v;v1;v@0;w)
12.  \mneg{}(v@0  \mmember{}  [u  /  v])
13.  \mneg{}(v@0  \mmember{}  v)
14.  w  =  v@0
15.  ||v||  =  ||v1||
16.  (w  \mmember{}  [u1  /  v1])
\mvdash{}  (w  \mmember{}  v1)


By

---

Latex:
(GenListD  (-1)  THEN  D  -1  THEN  Auto)

---

Home Index