Nuprl Definition : minus-polynom
minus-polynom(n;p)==r if n=0  then -p  else map-rev(λq.minus-polynom(n - 1;q);p)
minus-polynom(n;p) ==  fix((λminus-polynom,n,p. if n=0  then -p  else map-rev(λq.(minus-polynom (n - 1) q);p))) n p
Definitions occuring in Statement : 
map-rev: map-rev(f;L)
, 
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 : 
fix: fix(F)
, 
int_eq: if a=b  then c  else d
, 
minus: -n
, 
map-rev: map-rev(f;L)
, 
lambda: λx.A[x]
, 
apply: f a
, 
subtract: n - m
, 
natural_number: $n
FDL editor aliases : 
minus-polynom
Latex:
minus-polynom(n;p)==r  if  n=0    then  -p    else  map-rev(\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-rev(\mlambda{}q.(minus-polynom  (n  -  1)  q);p)))  n  p
Date html generated:
2017_09_29-PM-06_00_28
Last ObjectModification:
2017_04_27-PM-04_59_56
Theory : integer!polynomials
Home
Index