Nuprl Definition : LegCh

LegCh(n) ==
  primrec(n;Ax;λn,x. if n + 1=1
                     then []
                     else mklist(n

                          + 0;λi.find_rational(if i=0 then <-1, 1> else x[i - 1];if i=n - 1

                                                                                 then <1, 1>

                                                                                 else x[i];λr.if ratsign(ratLegendre(n

                                                                                              + 1;r))=(-1)^((n + 0) - i)

                                                                                              then inl Ax

                                                                                              else (inr (λx.Ax) ))))

Definitions occuring in Statement : ratLegendre: ratLegendre(n;x), find_rational: find_rational(a;b;d), ratsign: ratsign(x), mklist: mklist(n;f), exp: i^n, select: L[n], nil: [], primrec: primrec(n;b;c), int_eq: if a=b then c else d, 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: [], mklist: mklist(n;f), find_rational: find_rational(a;b;d), pair: <a, b>, select: L[n], int_eq: if a=b then c else d, ratsign: ratsign(x), ratLegendre: ratLegendre(n;x), exp: i^n, minus: -n, subtract: n - m, add: n + m, natural_number: $n, inl: inl x, inr: inr x , lambda: λx.A[x], axiom: Ax
FDL editor aliases : LegCh

Latex:
LegCh(n) == primrec(n;Ax; \mlambda{}n,x. if n + 1=1 then [] else mklist(n + 0;\mlambda{}i.find\_rational(if i=0 then <-1, 1> else x[i - 1];if i=n - 1 then ə, 1> else x[i];\mlambda{}r.if ratsign(ratLegendre(n + 1;r))=(-1)\^{}((n + 0) - i) then inl Ax else (inr (\mlambda{}x.Ax) )))) Date html generated: 2019_10_31-AM-06_23_07 Last ObjectModification: 2019_01_19-PM-05_10_12 Theory : reals_2 Home Index