Nuprl Definition : bs_treeco_size

bs_treeco_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "null" then 0
                   if lbl =a "leaf" then 0
                   if lbl =a "node" then 1 + (size (fst(x))) + (size (snd(snd(x))))
                   else 0
                   fi )) 
  p


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  pi1: fst(t),  pi2: snd(t),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  add: n + m,  natural_number: $n,  token: "$token"
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  token: "$token",  add: n + m,  pi1: fst(t),  apply: f a,  pi2: snd(t),  natural_number: $n
FDL editor aliases :  bs_treeco_size
Latex:
bs\_treeco\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "null"  then  0
                                      if  lbl  =a  "leaf"  then  0
                                      if  lbl  =a  "node"  then  1  +  (size  (fst(x)))  +  (size  (snd(snd(x))))
                                      else  0
                                      fi  )) 
    p


Date html generated: 2016_05_15-PM-01_50_07
Last ObjectModification: 2016_04_07-PM-02_24_26

Theory : tree_1


Home Index