---

Step * 1 1 6 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. y : varname()
17. y' : varname()
18. (<x@0, x'@0> ∈ [<x, x'> / a2])
19. (<y, y'> ∈ a2)
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()
BY
{ (GenListD (-3) THEN D -3) }

1
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. y : varname()
17. y' : varname()
18. <x@0, x'@0> = <x, x'> ∈ (varname() × varname())
19. (<y, y'> ∈ a2)
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()

2
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. y : varname()
17. y' : varname()
18. (<x@0, x'@0> ∈ a2)
19. (<y, y'> ∈ a2)
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()

---

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.  y  :  varname()
17.  y'  :  varname()
18.  (<x@0,  x'@0>  \mmember{}  [<x,  x'>  /  a2])
19.  (<y,  y'>  \mmember{}  a2)
20.  x'@0  =  y'
\mvdash{}  x@0  =  y


By

---

Latex:
(GenListD  (-3)  THEN  D  -3)

---

Home Index