---

Step * 1 1 1 of Lemma subst-term_functionality


1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
6. varterm(v) ∈ term(opr)
7. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
8. bnds1 : varname() List
9. bnds2 : varname() List
10. l_disjoint(varname();bnds1;vars-of-subst(s1))
11. l_disjoint(varname();bnds2;vars-of-subst(s2))
12. ↑same-binding(bnds1;bnds2;v;v1)
13. x : term(opr)
14. apply-alist(VarDeq;s1;v) = (inl x) ∈ (term(opr)?)
⊢ alpha-aux(opr;bnds1;bnds2;x;case apply-alist(VarDeq;s2;v1) of inl(a) => a | inr(_) => varterm(v1))
BY
{ ((Assert (v ∈ vars-of-subst(s1)) BY
          ((FLemma `apply-alist-inl` [-1] THENA Auto)
           THEN Unfold `vars-of-subst` 0
           THEN (BLemma `member-l-union-list` THENA Auto)
           THEN ((RWO "member-map" 0 THENA Auto) THEN Reduce 0)
           THEN InstConcl [⌜insert(v;free-vars(x))⌝]⋅
           THEN Auto
           THEN ((InstConcl [⌜<v, x>⌝] ⋅ THEN Reduce 0) ORELSE RWO "member-insert" 0)
           THEN Auto))
   THEN (Assert ¬(v ∈ bnds1) BY
               ((D 0 THENA Auto) THEN (D 10 With ⌜v⌝  THENA Auto) THEN D -1 THEN Auto))
   THEN (FLemma `same-binding-not-bound` [-5;-1] THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN PromoteHyp (-1) 10) }

1
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. equiv-substs(opr;s1;s2)
5. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
6. varterm(v) ∈ term(opr)
7. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
8. bnds1 : varname() List
9. bnds2 : varname() List
10. ||bnds1|| = ||bnds2|| ∈ ℤ
11. l_disjoint(varname();bnds1;vars-of-subst(s1))
12. l_disjoint(varname();bnds2;vars-of-subst(s2))
13. ↑same-binding(bnds1;bnds2;v;v1)
14. x : term(opr)
15. apply-alist(VarDeq;s1;v) = (inl x) ∈ (term(opr)?)
16. (v ∈ vars-of-subst(s1))
17. ¬(v ∈ bnds1)
18. ¬(v1 ∈ bnds2)
19. v1 = v ∈ varname()
⊢ alpha-aux(opr;bnds1;bnds2;x;case apply-alist(VarDeq;s2;v1) of inl(a) => a | inr(_) => varterm(v1))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  s1  :  (varname()  \mtimes{}  term(opr))  List
3.  s2  :  (varname()  \mtimes{}  term(opr))  List
4.  equiv-substs(opr;s1;s2)
5.  v  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
6.  varterm(v)  \mmember{}  term(opr)
7.  v1  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
8.  bnds1  :  varname()  List
9.  bnds2  :  varname()  List
10.  l\_disjoint(varname();bnds1;vars-of-subst(s1))
11.  l\_disjoint(varname();bnds2;vars-of-subst(s2))
12.  \muparrow{}same-binding(bnds1;bnds2;v;v1)
13.  x  :  term(opr)
14.  apply-alist(VarDeq;s1;v)  =  (inl  x)
\mvdash{}  alpha-aux(opr;bnds1;bnds2;x;case  apply-alist(VarDeq;s2;v1)  of  inl(a)  =>  a  |  inr($_{\mbackslash{}ff\000C7d$)  =>  varterm(v1))


By

---

Latex:
((Assert  (v  \mmember{}  vars-of-subst(s1))  BY
                ((FLemma  `apply-alist-inl`  [-1]  THENA  Auto)
                  THEN  Unfold  `vars-of-subst`  0
                  THEN  (BLemma  `member-l-union-list`  THENA  Auto)
                  THEN  ((RWO  "member-map"  0  THENA  Auto)  THEN  Reduce  0)
                  THEN  InstConcl  [\mkleeneopen{}insert(v;free-vars(x))\mkleeneclose{}]\mcdot{}
                  THEN  Auto
                  THEN  ((InstConcl  [\mkleeneopen{}<v,  x>\mkleeneclose{}]  \mcdot{}  THEN  Reduce  0)  ORELSE  RWO  "member-insert"  0)
                  THEN  Auto))
  THEN  (Assert  \mneg{}(v  \mmember{}  bnds1)  BY
                          ((D  0  THENA  Auto)  THEN  (D  10  With  \mkleeneopen{}v\mkleeneclose{}    THENA  Auto)  THEN  D  -1  THEN  Auto))
  THEN  (FLemma  `same-binding-not-bound`  [-5;-1]  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  PromoteHyp  (-1)  10)

---

Home Index