substexp.red 2.1 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172
  1. module substexp;
  2. algebraic;
  3. depend ff,x;
  4. depend f,x;
  5. depend f,!~k;
  6. operator pssubst;
  7. operator a,Pproduct;
  8. subst_rules :=
  9. { pssubst(- ~g,~x,~a,~n) => -pssubst(g,x,a,n),
  10. pssubst(~g+~h,~x,~a,~n) => pssubst(g,x,a,n) + pssubst(h,x,a,n),
  11. pssubst(~c*~g,~x,~a,~n) => c*pssubst(g,x,a,n)
  12. when freeof(c,x) and freeof(c,g),
  13. pssubst(df(~f,~x,~k),~x,~a,~n) => Pochhammer(n+1,k) * a(n+k),
  14. pssubst(df(~f,~x),~x,~a,~n) => (n + 1)* a(n + 1),
  15. pssubst(~x^~j * df(~f,~x),~x,~a,~n) => Pochhammer(n+1-j,1)*a(n+1-j),
  16. pssubst(~x^~j * df(~f,~x,~k),~x,~a,~n)=> Pochhammer(n+1-j,k)*a(n+k-j),
  17. pssubst(ff*~x^~j,~x,~a,~n) => a(n-j),
  18. pssubst(ff*~x,~x,~a,~n) => a(n-1),
  19. pssubst(df(~f,~x) *x,~x,~a,~n) => Pochhammer(n,1)*a(n),
  20. pssubst(df(~f,~x,~k) *x,~x,~a,~n) => Pochhammer(n,k)*a(n+k-1),
  21. pssubst(f,~x,~a,~n) => a(n),
  22. pssubst(ff,~x,~a,~n) => a(n),
  23. pssubst(~c,~x,~a,~n) => 0 when freeof(c,x),
  24. pssubst(~x^~j,~x,~a,~n) => 0 when fixp j,
  25. pssubst(~x,~x,~a,~n) => 0
  26. };
  27. spec_pochhammer :=
  28. { Pochhammer(~a,~k)//Pochhammer(~b,~k) => (a + k -1)/(a - 1)
  29. when (a - b)=1,
  30. Pochhammer(~a,~k)//Pochhammer(~b,~k) => (b - 1)/(b + k -1)
  31. when (b - a)=1,
  32. Pochhammer(~z,~k) * Pochhammer(~cz,~k) =>
  33. prod((repart(z) + (j - 1))^2 + (impart(z))^2,j,1,k)
  34. when not(impart(z) = 0) and z = conj cz,
  35. Pochhammer(~k,~n) => 1 when n=0,
  36. Pochhammer(~k,~n) => Pproduct (k,n) when fixp n,
  37. Pproduct (~k,~ii) => 1 when ii =0,
  38. Pproduct (~k,~ii) => (k + ii - 1) * Pproduct (k,ii -1)}$
  39. spec_factorial :=
  40. { Factorial (~n) // Factorial (~n+1) => 1/(n+1),
  41. Factorial (~n) * Factorial (~n) // Factorial (~n+1) =>
  42. Factorial (n)/(n+1),
  43. Factorial (~n+1) // Factorial (~n) => (n+1),
  44. Factorial (~n+1) * Factorial (~n+1) // Factorial (~n) =>
  45. (n+1) * Factorial (~n+1),
  46. (~otto ^(~k)) * Factorial (~n) // Factorial (~n +1) => otto^k /(n+1),
  47. (~otto ^(~k)) * Factorial (~n+1) // Factorial (~n) => otto^k * (n+1),
  48. (~otto ^~k) * ~hugo * Factorial (~n) // Factorial (~n +1) =>
  49. otto^k * hugo/(n+1),
  50. (~otto ^~k) * ~hugo * Factorial (~n+1) // Factorial (~n) =>
  51. otto^k * hugo *(n+1)}$
  52. endmodule;
  53. end;