Nuprl Definition : rP_to

Nuprl Definition : rP_to_poly

rP_to_poly(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more

                                              in rP_to_poly([if c=0  then []  else [<c, []>] / stack];evenmore)

else if op=2

                                                 then let v,evenmore = more

                                                      in rP_to_poly(<[<1, [v]>], stack>;evenmore)

else if op=3

                                                         then let q,p,s = stack in

                                                              rP_to_poly([add_ipoly(p;q) / s];more)

                                                         else if op=4

                                                                 then let q,p,s = stack in

                                                                      rP_to_poly([add_ipoly(p;minus-poly(q)) / s];more)

                                                                 else if op=5

                                                                         then let q,p,s = stack in

                                                                              rP_to_poly([mul_ipoly(p;q) / s];more)

                                                                         else let p,s = stack

                                                                              in rP_to_poly([minus-poly(p) / s];more)

rP_to_poly(stack;L) ==
  fix((λrP_to_poly,stack,L. if L = Ax then stack
                            otherwise let op,more = L
                                      in if op=1
                                            then let c,evenmore = more

                                                 in rP_to_poly [if c=0  then []  else [<c, []>] / stack] evenmore

else if op=2

                                                    then let v,evenmore = more

                                                         in rP_to_poly <[<1, [v]>], stack> evenmore

else if op=3

                                                            then let q,p,s = stack in

                                                                 rP_to_poly [add_ipoly(p;q) / s] more

                                                            else if op=4

                                                                    then let q,p,s = stack in

                                                                         rP_to_poly [add_ipoly(p;minus-poly(q)) / s]

                                                                         more

                                                                    else if op=5

                                                                            then let q,p,s = stack in

                                                                                 rP_to_poly [mul_ipoly(p;q) / s] more

                                                                            else let p,s = stack

                                                                                 in rP_to_poly [minus-poly(p) / s] more)\000C)

stack
L

Definitions occuring in Statement : mul_ipoly: mul_ipoly(p;q), minus-poly: minus-poly(p), add_ipoly: add_ipoly(p;q), cons: [a / b], nil: [], spreadn: spread3, isaxiom: if z = Ax then a otherwise b, int_eq: if a=b then c else d, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, pair: <a, b>, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], isaxiom: if z = Ax then a otherwise b, pair: <a, b>, nil: [], add_ipoly: add_ipoly(p;q), int_eq: if a=b then c else d, natural_number: $n, spreadn: spread3, mul_ipoly: mul_ipoly(p;q), spread: spread def, apply: f a, cons: [a / b], minus-poly: minus-poly(p)
FDL editor aliases : rP_to_poly

Latex:
rP\_to\_poly(stack;L) ==r if L = Ax then stack otherwise let op,more = L in if op=1 then let c,evenmore = more in rP\_to\_poly([if c=0 then [] else [<c, []>] / stack];evenmore) else if op=2 then let v,evenmore = more in rP\_to\_poly(<[ə, [v]>], stack>evenmore) else if op=3 then let q,p,s = stack in rP\_to\_poly([add\_ipoly(p;q) / s];more) else if op=4 then let q,p,s = stack in rP\_to\_poly([add\_ipoly(p;minus-poly(q)) / s];more) else if op=5 then let q,p,s = stack in rP\_to\_poly([mul\_ipoly(p;q) / s];more) else let p,s = stack in rP\_to\_poly([minus-poly(p) / s];more)

Latex:
rP\_to\_poly(stack;L) == fix((\mlambda{}rP\_to$_{poly}$,stack,L. if L = Ax then stack otherwise let op,more = L in if op=1 then let c,evenmore = more in rP\_to$_{poly}$ [if c=0 then [] else [<c, []>] / stack] evenmore else if op=2 then let v,evenmore = more in rP\_to$_{poly}$ <[ə, [\000Cv]>], stack> evenmore else if op=3 then let q,p,s = stack in rP\_to$_{poly}$ [a\000Cdd\_ipoly(p;q) / s] more else if op=4 then let q,p,s = stack in rP\_to$_{poly}\000C$ [add\_ipoly(p;...) / s] more else if op=5 then let q,p,s = stack in rP\_to$_{p\000Coly}$ [mul\_ipoly(p;q) / s] more else let p,s = stack in rP\_to$_\mbackslash{}ff\000C7bpoly}$ [minus-poly(p) / s] more)) stack L Date html generated: 2017_09_29-PM-05_54_43 Last ObjectModification: 2017_05_12-PM-05_39_04 Theory : omega Home Index