Nuprl Definition : l-all-decider

l-all-decider() ==
  λL,dcd. eval j' ||L|| in
          case letrec G(x)=if (x) < (j')  then if dcd L[x] then (x 1) else inl <x, λ%.Ax> fi   else (inr x.Ax) i\000Cn
           of inl(%6) =>
           inr let k,%8 %6 
               in λ%8.Ax 
           inr(%7) =>
           inl dcd L[k] of inl(%10) => %10 inr(%11) => Ax)

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

l-all-decider()  ==
    \mlambda{}L,dcd.  eval  j'  =  ||L||  in
                    case  letrec  G(x)=if  (x)  <  (j')
                                                            then  if  dcd  L[x]  then  G  (x  +  1)  else  inl  <x,  \mlambda{}\%.Ax>  fi 
                                                            else  (inr  (\mlambda{}x.Ax)  )  in
                      of  inl(\%6)  =>
                      inr  let  k,\%8  =  \%6 
                              in  \mlambda{}\%8.Ax 
                      |  inr(\%7)  =>
                      inl  (\mlambda{}  dcd  L[k]  of  inl(\%10)  =>  \%10  |  inr(\%11)  =>  Ax)

Date html generated: 2016_05_14-AM-07_47_36
Last ObjectModification: 2015_11_13-AM-00_35_30

Theory : list_1

Home Index