Nuprl Definition : MMTree-rank

MMTree-rank(t) ==
  fix((λMMTree-rank,t. if MMTree_Leaf?(t)
                      then 0
                      else imax-list([0 / map(λl.imax-list([0 / map(λs.(MMTree-rank s);l)]);MMTree_Node-forest(t))])
                      fi )) 
  t


Definitions occuring in Statement :  MMTree_Node-forest: MMTree_Node-forest(v),  MMTree_Leaf?: MMTree_Leaf?(v),  imax-list: imax-list(L),  map: map(f;as),  cons: [a / b],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  natural_number: $n
FDL editor aliases :  MMTree-rank
MMTree-rank(t)  ==
    fix((\mlambda{}MMTree-rank,t.  if  MMTree\_Leaf?(t)
                                            then  0
                                            else  imax-list([0  / 
                                                                            map(\mlambda{}l.imax-list([0  /  map(\mlambda{}s.(MMTree-rank  s);l)]);
                                                                                    MMTree\_Node-forest(t))])
                                            fi  )) 
    t


Date html generated: 2015_07_17-AM-07_47_20
Last ObjectModification: 2013_02_14-PM-05_32_04

Home Index