Nuprl Definition : LegendreChangesAux

LegendreChangesAux(n; m; L; i; j; s) ==
  if i=m
  then L
  else eval i' = i + 1 in
       eval s' = ratLegendreSign(n;i';m) in
         if s'=0
         then LegendreChangesAux(n; m; L; i'; j; s)
         else if s'=s
              then LegendreChangesAux(n; m; L; i'; i'; s')
              else LegendreChangesAux(n; m; [<j, i'> / L]; i'; i'; s')

Definitions occuring in Statement : ratLegendreSign: ratLegendreSign(n;k;m), cons: [a / b], callbyvalue: callbyvalue, int_eq: if a=b then c else d, pair: <a, b>, add: n + m, natural_number: $n
Definitions occuring in definition : add: n + m, callbyvalue: callbyvalue, ratLegendreSign: ratLegendreSign(n;k;m), natural_number: $n, int_eq: if a=b then c else d, cons: [a / b], pair: <a, b>

Latex:
LegendreChangesAux(n; m; L; i; j; s) == if i=m then L else eval i' = i + 1 in eval s' = ratLegendreSign(n;i';m) in if s'=0 then LegendreChangesAux(n; m; L; i'; j; s) else if s'=s then LegendreChangesAux(n; m; L; i'; i'; s') else LegendreChangesAux(n; m; [<j, i'> / L]; i'; i'; s') Date html generated: 2019_10_31-AM-06_22_34 Last ObjectModification: 2019_02_17-PM-02_09_24 Theory : reals_2 Home Index