---

Step * 1 1 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)?)
⊢ alpha-aux(opr;bnds1;bnds2;varterm(v);case apply-alist(VarDeq;s2;v1) of inl(a) => a | inr(_) => varterm(v1))
BY
{ ((GenConclTerm ⌜apply-alist(VarDeq;s2;v1)⌝⋅ THENA Auto) THEN D -2 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)
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)

2
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))

---

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  )
\mvdash{}  alpha-aux(opr;bnds1;bnds2;varterm(v);case  apply-alist(VarDeq;s2;v1)
  of  inl(a)  =>
  a
  |  inr($_{}$)  =>
  varterm(v1))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}apply-alist(VarDeq;s2;v1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)

---

Home Index