---

Step * 1 2 of Lemma co-value-height_wf


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(ℕ)
BY
{ TACTIC:CanonicalAuto }

1
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)
7. x : a1 ~ inl outl(a1)
⊢ 1 + (co-value-height outl(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)
7. ∀[u,v:Top].  (if a1 is inl then u else v ~ v)
⊢ 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  :  Base
4.  (a1)\mdownarrow{}
5.  \muparrow{}is-atomic(a1)
6.  \mforall{}[u,v:Top].    (if  a1  is  a  pair  then  u  otherwise  v  \msim{}  v)
\mvdash{}  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:
TACTIC:CanonicalAuto

---

Home Index