Nuprl Definition : poly-int-val

p@l==r if null(l) then p else let a,as = l in Σ(p[i]@as * a^||p|| - 1 - i | i < ||p||) fi 

p@l ==
  fix((λpoly-int-val,l,p. if null(l)
                         then p
                         else let a,as = l 
                              in Σ((poly-int-val as p[i]) * a^||p|| - 1 - i | i < ||p||)
                         fi )) 
  l 
  p



Definitions occuring in Statement :  exp: i^n,  sum: Σ(f[x] | x < k),  select: L[n],  length: ||as||,  null: null(as),  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  multiply: n * m,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  length: ||as||,  subtract: n - m,  exp: i^n,  select: L[n],  apply: f a,  multiply: n * m,  sum: Σ(f[x] | x < k),  spread: spread def,  null: null(as),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  poly-int-val poly-int-val
Latex:
p@l==r  if  null(l)  then  p  else  let  a,as  =  l  in  \mSigma{}(p[i]@as  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||)  fi 


Latex:
p@l  ==
    fix((\mlambda{}poly-int-val,l,p.  if  null(l)
                                                  then  p
                                                  else  let  a,as  =  l 
                                                            in  \mSigma{}((poly-int-val  as  p[i])  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||)
                                                  fi  )) 
    l 
    p



Date html generated: 2017_04_17-AM-09_04_15
Last ObjectModification: 2017_04_12-PM-03_59_09

Theory : list_1


Home Index