---

Step * of Lemma sq_stable__alpha-aux

No Annotations
∀[opr:Type]. ∀a,b:term(opr). ∀vs,ws:varname() List.  SqStable(alpha-aux(opr;vs;ws;a;b))
BY
{ (Intro
   THEN (BLemma `term-induction` THENW Auto)
   THEN Intro
   THEN ((BLemma `term-induction` THENW Auto) ORELSE (RepeatFor 2 (Intro) THEN (BLemma `term-induction` THENW Auto)))
   THEN Intros
   THEN Try ((Unfold `alpha-aux` 0 THEN Reduce 0 THEN Complete (Auto)))
   THEN Thin (-4)
   THEN RepeatFor 6 (MoveToConcl (-1))
   THEN (ListInd (-1)
         THENL [(Auto THEN Unfold `alpha-aux` 0 THEN Reduce 0 THEN DVar `b1' THEN Reduce 0 THEN Auto)
               ; ((ParallelLast THENA (RepeatFor 2 (ParallelLast) THEN Auto))
                  THEN (Intro THEN InductionOnList)
                  THEN Unfold `alpha-aux` 0
                  THEN Reduce 0
                  THEN Auto)]
   )) }

1
1. [opr] : Type
2. u : bound-term(opr)
3. v : bound-term(opr) List
4. ∀bt:bound-term(opr)
     ((bt ∈ [u / v]) ⇒ (∀b:term(opr). ∀vs,ws:varname() List.  SqStable(alpha-aux(opr;vs;ws;snd(bt);b))))
5. ∀f:opr. ∀b1:bound-term(opr) List. ∀f1:opr. ∀vs,ws:varname() List.
     SqStable(alpha-aux(opr;vs;ws;mkterm(f;v);mkterm(f1;b1)))
6. f : opr
7. u1 : bound-term(opr)
8. v1 : bound-term(opr) List
9. ∀f1:opr. ∀vs,ws:varname() List.  SqStable(alpha-aux(opr;vs;ws;mkterm(f;[u / v]);mkterm(f1;v1)))
10. f1 : opr
11. vs : varname() List
12. ws : varname() List
⊢ SqStable(let as,x = u 
           in let bs,y = u1 
              in (||as|| = ||bs|| ∈ ℤ) ∧ alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y))

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  (BLemma  `term-induction`  THENW  Auto)
  THEN  Intro
  THEN  ((BLemma  `term-induction`  THENW  Auto)
  ORELSE  (RepeatFor  2  (Intro)  THEN  (BLemma  `term-induction`  THENW  Auto))
  )
  THEN  Intros
  THEN  Try  ((Unfold  `alpha-aux`  0  THEN  Reduce  0  THEN  Complete  (Auto)))
  THEN  Thin  (-4)
  THEN  RepeatFor  6  (MoveToConcl  (-1))
  THEN  (ListInd  (-1)
              THENL  [(Auto  THEN  Unfold  `alpha-aux`  0  THEN  Reduce  0  THEN  DVar  `b1'  THEN  Reduce  0  THEN  Auto)
                          ;  ((ParallelLast  THENA  (RepeatFor  2  (ParallelLast)  THEN  Auto))
                                THEN  (Intro  THEN  InductionOnList)
                                THEN  Unfold  `alpha-aux`  0
                                THEN  Reduce  0
                                THEN  Auto)]
  ))

---

Home Index