---

Step * 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()
⊢ (↑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) ∈ ℤ))
BY
{ ((BoolCase ⌜eq_var(u;v@0)⌝⋅ THENA Auto) THEN (RW assert_pushdownC 0 THENA 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. 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) ∈ ℤ))

2
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) ∈ ℤ))

---

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()
\mvdash{}  (\muparrow{}case  eq\_var(u;v@0)
      of  inl($_{}$)  =>
      eq\_var(u1;w)
      |  inr($_{}$)  =>
      (\mneg{}\msubb{}eq\_var(u1;w))  \mwedge{}\msubb{}  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:
((BoolCase  \mkleeneopen{}eq\_var(u;v@0)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index