Nuprl Definition : minus-polynom

minus-polynom(n;p)==r if n=0  then -p  else map(λq.minus-polynom(n - 1;q);p)

minus-polynom(n;p) ==  fix((λminus-polynom,n,p. if n=0  then -p  else map(λq.(minus-polynom (n - 1) q);p))) n p



Definitions occuring in Statement :  map: map(f;as),  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  minus: -n,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  subtract: n - m,  apply: f a,  lambda: λx.A[x],  map: map(f;as),  minus: -n,  int_eq: if a=b  then c  else d,  fix: fix(F)
FDL editor aliases :  minus-polynom
Latex:
minus-polynom(n;p)==r  if  n=0    then  -p    else  map(\mlambda{}q.minus-polynom(n  -  1;q);p)


Latex:
minus-polynom(n;p)  ==
    fix((\mlambda{}minus-polynom,n,p.  if  n=0    then  -p    else  map(\mlambda{}q.(minus-polynom  (n  -  1)  q);p)))  n  p



Date html generated: 2017_04_20-AM-07_11_06
Last ObjectModification: 2017_04_19-AM-10_21_08

Theory : list_1


Home Index