---

Step * of Lemma alpha-rename-alist-property

No Annotations
∀[opr:Type]
  ∀t:term(opr). ∀L:varname() List.
    ((∀x,x':varname().  ((<x, x'> ∈ alpha-rename-alist(t;L)) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
    ∧ (∀x,x',y,y':varname().
         ((<x, x'> ∈ alpha-rename-alist(t;L))
         ⇒ (<y, y'> ∈ alpha-rename-alist(t;L))
         ⇒ (x' = y' ∈ varname())
         ⇒ (x = y ∈ varname()))))
BY
{ (Intros THEN Unfold `alpha-rename-alist` 0) }

1
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
⊢ (∀x,x':varname().
     ((<x, x'> ∈ snd(accumulate (with value p and list item x):
                      let vs,tab = p 
                      in eval x' = maybe_new_var(x;vs) in
                         <[x' / vs], [<x, x'> / tab]>
                     over list:
                       L
                     with starting value:
                      <L @ all-vars(t), []>)))
     ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
     ((<x, x'> ∈ snd(accumulate (with value p and list item x):
                      let vs,tab = p 
                      in eval x' = maybe_new_var(x;vs) in
                         <[x' / vs], [<x, x'> / tab]>
                     over list:
                       L
                     with starting value:
                      <L @ all-vars(t), []>)))
     ⇒ (<y, y'> ∈ snd(accumulate (with value p and list item x):
                        let vs,tab = p 
                        in eval x' = maybe_new_var(x;vs) in
                           <[x' / vs], [<x, x'> / tab]>
                       over list:
                         L
                       with starting value:
                        <L @ all-vars(t), []>)))
     ⇒ (x' = y' ∈ varname())
     ⇒ (x = y ∈ varname())))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}t:term(opr).  \mforall{}L:varname()  List.
        ((\mforall{}x,x':varname().
                ((<x,  x'>  \mmember{}  alpha-rename-alist(t;L))  {}\mRightarrow{}  ((x  \mmember{}  L)  \mwedge{}  (\mneg{}(x'  \mmember{}  L  @  all-vars(t))))))
        \mwedge{}  (\mforall{}x,x',y,y':varname().
                  ((<x,  x'>  \mmember{}  alpha-rename-alist(t;L))
                  {}\mRightarrow{}  (<y,  y'>  \mmember{}  alpha-rename-alist(t;L))
                  {}\mRightarrow{}  (x'  =  y')
                  {}\mRightarrow{}  (x  =  y))))


By

---

Latex:
(Intros  THEN  Unfold  `alpha-rename-alist`  0)

---

Home Index