Nuprl Definition : polyvar

polyvar(n;v)
==r if (v) < (0)
       then []
       else eval m = n - 1 in
            if (m) < (v)
               then []
               else if v=0
                       then eval one = polyconst(m;1) in
                            eval zero = polyconst(m;0) in
                              [one; zero]
                       else eval v' = v - 1 in
                            eval a = polyvar(m;v') in
                              [a]
polyvar(n;v) ==
  fix((λpolyvar,n,v. if (v) < (0)
                        then []
                        else eval m = n - 1 in
                             if (m) < (v)
                                then []
                                else if v=0
                                        then eval one = polyconst(m;1) in
                                             eval zero = polyconst(m;0) in
                                               [one; zero]
                                        else eval v' = v - 1 in
                                             eval a = polyvar m v' in
                                               [a])) 
  n 
  v


Definitions occuring in Statement :  polyconst: polyconst(n;k),  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  less: if (a) < (b)  then c  else d,  int_eq: if a=b  then c  else d,  polyconst: polyconst(n;k),  subtract: n - m,  natural_number: $n,  callbyvalue: callbyvalue,  apply: f a,  cons: [a / b],  nil: []
FDL editor aliases :  polyvar
Latex:
polyvar(n;v)
==r  if  (v)  <  (0)
              then  []
              else  eval  m  =  n  -  1  in
                        if  (m)  <  (v)
                              then  []
                              else  if  v=0
                                              then  eval  one  =  polyconst(m;1)  in
                                                        eval  zero  =  polyconst(m;0)  in
                                                            [one;  zero]
                                              else  eval  v'  =  v  -  1  in
                                                        eval  a  =  polyvar(m;v')  in
                                                            [a]
Latex:
polyvar(n;v)  ==
    fix((\mlambda{}polyvar,n,v.  if  (v)  <  (0)
                                                then  []
                                                else  eval  m  =  n  -  1  in
                                                          if  (m)  <  (v)
                                                                then  []
                                                                else  if  v=0
                                                                                then  eval  one  =  polyconst(m;1)  in
                                                                                          eval  zero  =  polyconst(m;0)  in
                                                                                              [one;  zero]
                                                                                else  eval  v'  =  v  -  1  in
                                                                                          eval  a  =  polyvar  m  v'  in
                                                                                              [a])) 
    n 
    v


Date html generated: 2017_09_29-PM-06_03_49
Last ObjectModification: 2017_04_26-PM-02_05_15

Theory : integer!polynomials


Home Index