Step
*
1
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. f = f1 ∈ opr
11. ||bts|| = ||b1|| ∈ ℤ
12. ∀i:ℕ||bts||
      (alpha-aux(opr;rev(fst(bts[i])) + vs;rev(fst(b1[i])) + ws;snd(bts[i]);snd(b1[i]))
      ∧ (||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ))
13. i : ℕ||b1||
14. ||fst(bts[i])|| = ||fst(b1[i])|| ∈ ℤ
15. alpha-aux(opr;rev(fst(bts[i])) + vs;rev(fst(b1[i])) + ws;snd(bts[i]);snd(b1[i]))
⊢ alpha-aux(opr;rev(fst(b1[i])) + ws;rev(fst(bts[i])) + vs;snd(b1[i]);snd(bts[i]))
BY
{ (RWO "3" (-1) 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.  f  =  f1
11.  ||bts||  =  ||b1||
12.  \mforall{}i:\mBbbN{}||bts||
            (alpha-aux(opr;rev(fst(bts[i]))  +  vs;rev(fst(b1[i]))  +  ws;snd(bts[i]);snd(b1[i]))
            \mwedge{}  (||fst(bts[i])||  =  ||fst(b1[i])||))
13.  i  :  \mBbbN{}||b1||
14.  ||fst(bts[i])||  =  ||fst(b1[i])||
15.  alpha-aux(opr;rev(fst(bts[i]))  +  vs;rev(fst(b1[i]))  +  ws;snd(bts[i]);snd(b1[i]))
\mvdash{}  alpha-aux(opr;rev(fst(b1[i]))  +  ws;rev(fst(bts[i]))  +  vs;snd(b1[i]);snd(bts[i]))
By
Latex:
(RWO  "3"  (-1)  THEN  Auto)
Home
Index