---

Step * 2 of Lemma alpha-aux-symm


1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀b:term(opr). ∀vs,ws:varname() List.  (alpha-aux(opr;vs;ws;snd(bt);b) ⇐⇒ alpha-aux(opr;ws;vs;b;snd(bt)))))
4. f : opr
5. b1 : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀vs,ws:varname() List.
           (alpha-aux(opr;vs;ws;mkterm(f;bts);snd(bt)) ⇐⇒ alpha-aux(opr;ws;vs;snd(bt);mkterm(f;bts)))))
7. f1 : opr
8. vs : varname() List
9. ws : varname() List
10. f1 = f ∈ opr
11. ||b1|| = ||bts|| ∈ ℤ
12. ∀i:ℕ||b1||
      (alpha-aux(opr;rev(fst(b1[i])) + ws;rev(fst(bts[i])) + vs;snd(b1[i]);snd(bts[i]))
      ∧ (||fst(b1[i])|| = ||fst(bts[i])|| ∈ ℤ))
13. i : ℕ||bts||
14. ||fst(b1[i])|| = ||fst(bts[i])|| ∈ ℤ
15. alpha-aux(opr;rev(fst(b1[i])) + ws;rev(fst(bts[i])) + vs;snd(b1[i]);snd(bts[i]))
⊢ alpha-aux(opr;rev(fst(bts[i])) + vs;rev(fst(b1[i])) + ws;snd(bts[i]);snd(b1[i]))
BY
{ (RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  bts  :  bound-term(opr)  List
3.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  bts)
          {}\mRightarrow{}  (\mforall{}b:term(opr).  \mforall{}vs,ws:varname()  List.
                      (alpha-aux(opr;vs;ws;snd(bt);b)  \mLeftarrow{}{}\mRightarrow{}  alpha-aux(opr;ws;vs;b;snd(bt)))))
4.  f  :  opr
5.  b1  :  bound-term(opr)  List
6.  \mforall{}bt:bound-term(opr)
          ((bt  \mmember{}  b1)
          {}\mRightarrow{}  (\mforall{}vs,ws:varname()  List.
                      (alpha-aux(opr;vs;ws;mkterm(f;bts);snd(bt))
                      \mLeftarrow{}{}\mRightarrow{}  alpha-aux(opr;ws;vs;snd(bt);mkterm(f;bts)))))
7.  f1  :  opr
8.  vs  :  varname()  List
9.  ws  :  varname()  List
10.  f1  =  f
11.  ||b1||  =  ||bts||
12.  \mforall{}i:\mBbbN{}||b1||
            (alpha-aux(opr;rev(fst(b1[i]))  +  ws;rev(fst(bts[i]))  +  vs;snd(b1[i]);snd(bts[i]))
            \mwedge{}  (||fst(b1[i])||  =  ||fst(bts[i])||))
13.  i  :  \mBbbN{}||bts||
14.  ||fst(b1[i])||  =  ||fst(bts[i])||
15.  alpha-aux(opr;rev(fst(b1[i]))  +  ws;rev(fst(bts[i]))  +  vs;snd(b1[i]);snd(bts[i]))
\mvdash{}  alpha-aux(opr;rev(fst(bts[i]))  +  vs;rev(fst(b1[i]))  +  ws;snd(bts[i]);snd(b1[i]))


By

---

Latex:
(RWO  "3"  0  THEN  Auto)

---

Home Index