---

Step * 1 of Lemma alpha-avoid-equivalent


1. opr : Type
2. t : term(opr)
3. L : varname() List
4. ¬(nullvar() ∈ L)
5. x : {v:varname()| (v ∈ all-vars(t))} 
6. (alist-map(VarDeq;alpha-rename-alist(t;L)) x ∈ free-vars(t))
⊢ (alist-map(VarDeq;alpha-rename-alist(t;L)) x) = x ∈ varname()
BY
{ ((MoveToConcl (-1) THEN Unfold `alist-map` 0)
   THEN Reduce 0
   THEN (GenConclAtAddr [2;2;1] THEN D -2 THEN Reduce 0)
   THEN Auto
   THEN (FLemma `apply-alist-inl` [-2] THENA Auto)
   THEN (Assert ¬(x1 ∈ L @ all-vars(t)) BY
               (InstLemma `alpha-rename-alist-property` [⌜opr⌝;⌜t⌝;⌜L⌝]⋅ THEN Auto))
   THEN D -1) }

1
1. opr : Type
2. t : term(opr)
3. L : varname() List
4. ¬(nullvar() ∈ L)
5. x : {v:varname()| (v ∈ all-vars(t))} 
6. x1 : varname()
7. apply-alist(VarDeq;alpha-rename-alist(t;L);x) = (inl x1) ∈ (varname()?)
8. (x1 ∈ free-vars(t))
9. (<x, x1> ∈ alpha-rename-alist(t;L))
⊢ (x1 ∈ L @ all-vars(t))

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  term(opr)
3.  L  :  varname()  List
4.  \mneg{}(nullvar()  \mmember{}  L)
5.  x  :  \{v:varname()|  (v  \mmember{}  all-vars(t))\} 
6.  (alist-map(VarDeq;alpha-rename-alist(t;L))  x  \mmember{}  free-vars(t))
\mvdash{}  (alist-map(VarDeq;alpha-rename-alist(t;L))  x)  =  x


By

---

Latex:
((MoveToConcl  (-1)  THEN  Unfold  `alist-map`  0)
  THEN  Reduce  0
  THEN  (GenConclAtAddr  [2;2;1]  THEN  D  -2  THEN  Reduce  0)
  THEN  Auto
  THEN  (FLemma  `apply-alist-inl`  [-2]  THENA  Auto)
  THEN  (Assert  \mneg{}(x1  \mmember{}  L  @  all-vars(t))  BY
                          (InstLemma  `alpha-rename-alist-property`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  D  -1)

---

Home Index