Nuprl Definition : polynom

polynom(n)==r if (n =z 0) then ℤ else {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)}  fi 
polynom(n) ==  fix((λpolynom,n. if (n =z 0) then ℤ else {p:(polynom (n - 1)) List| polyform-lead-nonzero(n;p)}  fi )) n


Definitions occuring in Statement :  polyform-lead-nonzero: polyform-lead-nonzero(n;p),  list: T List,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  set: {x:A| B[x]} ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n,  int: ℤ
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  int: ℤ,  set: {x:A| B[x]} ,  list: T List,  apply: f a,  subtract: n - m,  natural_number: $n,  polyform-lead-nonzero: polyform-lead-nonzero(n;p)
FDL editor aliases :  polynom polynom
Latex:
polynom(n)==r  if  (n  =\msubz{}  0)  then  \mBbbZ{}  else  \{p:polynom(n  -  1)  List|  polyform-lead-nonzero(n;p)\}    fi 

Latex:
polynom(n)  ==
    fix((\mlambda{}polynom,n.  if  (n  =\msubz{}  0)
                                    then  \mBbbZ{}
                                    else  \{p:(polynom  (n  -  1))  List|  polyform-lead-nonzero(n;p)\} 
                                    fi  )) 
    n


Date html generated: 2017_09_29-PM-05_59_47
Last ObjectModification: 2017_04_26-PM-02_04_27

Theory : integer!polynomials


Home Index