---

Step * 1 1 2 2 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. y1 : Unit
16. apply-alist(VarDeq;s2;v1) = (inr y1 ) ∈ (term(opr)?)
⊢ alpha-aux(opr;bnds1;bnds2;varterm(v);varterm(v1))
BY
{ ((Unfold `alpha-aux` 0 THEN Reduce 0) THEN Auto) }

---

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


By

---

Latex:
((Unfold  `alpha-aux`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index