---

Step * of Lemma term-size-positive

No Annotations
∀[opr:Type]. ∀t:term(opr). (1 ≤ term-size(t))
BY
{ (InstLemma `term-cases` []
   THEN RepeatFor 2 (ParallelLast')
   THEN D -1
   THEN ExRepD
   THEN (RWO "-1" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

1
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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}t:term(opr).  (1  \mleq{}  term-size(t))


By

---

Latex:
(InstLemma  `term-cases`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  D  -1
  THEN  ExRepD
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index