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;


