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 G (x + 1) else inl <x, λ%.Ax> fi   else (inr (λx.Ax) ) i\000Cn
                G(0)
           of inl(%6) =>
           inr let k,%8 = %6 
               in λ%8.Ax 
           | inr(%7) =>
           inl (λk.case 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 b then t else f fi ,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + 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 b then t else f fi ,  add: n + m,  pair: <a, b>,  natural_number: $n,  inr: inr x ,  spread: spread def,  inl: inl x,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  select: L[n],  axiom: Ax
FDL editor aliases :  l-all-decider
Latex:
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
                                G(0)
                      of  inl(\%6)  =>
                      inr  let  k,\%8  =  \%6 
                              in  \mlambda{}\%8.Ax 
                      |  inr(\%7)  =>
                      inl  (\mlambda{}k.case  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