---

Step * 1 1 2 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. ¬(v = nullvar() ∈ varname())
5. varterm(v) ∈ term(opr)
6. bnds : varname() List
7. ¬(v ∈ bnds)
8. f : {v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))}  ⟶ varname()
9. ∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
     ((f x ∈ free-vars-aux(bnds;varterm(v))) ⇒ ((f x) = x ∈ varname()))
10. ∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
      (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
11. Inj({v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} ;varname();f)
12. map(f;bnds) ∈ varname() List
13. all-vars(varterm(v)) ~ [v]
⊢ ↑same-binding(map(f;bnds);bnds;v;v)
BY
{ (Assert ¬(v ∈ map(f;bnds)) BY
         ((D 0 THENA Auto)
          THEN (GenListD (-1) THEN ExRepD)
          THEN (InstHyp [⌜y⌝] (-8)⋅ THENA Auto)
          THEN (((Unfold `free-vars-aux` 0 THEN Reduce 0) THEN AutoSplit)
          ORELSE (D 7 THEN Subst' v = y ∈ varname() 0 THEN Auto)
          ))) }

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. ¬(v = nullvar() ∈ varname())
5. varterm(v) ∈ term(opr)
6. bnds : varname() List
7. ¬(v ∈ bnds)
8. f : {v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))}  ⟶ varname()
9. ∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
     ((f x ∈ free-vars-aux(bnds;varterm(v))) ⇒ ((f x) = x ∈ varname()))
10. ∀x:{v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} 
      (((f x) = nullvar() ∈ varname()) ⇒ (x = nullvar() ∈ varname()))
11. Inj({v@0:varname()| (v@0 ∈ bnds @ all-vars(varterm(v)))} ;varname();f)
12. map(f;bnds) ∈ varname() List
13. all-vars(varterm(v)) ~ [v]
14. ¬(v ∈ map(f;bnds))
⊢ ↑same-binding(map(f;bnds);bnds;v;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.  \mneg{}(v  =  nullvar())
5.  varterm(v)  \mmember{}  term(opr)
6.  bnds  :  varname()  List
7.  \mneg{}(v  \mmember{}  bnds)
8.  f  :  \{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\}    {}\mrightarrow{}  varname()
9.  \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))
10.  \mforall{}x:\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\} 
            (((f  x)  =  nullvar())  {}\mRightarrow{}  (x  =  nullvar()))
11.  Inj(\{v@0:varname()|  (v@0  \mmember{}  bnds  @  all-vars(varterm(v)))\}  ;varname();f)
12.  map(f;bnds)  \mmember{}  varname()  List
13.  all-vars(varterm(v))  \msim{}  [v]
\mvdash{}  \muparrow{}same-binding(map(f;bnds);bnds;v;v)


By

---

Latex:
(Assert  \mneg{}(v  \mmember{}  map(f;bnds))  BY
              ((D  0  THENA  Auto)
                THEN  (GenListD  (-1)  THEN  ExRepD)
                THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-8)\mcdot{}  THENA  Auto)
                THEN  (((Unfold  `free-vars-aux`  0  THEN  Reduce  0)  THEN  AutoSplit)
                ORELSE  (D  7  THEN  Subst'  v  =  y  0  THEN  Auto)
                )))

---

Home Index