Nuprl Definition : MMTreeco_size

MMTreeco_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "Leaf" then 0
                   if lbl =a "Node" then 1 + Σ(Σ(size x[i][i1] | i1 < ||x[i]||) | i < ||x||)
                   else 0
                   fi )) 
  p


Definitions occuring in Statement :  sum: Σ(f[x] | x < k),  select: L[n],  length: ||as||,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  add: n + m,  natural_number: $n,  token: "$token"
FDL editor aliases :  MMTreeco_size
Latex:
MMTreeco\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "Leaf"  then  0
                                      if  lbl  =a  "Node"  then  1  +  \mSigma{}(\mSigma{}(size  x[i][i1]  |  i1  <  ||x[i]||)  |  i  <  ||x||)
                                      else  0
                                      fi  )) 
    p


Date html generated: 2016_05_16-AM-08_54_23
Last ObjectModification: 2014_05_06-PM-02_41_05

Theory : C-semantics


Home Index