---

Step * 1 of Lemma alpha-rename-alist-nonnullvar


1. [opr] : Type
2. t : term(opr)
3. L : varname() List
4. a1 : varname() List
5. a2 : (varname() × varname()) List
6. x : varname()
7. v : varname()
8. maybe_new_var(x;a1) = v ∈ varname()
9. (x ∈ L)
10. ∀x,x':varname().  ((<x, x'> ∈ a2) ⇒ (x' = nullvar() ∈ varname()) ⇒ (nullvar() ∈ L))
11. x@0 : varname()
12. x' : varname()
13. x@0 = x ∈ varname()
14. x' = v ∈ varname()
15. x' = nullvar() ∈ varname()
16. maybe_new_var(x;a1) = nullvar() ∈ varname()
⊢ (nullvar() ∈ L)
BY
{ (FLemma `maybe_new_var-is-null` [-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.  v  :  varname()
8.  maybe\_new\_var(x;a1)  =  v
9.  (x  \mmember{}  L)
10.  \mforall{}x,x':varname().    ((<x,  x'>  \mmember{}  a2)  {}\mRightarrow{}  (x'  =  nullvar())  {}\mRightarrow{}  (nullvar()  \mmember{}  L))
11.  x@0  :  varname()
12.  x'  :  varname()
13.  x@0  =  x
14.  x'  =  v
15.  x'  =  nullvar()
16.  maybe\_new\_var(x;a1)  =  nullvar()
\mvdash{}  (nullvar()  \mmember{}  L)


By

---

Latex:
(FLemma  `maybe\_new\_var-is-null`  [-1]  THEN  Auto)

---

Home Index