---

Step * 1 1 2 of Lemma alpha-rename-alist-property


1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. (x ∈ L)
8. L @ all-vars(t) ⊆ a1
9. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' ∈ a1))
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t)))))
11. ∀x,x',y,y':varname().  ((<x, x'> ∈ a2) ⇒ (<y, y'> ∈ a2) ⇒ (x' = y' ∈ varname()) ⇒ (x = y ∈ varname()))
12. x' : varname()
13. maybe_new_var(x;a1) = x' ∈ varname()
14. x@0 : varname()
15. x'@0 : varname()
16. (<x@0, x'@0> ∈ a2)
⊢ (x'@0 ∈ [x' / a1])
BY
{ (FHyp 9 [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  t  :  term(opr)
3.  L  :  varname()  List
4.  a1  :  varname()  List
5.  a2  :  (varname()  \mtimes{}  varname())  List
6.  x  :  varname()
7.  (x  \mmember{}  L)
8.  L  @  all-vars(t)  \msubseteq{}  a1
9.  \mforall{}x,x':varname().    ((<x,  x'>  \mmember{}  a2)  {}\mRightarrow{}  (x'  \mmember{}  a1))
10.  \mforall{}x,x':varname().    ((<x,  x'>  \mmember{}  a2)  {}\mRightarrow{}  ((x  \mmember{}  L)  \mwedge{}  (\mneg{}(x'  \mmember{}  L  @  all-vars(t)))))
11.  \mforall{}x,x',y,y':varname().    ((<x,  x'>  \mmember{}  a2)  {}\mRightarrow{}  (<y,  y'>  \mmember{}  a2)  {}\mRightarrow{}  (x'  =  y')  {}\mRightarrow{}  (x  =  y))
12.  x'  :  varname()
13.  maybe\_new\_var(x;a1)  =  x'
14.  x@0  :  varname()
15.  x'@0  :  varname()
16.  (<x@0,  x'@0>  \mmember{}  a2)
\mvdash{}  (x'@0  \mmember{}  [x'  /  a1])


By

---

Latex:
(FHyp  9  [-1]  THEN  Auto)

---

Home Index