Nuprl Definition : gensearch

gensearch(f;g;x) ==
  fix((λgensearch,x. case f x of inl(a) => inl a | inr(b) => case g x of inl(y) => gensearch y | inr(z) => inr z )) x


Definitions occuring in Statement :  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 ,  inl: inl x
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  inl: inl x,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  inr: inr x 
FDL editor aliases :  gensearch
Latex:
gensearch(f;g;x)  ==
    fix((\mlambda{}gensearch,x.  case  f  x
                                          of  inl(a)  =>
                                          inl  a
                                          |  inr(b)  =>
                                          case  g  x  of  inl(y)  =>  gensearch  y  |  inr(z)  =>  inr  z  )) 
    x


Date html generated: 2016_05_15-PM-03_24_23
Last ObjectModification: 2015_09_23-AM-07_43_06

Theory : general


Home Index