---

Step * 1 2 of Lemma coterm-size_wf


1. opr : Type
2. t : coterm(opr)
3. fix((λf,t. case t of inl(v) => 1 | inr(p) => let opr,bts = p in 1 + l_sum(map(λbt.(f (snd(bt)));bts))))
   ∈ corec(T.coterm-fun(opr;T)) ⟶ partial(ℕ)
⊢ coterm-size(t) ∈ partial(ℕ)
BY
{ (Fold `coterm` (-1) THEN Unfold `coterm-size` 0 THEN Unfold `lsum` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  coterm(opr)
3.  fix((\mlambda{}f,t.  case  t
                            of  inl(v)  =>
                            1
                            |  inr(p)  =>
                            let  opr,bts  =  p 
                            in  1  +  l\_sum(map(\mlambda{}bt.(f  (snd(bt)));bts))))  \mmember{}  corec(T.coterm-fun(opr;T))  {}\mrightarrow{}  partial(\mBbbN{})
\mvdash{}  coterm-size(t)  \mmember{}  partial(\mBbbN{})


By

---

Latex:
(Fold  `coterm`  (-1)  THEN  Unfold  `coterm-size`  0  THEN  Unfold  `lsum`  0  THEN  Auto)

---

Home Index