---

Step * 1 of Lemma coterm-size_wf


1. opr : Type
2. t : coterm(opr)
⊢ coterm-size(t) ∈ partial(ℕ)
BY
{ (InstLemma `fix_wf_corec-partial1` [⌜ℕ⌝;⌜λ2T.coterm-fun(opr;T)⌝;⌜λf,t. case t
                                                                         of inl(v) =>
                                                                         1
                                                                         | inr(p) =>
                                                                         let opr,bts = p 
                                                                         in 1 + l_sum(map(λbt.(f (snd(bt)));bts))⌝]⋅
   THENA Auto
   ) }

1
1. opr : Type
2. t : coterm(opr)
3. T : Type
4. f : T ⟶ partial(ℕ)
5. y1 : opr
6. y2 : (varname() List × T) List
⊢ 1 + l_sum(map(λbt.(f (snd(bt)));y2)) ∈ partial(ℕ)

2
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(ℕ)

---

Latex:

---

Latex:

1.  opr  :  Type
2.  t  :  coterm(opr)
\mvdash{}  coterm-size(t)  \mmember{}  partial(\mBbbN{})


By

---

Latex:
(InstLemma  `fix\_wf\_corec-partial1`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.coterm-fun(opr;T)\mkleeneclose{};
  \mkleeneopen{}\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))\mkleeneclose{}]\000C\mcdot{}
  THENA  Auto
  )

---

Home Index