---

Step * 1 of Lemma term-size-positive


1. [opr] : Type
2. t : term(opr)
3. f : opr
4. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t)}  List
5. t = mkterm(f;bts) ∈ term(opr)
⊢ 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ bts))
BY
{ ((Assert 0 ≤ Σ(term-size(snd(bt)) | bt ∈ bts) BY
          (Unfold `lsum` 0 THEN BLemma `l_sum_nonneg` THEN Auto THEN D 0 THEN Auto))
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  t  :  term(opr)
3.  f  :  opr
4.  bts  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t)\}    List
5.  t  =  mkterm(f;bts)
\mvdash{}  1  \mleq{}  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  bts))


By

---

Latex:
((Assert  0  \mleq{}  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  bts)  BY
                (Unfold  `lsum`  0  THEN  BLemma  `l\_sum\_nonneg`  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  Auto
  )

---

Home Index