---

Step * 2 of Lemma alpha-aux-mkterm


1. opr : Type
2. a : opr
3. b : opr
4. u2 : varname() List
5. u3 : term(opr)
6. v : bound-term(opr) List
7. ∀bs:bound-term(opr) List. ∀vs,ws:varname() List.
     (alpha-aux(opr;vs;ws;mkterm(a;v);mkterm(b;bs))
     ⇐⇒ (a = b ∈ opr)
         ∧ (||v|| = ||bs|| ∈ ℤ)
         ∧ (∀i:ℕ||v||
              (alpha-aux(opr;rev(fst(v[i])) + vs;rev(fst(bs[i])) + ws;snd(v[i]);snd(bs[i]))
              ∧ (||fst(v[i])|| = ||fst(bs[i])|| ∈ ℤ))))
8. u4 : varname() List
9. u5 : term(opr)
10. v1 : bound-term(opr) List
11. ∀vs,ws:varname() List.
      (alpha-aux(opr;vs;ws;mkterm(a;[<u2, u3> / v]);mkterm(b;v1))
      ⇐⇒ (a = b ∈ opr)
          ∧ ((||v|| + 1) = ||v1|| ∈ ℤ)
          ∧ (∀i:ℕ||v|| + 1
               (alpha-aux(opr;rev(fst([<u2, u3> / v][i])) + vs;rev(fst(v1[i])) + ws;snd([<u2, u3> / v][i]);snd(v1[i]))
               ∧ (||fst([<u2, u3> / v][i])|| = ||fst(v1[i])|| ∈ ℤ))))
12. vs : varname() List
13. ws : varname() List
14. a = b ∈ opr
15. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
16. i : ℕ||v||
17. alpha-aux(opr;rev(fst(v[(i + 1) - 1])) + vs;rev(fst(v1[(i + 1) - 1])) + ws;snd(v[(i + 1) - 1]);snd(v1[(i + 1) - 1]))
18. ||fst(v[(i + 1) - 1])|| = ||fst(v1[(i + 1) - 1])|| ∈ ℤ
⊢ ||fst(v[i])|| = ||fst(v1[i])|| ∈ ℤ
BY
{ (Subst' (i + 1) - 1 ~ i -1 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  a  :  opr
3.  b  :  opr
4.  u2  :  varname()  List
5.  u3  :  term(opr)
6.  v  :  bound-term(opr)  List
7.  \mforall{}bs:bound-term(opr)  List.  \mforall{}vs,ws:varname()  List.
          (alpha-aux(opr;vs;ws;mkterm(a;v);mkterm(b;bs))
          \mLeftarrow{}{}\mRightarrow{}  (a  =  b)
                  \mwedge{}  (||v||  =  ||bs||)
                  \mwedge{}  (\mforall{}i:\mBbbN{}||v||
                            (alpha-aux(opr;rev(fst(v[i]))  +  vs;rev(fst(bs[i]))  +  ws;snd(v[i]);snd(bs[i]))
                            \mwedge{}  (||fst(v[i])||  =  ||fst(bs[i])||))))
8.  u4  :  varname()  List
9.  u5  :  term(opr)
10.  v1  :  bound-term(opr)  List
11.  \mforall{}vs,ws:varname()  List.
            (alpha-aux(opr;vs;ws;mkterm(a;[<u2,  u3>  /  v]);mkterm(b;v1))
            \mLeftarrow{}{}\mRightarrow{}  (a  =  b)
                    \mwedge{}  ((||v||  +  1)  =  ||v1||)
                    \mwedge{}  (\mforall{}i:\mBbbN{}||v||  +  1
                              (alpha-aux(opr;rev(fst([<u2,  u3>  / 
                                                                              v][i]))  +  vs;rev(fst(v1[i]))  +  ws;snd([<u2,  u3>  / 
                                                                                                                                                            v][i]);snd(v1[i]))
                              \mwedge{}  (||fst([<u2,  u3>  /  v][i])||  =  ||fst(v1[i])||))))
12.  vs  :  varname()  List
13.  ws  :  varname()  List
14.  a  =  b
15.  (||v||  +  1)  =  (||v1||  +  1)
16.  i  :  \mBbbN{}||v||
17.  alpha-aux(opr;rev(fst(v[(i  +  1)  -  1]))  +  vs;rev(fst(v1[(i  +  1)  -  1]))  +  ws;snd(v[(i  +  1) 
-  1]);snd(v1[(i  +  1)  -  1]))
18.  ||fst(v[(i  +  1)  -  1])||  =  ||fst(v1[(i  +  1)  -  1])||
\mvdash{}  ||fst(v[i])||  =  ||fst(v1[i])||


By

---

Latex:
(Subst'  (i  +  1)  -  1  \msim{}  i  -1  THEN  Auto)

---

Home Index