---

Step * of Lemma alpha-aux-symm

No Annotations
∀[opr:Type]. ∀a,b:term(opr). ∀vs,ws:varname() List.  (alpha-aux(opr;vs;ws;a;b) ⇐⇒ alpha-aux(opr;ws;vs;b;a))
BY
{ (Intro
   THEN ((BLemma `term-induction` THENW Auto)
         THEN Intro
         THEN (((Assert varterm(v) ∈ term(opr) BY Auto) THEN RenameVar `a' (-2)) ORELSE RepeatFor 2 (Intro)))
   THEN ((BLemma `term-induction` THENW Auto)
         THEN Intro
         THEN (((Assert varterm(v) ∈ term(opr) BY Auto) THEN RenameVar `b' (-2)) ORELSE RepeatFor 2 (Intro)))
   THEN RepeatFor 2 (Intro)
   THEN (((RWO "alpha-aux-mkterm" 0 THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto) THEN RepeatFor 4 (ParallelLast))
   ORELSE (Unfold `alpha-aux` 0 THEN Reduce 0 THEN Complete (Auto))
   )) }

1
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]))

2
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]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}a,b:term(opr).  \mforall{}vs,ws:varname()  List.    (alpha-aux(opr;vs;ws;a;b)  \mLeftarrow{}{}\mRightarrow{}  alpha-aux(opr;ws;vs;b;a))


By

---

Latex:
(Intro
  THEN  ((BLemma  `term-induction`  THENW  Auto)
              THEN  Intro
              THEN  (((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  RenameVar  `a'  (-2))
              ORELSE  RepeatFor  2  (Intro)
              ))
  THEN  ((BLemma  `term-induction`  THENW  Auto)
              THEN  Intro
              THEN  (((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  RenameVar  `b'  (-2))
              ORELSE  RepeatFor  2  (Intro)
              ))
  THEN  RepeatFor  2  (Intro)
  THEN  (((RWO  "alpha-aux-mkterm"  0  THENA  Auto)
                THEN  (RepeatFor  2  (D  0)  THENA  Auto)
                THEN  RepeatFor  4  (ParallelLast))
  ORELSE  (Unfold  `alpha-aux`  0  THEN  Reduce  0  THEN  Complete  (Auto))
  ))

---

Home Index