---

Step * 2 2 1 2 of Lemma rec-value-ext


1. a1 : Base@i
2. [%2] : (a1)↓@i
3. ↑is-atomic(a1)@i
4. ∀[u,v:Top].  (if a1 is a pair then u otherwise v ~ v)
⊢ (if a1 is inl then 1 + rec-value-height(outl(a1))
   else if a1 is inr then 1 + rec-value-height(outr(a1))
        else 0)↓
BY
{ (Thin (-1) THEN CanonicalAuto) }

1
1. a1 : Base@i
2. [%2] : (a1)↓@i
3. ↑is-atomic(a1)@i
4. x : a1 ~ inl outl(a1)
⊢ (1 + rec-value-height(outl(a1)))↓

2
1. a1 : Base@i
2. [%2] : (a1)↓@i
3. ↑is-atomic(a1)@i
4. ∀[u,v:Top].  (if a1 is inl then u else v ~ v)
⊢ (if a1 is inr then 1 + rec-value-height(outr(a1))
   else 0)↓

---

Latex:

---

Latex:

1.  a1  :  Base@i
2.  [\%2]  :  (a1)\mdownarrow{}@i
3.  \muparrow{}is-atomic(a1)@i
4.  \mforall{}[u,v:Top].    (if  a1  is  a  pair  then  u  otherwise  v  \msim{}  v)
\mvdash{}  (if  a1  is  inl  then  1  +  rec-value-height(outl(a1))
      else  if  a1  is  inr  then  1  +  rec-value-height(outr(a1))
                else  0)\mdownarrow{}


By

---

Latex:
(Thin  (-1)  THEN  CanonicalAuto)

---

Home Index