---

Step * of Lemma alpha-aux-trans

No Annotations
∀[opr:Type]
  ∀a,b,c:term(opr). ∀us,vs,ws:varname() List.
    (alpha-aux(opr;us;vs;a;b) ⇒ alpha-aux(opr;vs;ws;b;c) ⇒ alpha-aux(opr;us;ws;a;c))
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 ((BLemma `term-induction` THENW Auto)
         THEN Intro
         THEN (((Assert varterm(v) ∈ term(opr) BY Auto) THEN RenameVar `c' (-2)) ORELSE RepeatFor 2 (Intro)))
   THEN RepeatFor 3 (Intro)
   THEN RepeatFor 2 ((Intro THEN Try ((Unfold `alpha-aux` -1 THEN Reduce -1 THEN FalseHD (-1)))))) }

1
1. [opr] : Type
2. a : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. varterm(a) ∈ term(opr)
4. b : {v:varname()| ¬(v = nullvar() ∈ varname())} 
5. varterm(b) ∈ term(opr)
6. c : {v:varname()| ¬(v = nullvar() ∈ varname())} 
7. varterm(c) ∈ term(opr)
8. us : varname() List
9. vs : varname() List
10. ws : varname() List
11. alpha-aux(opr;us;vs;varterm(a);varterm(b))
12. alpha-aux(opr;vs;ws;varterm(b);varterm(c))
⊢ alpha-aux(opr;us;ws;varterm(a);varterm(c))

2
1. [opr] : Type
2. bts : bound-term(opr) List
3. ∀bt:bound-term(opr)
     ((bt ∈ bts)
     ⇒ (∀b,c:term(opr). ∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;snd(bt);b) ⇒ alpha-aux(opr;vs;ws;b;c) ⇒ alpha-aux(opr;us;ws;snd(bt);c))))
4. f : opr
5. b1 : bound-term(opr) List
6. ∀bt:bound-term(opr)
     ((bt ∈ b1)
     ⇒ (∀c:term(opr). ∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;mkterm(f;bts);snd(bt))
           ⇒ alpha-aux(opr;vs;ws;snd(bt);c)
           ⇒ alpha-aux(opr;us;ws;mkterm(f;bts);c))))
7. f1 : opr
8. b2 : bound-term(opr) List
9. ∀bt:bound-term(opr)
     ((bt ∈ b2)
     ⇒ (∀us,vs,ws:varname() List.
           (alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
           ⇒ alpha-aux(opr;vs;ws;mkterm(f1;b1);snd(bt))
           ⇒ alpha-aux(opr;us;ws;mkterm(f;bts);snd(bt)))))
10. f2 : opr
11. us : varname() List
12. vs : varname() List
13. ws : varname() List
14. alpha-aux(opr;us;vs;mkterm(f;bts);mkterm(f1;b1))
15. alpha-aux(opr;vs;ws;mkterm(f1;b1);mkterm(f2;b2))
⊢ alpha-aux(opr;us;ws;mkterm(f;bts);mkterm(f2;b2))

---

Latex:

---

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


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  ((BLemma  `term-induction`  THENW  Auto)
              THEN  Intro
              THEN  (((Assert  varterm(v)  \mmember{}  term(opr)  BY  Auto)  THEN  RenameVar  `c'  (-2))
              ORELSE  RepeatFor  2  (Intro)
              ))
  THEN  RepeatFor  3  (Intro)
  THEN  RepeatFor  2  ((Intro  THEN  Try  ((Unfold  `alpha-aux`  -1  THEN  Reduce  -1  THEN  FalseHD  (-1))))))

---

Home Index