Nuprl Definition : bar-val

bar-val(n;x) ==  fix((λbar-val,n,x. case x of inl(b) => x | inr(z) => if (n =z 0) then inr ⋅  else bar-val (n - 1) z fi \000C)) n x


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  it: ⋅,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  inr: inr x ,  it: ⋅,  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  bar-val
Latex:
bar-val(n;x)  ==
    fix((\mlambda{}bar-val,n,x.  case  x
                                          of  inl(b)  =>
                                          x
                                          |  inr(z)  =>
                                          if  (n  =\msubz{}  0)  then  inr  \mcdot{}    else  bar-val  (n  -  1)  z  fi  )) 
    n 
    x


Date html generated: 2016_05_14-AM-06_19_42
Last ObjectModification: 2015_09_22-PM-05_47_32

Theory : co-recursion


Home Index