---

Step * of Lemma alpha-rename-alist-property2

No Annotations
∀[opr:Type]
  ∀t:term(opr). ∀L:varname() List. ∀x:varname().  ((x ∈ L) ⇒ (∃x':varname(). (<x, x'> ∈ alpha-rename-alist(t;L))))
BY
{ (Intros
   THEN Unfold `alpha-rename-alist` 0
   THEN (Enough to prove ∀Z:varname() List × ((varname() × varname()) List)
                           ∃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:
                                            Z)))
          Because (BHyp -1 THEN Auto))
   THEN ListInd (-3)
   THEN Auto
   THEN GenListD (-2)
   THEN Reduce 0) }

1
1. [opr] : Type
2. t : term(opr)
3. x : varname()
4. u : varname()
5. v : varname() List
6. (x ∈ v)
⇒ (∀Z:varname() List × ((varname() × varname()) List)
      ∃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:
                        v
                      with starting value:
                       Z))))
7. (x = u ∈ varname()) ∨ (x ∈ v)
8. Z : varname() List × ((varname() × varname()) List)
⊢ ∃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:
                    v
                  with starting value:
                   let vs,tab = Z 
                   in eval x' = maybe_new_var(u;vs) in
                      <[x' / vs], [<u, x'> / tab]>)))

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unfold  `alpha-rename-alist`  0
  THEN  (Enough  to  prove  \mforall{}Z:varname()  List  \mtimes{}  ((varname()  \mtimes{}  varname())  List)
                                                  \mexists{}x':varname()
                                                    (<x,  x'>  \mmember{}  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:
                                                                                    Z)))
                Because  (BHyp  -1  THEN  Auto))
  THEN  ListInd  (-3)
  THEN  Auto
  THEN  GenListD  (-2)
  THEN  Reduce  0)

---

Home Index