---

Step * 1 1 3 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> = <x, x'> ∈ (varname() × varname())
⊢ (x@0 ∈ L) ∧ (¬(x'@0 ∈ L @ all-vars(t)))
BY
{ ((EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN RWO "-1 -2" 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN (InstLemma `maybe_new_var-distinct` [⌜x⌝;⌜a1⌝]⋅ THENA Auto)
   THEN RWO "l_all_iff" (-1)
   THEN Auto
   THEN (InstHyp [⌜x'⌝] (-1)⋅ THEN Auto)
   THEN Unfold `l_contains` 8
   THEN RWO "l_all_iff" 8
   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>  =  <x,  x'>
\mvdash{}  (x@0  \mmember{}  L)  \mwedge{}  (\mneg{}(x'@0  \mmember{}  L  @  all-vars(t)))


By

---

Latex:
((EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  RWO  "-1  -2"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `maybe\_new\_var-distinct`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "l\_all\_iff"  (-1)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x'\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  THEN  Unfold  `l\_contains`  8
  THEN  RWO  "l\_all\_iff"  8
  THEN  Auto)

---

Home Index