Nuprl Definition : l-exists-decider

l-exists-decider() ==
  λL,dcd. eval j' ||L|| in
          letrec G(x)=if (x) < (j')
                         then case dcd L[x] of inl(z) => inl <x, z> inr(z) => (x 1)
                         else (inr x.Ax) in

Definitions occuring in Statement :  select: L[n] length: ||as|| genrec-ap: genrec-ap callbyvalue: callbyvalue less: if (a) < (b)  then c  else d apply: a lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n axiom: Ax
Definitions occuring in definition :  callbyvalue: callbyvalue length: ||as|| genrec-ap: genrec-ap less: if (a) < (b)  then c  else d decide: case of inl(x) => s[x] inr(y) => t[y] select: L[n] inl: inl x pair: <a, b> apply: a add: m inr: inr  lambda: λx.A[x] axiom: Ax natural_number: $n
FDL editor aliases :  l-exists-decider

l-exists-decider()  ==
    \mlambda{}L,dcd.  eval  j'  =  ||L||  in
                    letrec  G(x)=if  (x)  <  (j')
                                                  then  case  dcd  L[x]  of  inl(z)  =>  inl  <x,  z>  |  inr(z)  =>  G  (x  +  1)
                                                  else  (inr  (\mlambda{}x.Ax)  )  in

Date html generated: 2016_05_14-AM-07_47_55
Last ObjectModification: 2015_09_22-PM-05_54_00

Theory : list_1

Home Index