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 :  polyform-lead-nonzero: polyform-lead-nonzero(n;p),  natural_number: $n,  subtract: n - m,  apply: f a,  list: T List,  set: {x:A| B[x]} ,  int: ℤ,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  polynom polynom polynom polynom polynom polynom 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_04_17-AM-09_03_05
Last ObjectModification: 2017_04_13-PM-01_04_34

Theory : list_1


Home Index