---

Step * 2 of Lemma co-value-height_wf


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(ℕ)
BY
{ (D_b_union (-1) THEN D -1 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  co-value-height  :  T  {}\mrightarrow{}  partial(\mBbbN{})
3.  a1  :  (T  \mtimes{}  T)  \mcup{}  (T  +  T)
\mvdash{}  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  \mmember{}  partial(\mBbbN{})


By

---

Latex:
(D\_b\_union  (-1)  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index