Nuprl Definition : co-value-height

co-value-height(t)
==r if t is a pair then let a,b = t 
                        in 1 + co-value-height(a) + co-value-height(b) otherwise if t is inl then 1
                                                                                 + co-value-height(outl(t))
                                                                                 else if t is inr then 1
                                                                                      + co-value-height(outr(t))
                                                                                      else 0
co-value-height(t) ==
  fix((λco-value-height,t. if t is a pair then let a,b = t 
                                               in 1 + (co-value-height a) + (co-value-height b)
                           otherwise if t is inl then 1 + (co-value-height outl(t))
                                     else if t is inr then 1 + (co-value-height outr(t))
                                          else 0)) 
  t


Definitions occuring in Statement :  outr: outr(x),  outl: outl(x),  ispair: if z is a pair then a otherwise b,  isinr: isinr def,  isinl: isinl def,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ispair: if z is a pair then a otherwise b,  spread: spread def,  isinl: isinl def,  outl: outl(x),  isinr: isinr def,  add: n + m,  apply: f a,  outr: outr(x),  natural_number: $n
FDL editor aliases :  co-value-height
Latex:
co-value-height(t)
==r  if  t  is  a  pair  then  let  a,b  =  t 
                                                in  1  +  co-value-height(a)  +  co-value-height(b)
        otherwise  if  t  is  inl  then  1  +  co-value-height(outl(t))
                            else  if  t  is  inr  then  1  +  co-value-height(outr(t))
                                      else  0
Latex:
co-value-height(t)  ==
    fix((\mlambda{}co-value-height,t.  if  t  is  a  pair  then  let  a,b  =  t 
                                                                                              in  1  +  (co-value-height  a)  +  (co-value-height  b)
                                                      otherwise  if  t  is  inl  then  1  +  (co-value-height  outl(t))
                                                                          else  if  t  is  inr  then  1  +  (co-value-height  outr(t))
                                                                                    else  0)) 
    t


Date html generated: 2016_05_14-PM-03_20_45
Last ObjectModification: 2015_09_22-PM-05_59_27

Theory : rec_values


Home Index