---

Step * 1 of Lemma co-value-height_wf


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(ℕ)
BY
{ ((D -1 THEN D -2) THEN CanonicalAuto) }

1
1. T : Type
2. co-value-height : T ⟶ partial(ℕ)
3. a1 : Base
4. (a1)↓
5. ↑is-atomic(a1)
6. x : a1 ~ <fst(a1), snd(a1)>
⊢ 1 + (co-value-height (fst(a1))) + (co-value-height (snd(a1))) ∈ partial(ℕ)

2
1. T : Type
2. co-value-height : T ⟶ partial(ℕ)
3. a1 : Base
4. (a1)↓
5. ↑is-atomic(a1)
6. ∀[u,v:Top].  (if a1 is a pair then u otherwise v ~ v)
⊢ 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:

1.  T  :  Type
2.  co-value-height  :  T  {}\mrightarrow{}  partial(\mBbbN{})
3.  a1  :  atomic-values()
\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  -1  THEN  D  -2)  THEN  CanonicalAuto)

---

Home Index