input_case nil$

% Substituting an expression for a variable
% -----------------------------------------
a:=(x+y)^2; a:=sub(x=x+1,a); a:=sub(x=x-1,y=y^2,a);
sub(x=y,y=x,a); % variable interchange
clear a;

% Defining a substitution rule
% ----------------------------
let x*y^2=z; x^2*y^4; x^3*y^5;
clear x*y^2; x^2*y^4; % removing this rule

let x=y+1,y=2*x; x;   % an infinite loop
clear x,y;

% Complex algebra
% ---------------
z:=x+i*y; z:=z^2;
repart(z);
% x and y are real
let repart(x)=x,impart(x)=0,repart(y)=y,impart(y)=0;
impart(z); conj(z);
sub(i=-i,z);        % complex conjugate
1/z;
on rationalize; ws; % getting rid of i in denominator
off rationalize; clear z;
clear repart(x),impart(x),repart(y),impart(y);

% User functions
% --------------
operator f; let f(x)=x^2; f(x); f(x+y);
clear f(x);

for all x let f(x)=x^2; f(x); f(x+y);
for all x clear f(x);

for all x such that fixp(x) let f(x)=x^2; % if x is integer
f(a); a:=2$ f(a); clear a;
for all x such that fixp(x) clear f(x);

a:=(x*f(x))^2; df(a,x);

operator f2; for all x let df(f(x),x)=f2(x); df(a,x);
for all x clear df(f(x),x); clear a; clear f2;

% defining even and odd functions
operator fe,fo; even fe; odd fo;
fe(x); fe(-x); fe(x-y)+fe(y-x);
fo(x-y); fo(y-x); fo(0);
clear fe,fo;

% let's define an odd function ourselves
let f(0)=0;
for all x such that not ordp(-x,x) let f(x)=-f(-x);
f(x); f(-x); f(x-y); f(y-x); f(x-y)+f(y-x);
clear f(0); for all x such that not ordp(-x,x) clear f(x);

% defining symmetric and antisymmetric functions
operator S,A; symmetric S; antisymmetric A;
S(x,y,z); S(y,x,z); S(z,y,x);
A(x,y,z); A(y,x,z); A(z,y,x); A(x,y,x);
clear S,A;

% let's define an antisymmetric function ourselves
for all x let f(x,x)=0;
for all x,y such that not ordp(y,x) let f(x,y)=-f(y,x);
f(x,y); f(y,x); f(x+y,x+y); f(x+y,x-y)+2*f(x-y,x+y);
for all x clear f(x,x);
for all x,y such that not ordp(y,x) clear f(x,y);

% defining a function linear in first argument
operator lin; linear lin; lin(a+b*x+c*x^2,x);
% x-independent factors are placed outside lin
clear lin;

% switching substitutions on and off
for all x such that fixp(x) and c neq 0 let f(x)=x^2;
c:=1$ f(2); c:=0$ f(2);
for all x such that fixp(x) and c neq 0 clear f(x); clear f;

% Defining function properties using substitutions
% ------------------------------------------------
% 1. Properties of log
for all x,y let log(x/y)=log(x)-log(y),
    log(x*y)=log(x)+log(y),log(x^y)=y*log(x);
log(x*e^y); log(x/2+y); log(x*(a+1));

for all x,y such that x neq 1 and remainder(y,x)=0 let
    log(x+y)=log(x)+log(1+y/x);
for all x,y,z such that remainder(z,x)=0 let
    log(x*y+z)=log(x)+log(y+z/x);
log(x*(a+1)); log(x*(a+b+c)/y);

for all x,y clear log(x/y),log(x*y),log(x^y);
for all x,y such that remainder(y,x)=0 clear log(x+y);
for all x,y,z such that remainder(z,x)=0 clear log(x*y+z);

% 2. Transforming products of sin, cos into sums
% Fourier analysis
for all x let cos(x)^2=(1+cos(2*x))/2,
              sin(x)^2=(1-cos(2*x))/2;
for all x,y let cos(x)*cos(y)=(cos(x-y)+cos(x+y))/2,
                sin(x)*sin(y)=(cos(x-y)-cos(x+y))/2,
                sin(x)*cos(y)=(sin(x-y)+sin(x+y))/2;
factor cos,sin;
a:=a1*cos(x)+a2*cos(2*x)+b1*sin(x)+b2*sin(2*x)$ a^2;
clear a; for all x clear cos(x)^2,sin(x)^2;
for all x,y clear cos(x)*cos(y),sin(x)*sin(y),sin(x)*cos(y);
remfac cos,sin;

% 3. Expanding sin, cos of sums and multiple angles
for all x let cos(x)^2=1-sin(x)^2;
for all x,y let sin(x+y)=sin(x)*cos(y)+cos(x)*sin(y),
                cos(x+y)=cos(x)*cos(y)-sin(x)*sin(y);
sin(u+v); sin(u-v); sin(x+y+z); sin(x/2+y);

for all x,y,z let
    sin((x+y)/z)=sin(x/z)*cos(y/z)+cos(x/z)*sin(y/z),
    cos((x+y)/z)=cos(x/z)*cos(y/z)-sin(x/z)*sin(y/z);
sin(x/2+y); sin(pi/2+x);

for all n,x such that fixp(n) and n>1 let
    sin(n*x)=sin(x)*cos((n-1)*x)+cos(x)*sin((n-1)*x),
    cos(n*x)=cos(x)*cos((n-1)*x)-sin(x)*sin((n-1)*x);
sin(2*x); sin(4*x); sin(4*x/u);

for all n,x,z such that fixp(n) and n>1 let
    sin(n*x/z)=sin(x/z)*cos((n-1)*x/z)+cos(x/z)*sin((n-1)*x/z),
    cos(n*x/z)=cos(x/z)*cos((n-1)*x/z)-sin(x/z)*sin((n-1)*x/z);
sin(4*x/u); sin(4*x/3); sin(4);

for all x clear cos(x)^2;
for all x,y clear sin(x+y),cos(x+y);
for all x,y,z clear sin((x+y)/z),cos((x+y)/z);
for all n,x such that fixp(n) and n>1 clear sin(n*x),cos(n*x);
for all n,x,z such that fixp(n) and n>1 clear
    sin(n*x/z),cos(n*x/z);

end;