---

Step * of Lemma term_size_mkterm_lemma

No Annotations
∀bts,opr:Top.  (term-size(mkterm(opr;bts)) ~ 1 + Σ(term-size(snd(bt)) | bt ∈ bts))
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (UnfoldC `term-size`)) 0
   THEN RepUR ``coterm-size mkterm`` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Fold `coterm-size` 0
   THEN Fold `term-size` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}bts,opr:Top.    (term-size(mkterm(opr;bts))  \msim{}  1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  bts))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (UnfoldC  `term-size`))  0
  THEN  RepUR  ``coterm-size  mkterm``  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Fold  `coterm-size`  0
  THEN  Fold  `term-size`  0
  THEN  Auto)

---

Home Index