---

Step * of Lemma alpha-aux_wf

No Annotations
∀[opr:Type]. ∀[a,b:term(opr)]. ∀[vs,ws:varname() List].  (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)
BY
{ (RepeatFor 2 (Intro)
   THEN (Enough to prove ∀n:ℕ
                           ∀[a:term(opr)]
                             ((term-size(a) ≤ n)
                             ⇒ (∀[b:term(opr)]. ∀[vs,ws:varname() List].  (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)))
          Because ((D 0 THENA Auto) THEN (D -2 With ⌜term-size(a)⌝  THENA Auto) THEN InstHyp [⌜a⌝] (-1)⋅ THEN Auto))
   THEN Thin (-1)
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN (Assert t ∈ term(opr) BY
               Auto)
   THEN RepeatFor 2 (D -2)
   THEN Folds  ``varterm mkterm`` 0
   THEN Reduce 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (GenConcl ⌜b = s ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `b'
   THEN (Assert s ∈ term(opr) BY
               Auto)
   THEN RepeatFor 2 (D -2)
   THEN Folds  ``varterm mkterm`` 0
   THEN Reduce 0
   THEN (Unfold `alpha-aux` 0 THEN Reduce 0)
   THEN Auto
   THEN (Assert 0 ≤ Σ(term-size(snd(bt)) | bt ∈ y2) BY
               (Unfold `lsum` 0 THEN BLemma `l_sum_nonneg` THEN Auto THEN D 0 THEN Auto))
   THEN (D 3 With ⌜n - 1⌝  THENA Auto)
   THEN (D -10 THEN D -6 THEN Reduce 0)
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

1
1. opr : Type
2. n : ℕ
3. term(opr) ≡ coterm-fun(opr;term(opr))
4. y1 : opr
5. u2 : varname() List
6. u3 : term(opr)
7. v : (varname() List × term(opr)) List
8. inr <y1, [<u2, u3> / v]>  ∈ term(opr)
9. (1 + Σ(term-size(snd(bt)) | bt ∈ [<u2, u3> / v])) ≤ n
10. y3 : opr
11. u4 : varname() List
12. u5 : term(opr)
13. v1 : (varname() List × term(opr)) List
14. inr <y3, [<u4, u5> / v1]>  ∈ term(opr)
15. vs : varname() List
16. ws : varname() List
17. 0 ≤ Σ(term-size(snd(bt)) | bt ∈ [<u2, u3> / v])
18. ∀[a:term(opr)]
      ((term-size(a) ≤ (n - 1)) ⇒ (∀[b:term(opr)]. ∀[vs,ws:varname() List].  (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)))
⊢ term-size(u3) ≤ (n - 1)

2
1. opr : Type
2. n : ℕ
3. term(opr) ≡ coterm-fun(opr;term(opr))
4. y1 : opr
5. u : varname() List × term(opr)
6. v : (varname() List × term(opr)) List
7. inr <y1, [u / v]>  ∈ term(opr)
8. (1 + Σ(term-size(snd(bt)) | bt ∈ [u / v])) ≤ n
9. y3 : opr
10. u1 : varname() List × term(opr)
11. v1 : (varname() List × term(opr)) List
12. inr <y3, [u1 / v1]>  ∈ term(opr)
13. vs : varname() List
14. ws : varname() List
15. 0 ≤ Σ(term-size(snd(bt)) | bt ∈ [u / v])
16. ∀[a:term(opr)]
      ((term-size(a) ≤ (n - 1)) ⇒ (∀[b:term(opr)]. ∀[vs,ws:varname() List].  (alpha-aux(opr;vs;ws;a;b) ∈ ℙ)))
17. let as,x = u 
    in let bs,y = u1 
       in alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y)
⊢ term-size(mkterm(y1;v)) ≤ (n - 1)

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Enough  to  prove  \mforall{}n:\mBbbN{}
                                                  \mforall{}[a:term(opr)]
                                                      ((term-size(a)  \mleq{}  n)
                                                      {}\mRightarrow{}  (\mforall{}[b:term(opr)].  \mforall{}[vs,ws:varname()  List].
                                                                  (alpha-aux(opr;vs;ws;a;b)  \mmember{}  \mBbbP{})))
                Because  ((D  0  THENA  Auto)
                                  THEN  (D  -2  With  \mkleeneopen{}term-size(a)\mkleeneclose{}    THENA  Auto)
                                  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}
                                  THEN  Auto))
  THEN  Thin  (-1)
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  (Assert  t  \mmember{}  term(opr)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Folds    ``varterm  mkterm``  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}b  =  s\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  (Assert  s  \mmember{}  term(opr)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Folds    ``varterm  mkterm``  0
  THEN  Reduce  0
  THEN  (Unfold  `alpha-aux`  0  THEN  Reduce  0)
  THEN  Auto
  THEN  (Assert  0  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2)  BY
                          (Unfold  `lsum`  0  THEN  BLemma  `l\_sum\_nonneg`  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  (D  3  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  (D  -10  THEN  D  -6  THEN  Reduce  0)
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index