Nuprl Definition : urec-level

urec-level(f;x) ==
  fix((λurec-level,x. let con,L = f x in if null(L) then 1 else imax-list(map(λt.(urec-level t);L)) + 1 fi )) x


Definitions occuring in Statement :  imax-list: imax-list(L),  null: null(as),  map: map(f;as),  ifthenelse: if b then t else f fi ,  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),  spread: spread def,  ifthenelse: if b then t else f fi ,  null: null(as),  add: n + m,  imax-list: imax-list(L),  map: map(f;as),  lambda: λx.A[x],  apply: f a,  natural_number: $n
FDL editor aliases :  urec-level
Latex:
urec-level(f;x)  ==
    fix((\mlambda{}urec-level,x.  let  con,L  =  f  x 
                                            in  if  null(L)  then  1  else  imax-list(map(\mlambda{}t.(urec-level  t);L))  +  1  fi  )) 
    x


Date html generated: 2016_05_15-PM-06_57_45
Last ObjectModification: 2015_09_23-AM-08_08_18

Theory : general


Home Index