Nuprl Definition : ratLegendre-aux
ratLegendre-aux(n;x;tr) ==
  let k,a,b = tr in 
  if k=n
  then a
  else eval k' = k + 1 in
       eval a' = rat-nat-div(ratadd(int-rat-mul((2 * k) + 1;ratmul(x;a));int-rat-mul(-k;b));k') in
         ratLegendre-aux(n;x;<k', a', a>)
Definitions occuring in Statement : 
rat-nat-div: rat-nat-div(x;n), 
int-rat-mul: int-rat-mul(n;x), 
ratmul: ratmul(a;b), 
ratadd: ratadd(x;y), 
callbyvalue: callbyvalue, 
spreadn: spread3, 
int_eq: if a=b then c else d, 
pair: <a, b>, 
multiply: n * m, 
add: n + m, 
minus: -n, 
natural_number: $n
Definitions occuring in definition : 
spreadn: spread3, 
int_eq: if a=b then c else d, 
callbyvalue: callbyvalue, 
rat-nat-div: rat-nat-div(x;n), 
ratadd: ratadd(x;y), 
add: n + m, 
multiply: n * m, 
natural_number: $n, 
ratmul: ratmul(a;b), 
int-rat-mul: int-rat-mul(n;x), 
minus: -n, 
pair: <a, b>
FDL editor aliases : 
ratLegendre-aux
Latex:
ratLegendre-aux(n;x;tr)  ==
    let  k,a,b  =  tr  in 
    if  k=n
    then  a
    else  eval  k'  =  k  +  1  in
              eval  a'  =  rat-nat-div(ratadd(int-rat-mul((2  *  k)  +  1;ratmul(x;a));int-rat-mul(-k;b));k')  in
                  ratLegendre-aux(n;x;<k',  a',  a>)
Date html generated:
2019_10_30-AM-11_34_01
Last ObjectModification:
2019_01_10-PM-03_56_20
Theory : reals_2
Home
Index