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


1. a1 Value()@i
2. ↑is-atomic(a1)@i
⊢ (if a1 is pair then let a,b a1 
                        in rec-value-height(a) rec-value-height(b) otherwise 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
(D THEN CanonicalAuto) }

1
1. a1 Base@i
2. [%2] (a1)↓@i
3. ↑is-atomic(a1)@i
4. a1 ~ <fst(a1), snd(a1)>
⊢ (1 rec-value-height(fst(a1)) rec-value-height(snd(a1)))↓

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


Latex:


Latex:

1.  a1  :  Value()@i
2.  \muparrow{}is-atomic(a1)@i
\mvdash{}  (if  a1  is  a  pair  then  let  a,b  =  a1 
                                                in  1  +  rec-value-height(a)  +  rec-value-height(b)
      otherwise  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:
(D  1  THEN  CanonicalAuto)




Home Index