---

Step * 1 2 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()
⊢ ((¬(u1 = w ∈ varname())) ∧ (↑same-binding(v;v1;v@0;w)))
⇒ (¬(v@0 ∈ [u / v]))
⇒ ((¬(w ∈ [u1 / v1])) ∧ (w = v@0 ∈ varname()) ∧ ((||v|| + 1) = (||v1|| + 1) ∈ ℤ))
BY
{ ((Intros THEN D -2)
   THEN (Assert ¬(v@0 ∈ v) BY
               (ParallelLast THEN Auto))
   THEN (InstHyp [⌜v1⌝;⌜v@0⌝;⌜w⌝] 3⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

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. ¬(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)

---

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()
\mvdash{}  ((\mneg{}(u1  =  w))  \mwedge{}  (\muparrow{}same-binding(v;v1;v@0;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:
((Intros  THEN  D  -2)
  THEN  (Assert  \mneg{}(v@0  \mmember{}  v)  BY
                          (ParallelLast  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v@0\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index