---

Step * 2 2 2 of Lemma term-ext


1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y : opr × ((varname() List × term(opr)) List)
⊢ (coterm-size(inr y ))↓
BY
{ ((D -1 THEN Unfold `coterm-size` 0 THEN RW (SweepUpC UnrollRecursionC) 0) THEN Reduce 0 THEN Fold `coterm-size` 0) }

1
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
4. y2 : (varname() List × term(opr)) List
⊢ (1 + Σ(coterm-size(snd(bt)) | bt ∈ y2))↓

---

Latex:

---

Latex:

1.  opr  :  Type
2.  coterm(opr)  \mequiv{}  coterm-fun(opr;coterm(opr))
3.  y  :  opr  \mtimes{}  ((varname()  List  \mtimes{}  term(opr))  List)
\mvdash{}  (coterm-size(inr  y  ))\mdownarrow{}


By

---

Latex:
((D  -1  THEN  Unfold  `coterm-size`  0  THEN  RW  (SweepUpC  UnrollRecursionC)  0)
  THEN  Reduce  0
  THEN  Fold  `coterm-size`  0)

---

Home Index