---

Step * 1 of Lemma alpha-rename-equivalent


1. [opr] : Type
2. ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
     (map(f;bnds) ∈ varname() List)
3. v : varname()
4. [%3] : ¬(v = nullvar() ∈ varname())
5. varterm(v) ∈ term(opr)
6. bnds : varname() List
7. f : {v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))}  ⟶ varname()
8. [%] : ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
             ((f x ∈ free-vars-aux(bnds;varterm(v))) ⇒ ((f x) = x ∈ varname())))
∧ (∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
     (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
∧ Inj({v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} ;varname();f)
⊢ alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;varterm(v));varterm(v))
BY
{ ((InstHyp [⌜varterm(v)⌝;⌜bnds⌝;⌜f⌝] 2⋅ THENA Auto) THEN (Assert all-vars(varterm(v)) ~ [v] BY Computation)) }

1
1. [opr] : Type
2. ∀t:term(opr). ∀bnds:varname() List. ∀f:{v:varname()| (v ∈ bnds @ all-vars(t))}  ⟶ varname().
     (map(f;bnds) ∈ varname() List)
3. v : varname()
4. [%3] : ¬(v = nullvar() ∈ varname())
5. varterm(v) ∈ term(opr)
6. bnds : varname() List
7. f : {v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))}  ⟶ varname()
8. [%] : ((∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
             ((f x ∈ free-vars-aux(bnds;varterm(v))) ⇒ ((f x) = x ∈ varname())))
∧ (∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
     (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))))
∧ Inj({v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} ;varname();f)
9. map(f;bnds) ∈ varname() List
10. all-vars(varterm(v)) ~ [v]
⊢ alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;varterm(v));varterm(v))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  \mforall{}t:term(opr).  \mforall{}bnds:varname()  List.  \mforall{}f:\{v:varname()|  (v  \mmember{}  bnds  @  all-vars(t))\}    {}\mrightarrow{}  varname().
          (map(f;bnds)  \mmember{}  varname()  List)
3.  v  :  varname()
4.  [\%3]  :  \mneg{}(v  =  nullvar())
5.  varterm(v)  \mmember{}  term(opr)
6.  bnds  :  varname()  List
7.  f  :  \{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\}    {}\mrightarrow{}  varname()
8.  [\%]  :  ((\mforall{}x:\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\} 
                          ((f  x  \mmember{}  free-vars-aux(bnds;varterm(v)))  {}\mRightarrow{}  ((f  x)  =  x)))
\mwedge{}  (\mforall{}x:\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\} 
          (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))))
\mwedge{}  Inj(\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\}  ;varname();f)
\mvdash{}  alpha-aux(opr;map(f;bnds);bnds;alpha-rename-aux(f;bnds;varterm(v));varterm(v))


By

---

Latex:
((InstHyp  [\mkleeneopen{}varterm(v)\mkleeneclose{};\mkleeneopen{}bnds\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  (Assert  all-vars(varterm(v))  \msim{}  [v]  BY
                          Computation)
  )

---

Home Index