---

Step * 1 1 1 1 1 1 1 1 of Lemma subst-term_functionality


1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. varterm(v) ∈ term(opr)
6. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
7. bnds1 : varname() List
8. bnds2 : varname() List
9. ||bnds1|| = ||bnds2|| ∈ ℤ
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. x : term(opr)
14. apply-alist(VarDeq;s1;v) = (inl x) ∈ (term(opr)?)
15. (v ∈ vars-of-subst(s1))
16. ¬(v ∈ bnds1)
17. ¬(v1 ∈ bnds2)
18. v1 = v ∈ varname()
19. x1 : term(opr)
20. apply-alist(VarDeq;s2;v) = (inl x1) ∈ (term(opr)?)
21. tt = tt
22. alpha-aux(opr;[];[];x;x1)
23. l_disjoint(varname();bnds1;free-vars-aux([];x))
24. l_disjoint(varname();bnds2;free-vars-aux([];x1))
⊢ alpha-aux(opr;bnds1;bnds2;x;x1)
BY
{ (Enough to prove ∀x,x1:term(opr). ∀bnds1,bnds2:varname() List.
                     ((||bnds1|| = ||bnds2|| ∈ ℤ)
                     ⇒ (∀as,bs,cs,ds:varname() List.
                           ((||as|| = ||bs|| ∈ ℤ)
                           ⇒ alpha-aux(opr;as @ cs;bs @ ds;x;x1)
                           ⇒ l_disjoint(varname();bnds1;free-vars-aux(as;x))
                           ⇒ l_disjoint(varname();bnds2;free-vars-aux(bs;x1))
                           ⇒ alpha-aux(opr;as @ bnds1 @ cs;bs @ bnds2 @ ds;x;x1))))
    Because (InstHyp [⌜x⌝;⌜x1⌝;⌜bnds1⌝;⌜bnds2⌝;⌜[]⌝;⌜[]⌝;⌜[]⌝;⌜[]⌝] (-1)⋅
             THEN Auto
             THEN NthHypSq (-1)
             THEN Auto
             THEN Reduce 0
             THEN Auto)) }

1
1. [opr] : Type
2. s1 : (varname() × term(opr)) List
3. s2 : (varname() × term(opr)) List
4. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. varterm(v) ∈ term(opr)
6. v1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
7. bnds1 : varname() List
8. bnds2 : varname() List
9. ||bnds1|| = ||bnds2|| ∈ ℤ
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. x : term(opr)
14. apply-alist(VarDeq;s1;v) = (inl x) ∈ (term(opr)?)
15. (v ∈ vars-of-subst(s1))
16. ¬(v ∈ bnds1)
17. ¬(v1 ∈ bnds2)
18. v1 = v ∈ varname()
19. x1 : term(opr)
20. apply-alist(VarDeq;s2;v) = (inl x1) ∈ (term(opr)?)
21. tt = tt
22. alpha-aux(opr;[];[];x;x1)
23. l_disjoint(varname();bnds1;free-vars-aux([];x))
24. l_disjoint(varname();bnds2;free-vars-aux([];x1))
⊢ ∀x,x1:term(opr). ∀bnds1,bnds2:varname() List.
    ((||bnds1|| = ||bnds2|| ∈ ℤ)
    ⇒ (∀as,bs,cs,ds:varname() List.
          ((||as|| = ||bs|| ∈ ℤ)
          ⇒ alpha-aux(opr;as @ cs;bs @ ds;x;x1)
          ⇒ l_disjoint(varname();bnds1;free-vars-aux(as;x))
          ⇒ l_disjoint(varname();bnds2;free-vars-aux(bs;x1))
          ⇒ alpha-aux(opr;as @ bnds1 @ cs;bs @ bnds2 @ ds;x;x1))))

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  s1  :  (varname()  \mtimes{}  term(opr))  List
3.  s2  :  (varname()  \mtimes{}  term(opr))  List
4.  v  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
5.  varterm(v)  \mmember{}  term(opr)
6.  v1  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
7.  bnds1  :  varname()  List
8.  bnds2  :  varname()  List
9.  ||bnds1||  =  ||bnds2||
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.  x  :  term(opr)
14.  apply-alist(VarDeq;s1;v)  =  (inl  x)
15.  (v  \mmember{}  vars-of-subst(s1))
16.  \mneg{}(v  \mmember{}  bnds1)
17.  \mneg{}(v1  \mmember{}  bnds2)
18.  v1  =  v
19.  x1  :  term(opr)
20.  apply-alist(VarDeq;s2;v)  =  (inl  x1)
21.  tt  =  tt
22.  alpha-aux(opr;[];[];x;x1)
23.  l\_disjoint(varname();bnds1;free-vars-aux([];x))
24.  l\_disjoint(varname();bnds2;free-vars-aux([];x1))
\mvdash{}  alpha-aux(opr;bnds1;bnds2;x;x1)


By

---

Latex:
(Enough  to  prove  \mforall{}x,x1:term(opr).  \mforall{}bnds1,bnds2:varname()  List.
                                      ((||bnds1||  =  ||bnds2||)
                                      {}\mRightarrow{}  (\mforall{}as,bs,cs,ds:varname()  List.
                                                  ((||as||  =  ||bs||)
                                                  {}\mRightarrow{}  alpha-aux(opr;as  @  cs;bs  @  ds;x;x1)
                                                  {}\mRightarrow{}  l\_disjoint(varname();bnds1;free-vars-aux(as;x))
                                                  {}\mRightarrow{}  l\_disjoint(varname();bnds2;free-vars-aux(bs;x1))
                                                  {}\mRightarrow{}  alpha-aux(opr;as  @  bnds1  @  cs;bs  @  bnds2  @  ds;x;x1))))
    Because  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}bnds1\mkleeneclose{};\mkleeneopen{}bnds2\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}
                      THEN  Auto
                      THEN  NthHypSq  (-1)
                      THEN  Auto
                      THEN  Reduce  0
                      THEN  Auto))

---

Home Index