---

Step * of Lemma alpha-rename-alist-nonnullvar

No Annotations
∀[opr:Type]
  ∀t:term(opr). ∀L:varname() List. ∀x,x':varname().
    ((<x, x'> ∈ alpha-rename-alist(t;L)) ⇒ (x' = nullvar() ∈ varname()) ⇒ (nullvar() ∈ L))
BY
{ (RepeatFor 3 (Intro)
   THEN Unfold `alpha-rename-alist` 0
   THEN ProveListAccumInvWithType ⌜varname() List × ((varname() × varname()) List)⌝⋅
   THEN Try (Complete (Auto))
   THEN Intro
   THEN D -1
   THEN Reduce 0
   THEN Intro
   THEN (GenConclTerm ⌜maybe_new_var(x;a1)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN GenListD (-2)
   THEN D -2
   THEN Auto
   THEN (EqHD (-2) THENA Auto)
   THEN All Reduce
   THEN (Assert maybe_new_var(x;a1) = nullvar() ∈ varname() BY
               Eq)) }

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. 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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}t:term(opr).  \mforall{}L:varname()  List.  \mforall{}x,x':varname().
        ((<x,  x'>  \mmember{}  alpha-rename-alist(t;L))  {}\mRightarrow{}  (x'  =  nullvar())  {}\mRightarrow{}  (nullvar()  \mmember{}  L))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  Unfold  `alpha-rename-alist`  0
  THEN  ProveListAccumInvWithType  \mkleeneopen{}varname()  List  \mtimes{}  ((varname()  \mtimes{}  varname())  List)\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Intro
  THEN  D  -1
  THEN  Reduce  0
  THEN  Intro
  THEN  (GenConclTerm  \mkleeneopen{}maybe\_new\_var(x;a1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  GenListD  (-2)
  THEN  D  -2
  THEN  Auto
  THEN  (EqHD  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  (Assert  maybe\_new\_var(x;a1)  =  nullvar()  BY
                          Eq))

---

Home Index