---

Step * 1 of Lemma alpha-aux_wf


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)
BY
{ ((Assert term-size(snd(<u2, u3>)) ≤ Σ(term-size(snd(bt)) | bt ∈ [<u2, u3> / v]) BY
          ((InstLemma `summand-le-lsum` [⌜bound-term(opr)⌝;⌜[<u2, u3> / v]⌝;⌜λ2bt.term-size(snd(bt))⌝]⋅ THENA Auto)
           THEN BHyp -1
           THEN Auto))
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  n  :  \mBbbN{}
3.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
4.  y1  :  opr
5.  u2  :  varname()  List
6.  u3  :  term(opr)
7.  v  :  (varname()  List  \mtimes{}  term(opr))  List
8.  inr  <y1,  [<u2,  u3>  /  v]>    \mmember{}  term(opr)
9.  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [<u2,  u3>  /  v]))  \mleq{}  n
10.  y3  :  opr
11.  u4  :  varname()  List
12.  u5  :  term(opr)
13.  v1  :  (varname()  List  \mtimes{}  term(opr))  List
14.  inr  <y3,  [<u4,  u5>  /  v1]>    \mmember{}  term(opr)
15.  vs  :  varname()  List
16.  ws  :  varname()  List
17.  0  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [<u2,  u3>  /  v])
18.  \mforall{}[a:term(opr)]
            ((term-size(a)  \mleq{}  (n  -  1))
            {}\mRightarrow{}  (\mforall{}[b:term(opr)].  \mforall{}[vs,ws:varname()  List].    (alpha-aux(opr;vs;ws;a;b)  \mmember{}  \mBbbP{})))
\mvdash{}  term-size(u3)  \mleq{}  (n  -  1)


By

---

Latex:
((Assert  term-size(snd(<u2,  u3>))  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  [<u2,  u3>  /  v])  BY
                ((InstLemma  `summand-le-lsum`  [\mkleeneopen{}bound-term(opr)\mkleeneclose{};\mkleeneopen{}[<u2,  u3>  /  v]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.term-size(snd(bt))\mkleeneclose{}]
                    \mcdot{}
                    THENA  Auto
                    )
                  THEN  BHyp  -1
                  THEN  Auto))
  THEN  All  Reduce
  THEN  Auto)

---

Home Index