123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172 |
- module substexp;
- algebraic;
- depend ff,x;
- depend f,x;
- depend f,!~k;
- operator pssubst;
- operator a,Pproduct;
- subst_rules :=
- { pssubst(- ~g,~x,~a,~n) => -pssubst(g,x,a,n),
- pssubst(~g+~h,~x,~a,~n) => pssubst(g,x,a,n) + pssubst(h,x,a,n),
- pssubst(~c*~g,~x,~a,~n) => c*pssubst(g,x,a,n)
- when freeof(c,x) and freeof(c,g),
- pssubst(df(~f,~x,~k),~x,~a,~n) => Pochhammer(n+1,k) * a(n+k),
- pssubst(df(~f,~x),~x,~a,~n) => (n + 1)* a(n + 1),
- pssubst(~x^~j * df(~f,~x),~x,~a,~n) => Pochhammer(n+1-j,1)*a(n+1-j),
- pssubst(~x^~j * df(~f,~x,~k),~x,~a,~n)=> Pochhammer(n+1-j,k)*a(n+k-j),
- pssubst(ff*~x^~j,~x,~a,~n) => a(n-j),
- pssubst(ff*~x,~x,~a,~n) => a(n-1),
- pssubst(df(~f,~x) *x,~x,~a,~n) => Pochhammer(n,1)*a(n),
- pssubst(df(~f,~x,~k) *x,~x,~a,~n) => Pochhammer(n,k)*a(n+k-1),
- pssubst(f,~x,~a,~n) => a(n),
- pssubst(ff,~x,~a,~n) => a(n),
-
- pssubst(~c,~x,~a,~n) => 0 when freeof(c,x),
- pssubst(~x^~j,~x,~a,~n) => 0 when fixp j,
- pssubst(~x,~x,~a,~n) => 0
- };
- spec_pochhammer :=
- { Pochhammer(~a,~k)//Pochhammer(~b,~k) => (a + k -1)/(a - 1)
- when (a - b)=1,
- Pochhammer(~a,~k)//Pochhammer(~b,~k) => (b - 1)/(b + k -1)
- when (b - a)=1,
- Pochhammer(~z,~k) * Pochhammer(~cz,~k) =>
- prod((repart(z) + (j - 1))^2 + (impart(z))^2,j,1,k)
- when not(impart(z) = 0) and z = conj cz,
- Pochhammer(~k,~n) => 1 when n=0,
- Pochhammer(~k,~n) => Pproduct (k,n) when fixp n,
- Pproduct (~k,~ii) => 1 when ii =0,
- Pproduct (~k,~ii) => (k + ii - 1) * Pproduct (k,ii -1)}$
- spec_factorial :=
- { Factorial (~n) // Factorial (~n+1) => 1/(n+1),
- Factorial (~n) * Factorial (~n) // Factorial (~n+1) =>
- Factorial (n)/(n+1),
- Factorial (~n+1) // Factorial (~n) => (n+1),
- Factorial (~n+1) * Factorial (~n+1) // Factorial (~n) =>
- (n+1) * Factorial (~n+1),
- (~otto ^(~k)) * Factorial (~n) // Factorial (~n +1) => otto^k /(n+1),
- (~otto ^(~k)) * Factorial (~n+1) // Factorial (~n) => otto^k * (n+1),
- (~otto ^~k) * ~hugo * Factorial (~n) // Factorial (~n +1) =>
- otto^k * hugo/(n+1),
- (~otto ^~k) * ~hugo * Factorial (~n+1) // Factorial (~n) =>
- otto^k * hugo *(n+1)}$
- endmodule;
- end;
|