---

Step * 1 1 2 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. y : Unit
14. apply-alist(VarDeq;s1;v) = (inr y ) ∈ (term(opr)?)
15. x : term(opr)
16. apply-alist(VarDeq;s2;v1) = (inl x) ∈ (term(opr)?)
⊢ alpha-aux(opr;bnds1;bnds2;varterm(v);x)
BY
{ (DVar `v'
   THEN DVar `v1'
   THEN (Assert (v1 ∈ vars-of-subst(s2)) 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(v1;free-vars(x))⌝]⋅
                THEN Auto
                THEN ((InstConcl [⌜<v1, x>⌝] ⋅ THEN Reduce 0) ORELSE RWO "member-insert" 0)
                THEN Auto))
   THEN (Assert ¬(v1 ∈ bnds2) BY
               ((D 0 THENA Auto) THEN (D 13 With ⌜v1⌝  THENA Auto) THEN D -1 THEN Auto))
   THEN (RWO "same-binding-symm" (-7) THENA Auto)
   THEN (FLemma `same-binding-not-bound` [-7;-1] THENA Auto)
   THEN D -1) }

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

---

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.  y  :  Unit
14.  apply-alist(VarDeq;s1;v)  =  (inr  y  )
15.  x  :  term(opr)
16.  apply-alist(VarDeq;s2;v1)  =  (inl  x)
\mvdash{}  alpha-aux(opr;bnds1;bnds2;varterm(v);x)


By

---

Latex:
(DVar  `v'
  THEN  DVar  `v1'
  THEN  (Assert  (v1  \mmember{}  vars-of-subst(s2))  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(v1;free-vars(x))\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  ((InstConcl  [\mkleeneopen{}<v1,  x>\mkleeneclose{}]  \mcdot{}  THEN  Reduce  0)  ORELSE  RWO  "member-insert"  0)
                            THEN  Auto))
  THEN  (Assert  \mneg{}(v1  \mmember{}  bnds2)  BY
                          ((D  0  THENA  Auto)  THEN  (D  13  With  \mkleeneopen{}v1\mkleeneclose{}    THENA  Auto)  THEN  D  -1  THEN  Auto))
  THEN  (RWO  "same-binding-symm"  (-7)  THENA  Auto)
  THEN  (FLemma  `same-binding-not-bound`  [-7;-1]  THENA  Auto)
  THEN  D  -1)

---

Home Index