Nuprl Definition : Legendre_changes

Legendre_changes(n) ==
  primrec(n;Ax;λn,x. if n + 1=1
                     then []
                     else eval L = x in
                          let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - i) then inl Ax else (inr (λx.Ax) ) in
                              eval-mklist(n + 0;λi.if i=0
                                                   then if i=n - 1
                                                        then find_rational(<-1, 1>;<1, 1>;d i)
                                                        else eval b = L[i] in
                                                             find_rational(<-1, 1>;b;d i)
                                                   else eval a = L[i - 1] in
                                                        if i=n - 1
                                                        then find_rational(a;<1, 1>;d i)
                                                        else eval b = L[i] in
                                                             find_rational(a;b;d i);0))


Definitions occuring in Statement :  ratLegendre: ratLegendre(n;x),  find_rational: find_rational(a;b;d),  ratsign: ratsign(x),  eval-mklist: eval-mklist(n;f;offset),  exp: i^n,  select: L[n],  nil: [],  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  let: let,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  inr: inr x ,  inl: inl x,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  primrec: primrec(n;b;c),  nil: [],  let: let,  ratsign: ratsign(x),  ratLegendre: ratLegendre(n;x),  exp: i^n,  inl: inl x,  inr: inr x ,  axiom: Ax,  eval-mklist: eval-mklist(n;f;offset),  add: n + m,  lambda: λx.A[x],  minus: -n,  int_eq: if a=b then c else d,  subtract: n - m,  pair: <a, b>,  callbyvalue: callbyvalue,  select: L[n],  find_rational: find_rational(a;b;d),  apply: f a,  natural_number: $n
FDL editor aliases :  Legendre_changes
Latex:
Legendre\_changes(n)  ==
    primrec(n;Ax;\mlambda{}n,x.  if  n  +  1=1
                                          then  []
                                          else  eval  L  =  x  in
                                                    let  d  =  \mlambda{}i,r.  if  ratsign(ratLegendre(n  +  1;r))=(-1)\^{}(n  -  i)
                                                                                then  inl  Ax
                                                                                else  (inr  (\mlambda{}x.Ax)  )  in
                                                            eval-mklist(n  +  0;\mlambda{}i.if  i=0
                                                                                                      then  if  i=n  -  1
                                                                                                                then  find\_rational(<-1,  1>ə,  1>d  i)
                                                                                                                else  eval  b  =  L[i]  in
                                                                                                                          find\_rational(<-1,  1>b;d  i)
                                                                                                      else  eval  a  =  L[i  -  1]  in
                                                                                                                if  i=n  -  1
                                                                                                                then  find\_rational(a;ə,  1>d  i)
                                                                                                                else  eval  b  =  L[i]  in
                                                                                                                          find\_rational(a;b;d  i);0))


Date html generated: 2019_10_31-AM-06_21_02
Last ObjectModification: 2019_01_21-PM-03_37_26

Theory : reals_2


Home Index