Prolog snippet with term replacement system for symbolic differentiation (not quite complete)

symbMathTermDifferentiate.pl

rule(0+X,X). 
rule(X+0,X).
rule(1*X,X).
rule(X*1,X).
rule(1*X,X).
rule(0*_,0).
rule(_*0,0).
rule(sum(_,0),0).

rule((X+Y)*Z, (X*Z)+(Y*Z)).
rule(X*(Y+Z), X*Y + X*Z).

rule(X+(Y+Z), X+Y+Z).
rule(X*(Y*Z), X*Y*Z).

rule(X+Y, Y+X) :- X @< Y.
rule(X*Y, Y*X) :- X @< Y.
rule(X+Y+Z, X+Z+Y) :- Y @< Z.
rule(X*Y*Z, X*Z*Y) :- Y @< Z.

rule(X+X, X*2).

rule(d(V,X + Y), d(V,X) + d(V,Y)).
rule(d(V,X*Y), d(V,X) * Y + X * d(V,Y)).
rule(d(V,V), 1).
rule(d(V,N), 0) :- number(N); atom(N), V \= N.
rule(d(V,sum(I,T)), sum(I,d(V,T))).

rule(d(V,X),D * d(V,A)) :- X =.. [F,A], atomic_concat(F,'`',FD), D =.. [FD,d(V,A)].

applyrules(P,X,TX) :- call(P,X,T), !, applyrules(P,T,TX), !.
applyrules(_,X,X).

treplacelist(_,[],[]) :- !.
treplacelist(P,[H|T], [HR|TR]) :- treplace(P,H,HR), treplacelist(P,T,TR), !.

treplace(X,TX) :- treplace(rule,X,TX).

treplace(P,X,TX) :- applyrules(P, X, XR), XR =.. [F|L], treplacelist(P, L,LR), XRR =.. [F|LR], 
	applyrules(P, XRR, XRRR), !, (XRR \= XRRR, !, treplace(P,XRRR,TX); XRRR = TX).

subst(V,S,V,S) :- !.
subst(_,_,[],[]) :- !.
subst(V,S,[H|T],[HS|TS]) :- !, subst(V,S,H,HS), subst(V,S,T,TS), !.
subst(V,S,T,TS) :- !, T =.. [TF|Args], subst(V,S,Args,Sargs), TS =.. [TF|Sargs], !.

printLtx(T) :- treplace(printrule,T,T1), !, print('$$'), write_term(T1,[]), print('$$'), nl.

printrule(d(V,T), R) :- atomic_list_concat(['\\frac{d}{d', V, '}'], P), R =.. [P,T].
printrule(sum(V,T), R) :- atomic_list_concat(['\\sum_{', V, '}'], P), R =.. [P,T].
printrule(ind(V,T), R) :- T=.. [F|A], atomic_list_concat(['{', F, '}_{', V, '}'], P), R =.. [P|A].

printEval(T) :- print(T), nl, treplace(T,TR), print(TR), nl, printLtx(T=TR), nl, nl.

/* 
treplace is the term replacer, printLtx prints a LaTeX representation of a term, e.g. for use with MathJax.
d(V,T) means the derivation of term T after variable V.
subst is term substitution> subst(Term,SubstitutedBy,InTerm,Result)
*/