Nuprl Definition : pos-Legendre-changes

pos-Legendre-changes(n) ==
  primrec(n;Ax;λn,x. if n + 1=1
                     then []
                     else eval L = x in
                          eval m = n ÷ 2 in
                          eval r = n rem 2 in
                            if r=1
                            then let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - i)
                                               then inl Ax
                                               else (inr (λx.Ax) ) in
                                     eval-mklist(m;λi.eval a = L[i] in
                                                      if i=m - 1
                                                      then find_rational(a;<1, 1>;d i)
                                                      else eval b = L[i + 1] in
                                                           find_rational(a;b;d i);0)
                            else let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - 1 - i)
                                               then inl Ax
                                               else (inr (λx.Ax) ) in
                                     eval-mklist(m;λi.if i=0
                                                      then if i=m - 1
                                                           then find_rational(<0, 1>;<1, 1>;d i)
                                                           else eval b = L[i] in
                                                                find_rational(<0, 1>;b;d i)
                                                      else eval a = L[i - 1] in
                                                           if i=m - 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,  remainder: n rem m,  divide: n ÷ m,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  subtract: n - m,  int_eq: if a=b then c else d,  natural_number: $n,  select: L[n],  callbyvalue: callbyvalue,  apply: f a,  pair: <a, b>,  find_rational: find_rational(a;b;d),  lambda: λx.A[x],  eval-mklist: eval-mklist(n;f;offset),  axiom: Ax,  inr: inr x ,  inl: inl x,  minus: -n,  exp: i^n,  add: n + m,  ratLegendre: ratLegendre(n;x),  ratsign: ratsign(x),  let: let,  remainder: n rem m,  divide: n ÷ m,  nil: [],  primrec: primrec(n;b;c)
FDL editor aliases :  pos-Legendre-changes
Latex:
pos-Legendre-changes(n)  ==
    primrec(n;Ax;\mlambda{}n,x.  if  n  +  1=1
                                          then  []
                                          else  eval  L  =  x  in
                                                    eval  m  =  n  \mdiv{}  2  in
                                                    eval  r  =  n  rem  2  in
                                                        if  r=1
                                                        then  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(m;\mlambda{}i.eval  a  =  L[i]  in
                                                                                                            if  i=m  -  1
                                                                                                            then  find\_rational(a;ə,  1>d  i)
                                                                                                            else  eval  b  =  L[i  +  1]  in
                                                                                                                      find\_rational(a;b;d  i);0)
                                                        else  let  d  =  \mlambda{}i,r.  if  ratsign(ratLegendre(n  +  1;r))=(-1)\^{}(n  -  1  -  i)
                                                                                              then  inl  Ax
                                                                                              else  (inr  (\mlambda{}x.Ax)  )  in
                                                                          eval-mklist(m;\mlambda{}i.if  i=0
                                                                                                            then  if  i=m  -  1
                                                                                                                      then  find\_rational(ɘ,  1>ə,  1>d  i)
                                                                                                                      else  eval  b  =  L[i]  in
                                                                                                                                find\_rational(ɘ,  1>b;d  i)
                                                                                                            else  eval  a  =  L[i  -  1]  in
                                                                                                                      if  i=m  -  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_22_51
Last ObjectModification: 2019_01_21-PM-04_52_14

Theory : reals_2


Home Index