---

Step * of Lemma co-value-height_wf

∀[t:co-value()]. (co-value-height(t) ∈ partial(ℕ))
BY
{ ProveCoSizeWf }

1
1. T : Type
2. co-value-height : T ⟶ partial(ℕ)
3. a1 : atomic-values()
⊢ if a1 is a pair then let a,b = a1 
                       in 1 + (co-value-height a) + (co-value-height b) otherwise if a1 is inl then 1
                                                                                  + (co-value-height outl(a1))
                                                                                  else if a1 is inr then 1
                                                                                       + (co-value-height outr(a1))
                                                                                       else 0 ∈ partial(ℕ)

2
1. T : Type
2. co-value-height : T ⟶ partial(ℕ)
3. a1 : (T × T) ⋃ (T + T)
⊢ if a1 is a pair then let a,b = a1 
                       in 1 + (co-value-height a) + (co-value-height b) otherwise if a1 is inl then 1
                                                                                  + (co-value-height outl(a1))
                                                                                  else if a1 is inr then 1
                                                                                       + (co-value-height outr(a1))
                                                                                       else 0 ∈ partial(ℕ)

---

Latex:

---

Latex:
\mforall{}[t:co-value()].  (co-value-height(t)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
ProveCoSizeWf

---

Home Index