---

Step * 1 1 2 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 : 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)
BY
{ (D -1
   THEN Thin (-1)
   THEN (RWO "-1<" (-5) THENA Auto)
   THEN (D 4 With ⌜v⌝  THENA Auto)
   THEN D -1
   THEN (RWO "-9 -7" (-2) THENA Auto)
   THEN Reduce -2
   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  :  varname()
6.  [\%12]  :  \mneg{}(v  =  nullvar())
7.  varterm(v)  \mmember{}  term(opr)
8.  v1  :  varname()
9.  [\%14]  :  \mneg{}(v1  =  nullvar())
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.  \muparrow{}same-binding(bnds2;bnds1;v1;v)
15.  y  :  Unit
16.  apply-alist(VarDeq;s1;v)  =  (inr  y  )
17.  x  :  term(opr)
18.  apply-alist(VarDeq;s2;v1)  =  (inl  x)
19.  (v1  \mmember{}  vars-of-subst(s2))
20.  \mneg{}(v1  \mmember{}  bnds2)
21.  \mneg{}(v  \mmember{}  bnds1)
22.  (v  =  v1)  \mwedge{}  (||bnds2||  =  ||bnds1||)
\mvdash{}  alpha-aux(opr;bnds1;bnds2;varterm(v);x)


By

---

Latex:
(D  -1
  THEN  Thin  (-1)
  THEN  (RWO  "-1<"  (-5)  THENA  Auto)
  THEN  (D  4  With  \mkleeneopen{}v\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (RWO  "-9  -7"  (-2)  THENA  Auto)
  THEN  Reduce  -2
  THEN  Auto)

---

Home Index