---

Step * 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. alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
13. binders-disjoint(opr;vars-of-subst(s1);varterm(v))
14. binders-disjoint(opr;vars-of-subst(s2);varterm(v1))
⊢ alpha-aux(opr;bnds1;bnds2;replace-vars(s1;varterm(v));replace-vars(s2;varterm(v1)))
BY
{ (RepeatFor 2 (Thin (-1)) THEN Unfold `alpha-aux` -1 THEN Reduce -1 THEN Unfold `replace-vars` 0 THEN Reduce 0) }

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. l_disjoint(varname();bnds1;vars-of-subst(s1))
11. l_disjoint(varname();bnds2;vars-of-subst(s2))
12. ↑same-binding(bnds1;bnds2;v;v1)
⊢ alpha-aux(opr;bnds1;bnds2;case apply-alist(VarDeq;s1;v)
 of inl(a) =>
 a
 | inr(_) =>
 varterm(v);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.  alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
13.  binders-disjoint(opr;vars-of-subst(s1);varterm(v))
14.  binders-disjoint(opr;vars-of-subst(s2);varterm(v1))
\mvdash{}  alpha-aux(opr;bnds1;bnds2;replace-vars(s1;varterm(v));replace-vars(s2;varterm(v1)))


By

---

Latex:
(RepeatFor  2  (Thin  (-1))
  THEN  Unfold  `alpha-aux`  -1
  THEN  Reduce  -1
  THEN  Unfold  `replace-vars`  0
  THEN  Reduce  0)

---

Home Index