---

Step * 1 1 6 1 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'> ∈ (varname() × varname())
19. (<y, y'> ∈ a2)
20. x'@0 = y' ∈ varname()
⊢ x@0 = y ∈ varname()
BY
{ (((EqHD (-3) THENA Auto) THEN All Reduce)
   THEN (FHyp 9 [-2] THENA Auto)
   THEN (Enough to prove ¬(maybe_new_var(x;a1) = y' ∈ varname())
          Because (D -1 THEN Eq))
   THEN (InstLemma `maybe_new_var-distinct` [⌜x⌝;⌜a1⌝]⋅ THENA Auto)
   THEN RWO "l_all_iff" (-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.  y  :  varname()
17.  y'  :  varname()
18.  <x@0,  x'@0>  =  <x,  x'>
19.  (<y,  y'>  \mmember{}  a2)
20.  x'@0  =  y'
\mvdash{}  x@0  =  y


By

---

Latex:
(((EqHD  (-3)  THENA  Auto)  THEN  All  Reduce)
  THEN  (FHyp  9  [-2]  THENA  Auto)
  THEN  (Enough  to  prove  \mneg{}(maybe\_new\_var(x;a1)  =  y')
                Because  (D  -1  THEN  Eq))
  THEN  (InstLemma  `maybe\_new\_var-distinct`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "l\_all\_iff"  (-1)
  THEN  Auto)

---

Home Index