Nuprl Definition : fps-set-to-one

[f]_n(y:=1) ==  λb.if 0 <z (#y in b) ∨bn <z #(b) then 0 else f[b + bag-rep(n - #(b);y)] fi 


Definitions occuring in Statement :  fps-coeff: f[b],  bag-count: (#x in bs),  bag-rep: bag-rep(n;x),  bag-size: #(bs),  bag-append: as + bs,  atom-deq: AtomDeq,  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  lambda: λx.A[x],  subtract: n - m,  natural_number: $n,  rng_zero: 0
Definitions occuring in definition :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  bor: p ∨bq,  natural_number: $n,  bag-count: (#x in bs),  atom-deq: AtomDeq,  lt_int: i <z j,  rng_zero: 0,  fps-coeff: f[b],  bag-append: as + bs,  bag-rep: bag-rep(n;x),  subtract: n - m,  bag-size: #(bs)
FDL editor aliases :  fps-set-to-one
Latex:
[f]\_n(y:=1)  ==    \mlambda{}b.if  0  <z  (\#y  in  b)  \mvee{}\msubb{}n  <z  \#(b)  then  0  else  f[b  +  bag-rep(n  -  \#(b);y)]  fi 


Date html generated: 2016_05_15-PM-09_59_35
Last ObjectModification: 2015_09_23-AM-08_21_37

Theory : power!series


Home Index