Term-Ersetzung und Computeralgebra

Regeln (Term-Ersetzungs-System) für das Differenzieren:

D_x(x) = 1, wennx $\displaystyle \notin$ A : D_x(A) = 0

D_x(A + B) = D_x(A) + D_x(B)

D_x(A⋅B) = ..., D_x(A/B) = …

D_x(log x) = 1/x, D_x(sin x) = cos x,…

Dazu braucht man aber noch Vereinfachungsregeln.
Wie drückt man die Kettenregel D_x(f (g(x)) = ... aus?
Hier sind f und g Variablen, aber zweiter Ordnung (bezeichnen Funktionen).
allgemein: Higher Order Rewriting (HOR) als Verallgemeinerung von TRS und Lambda-Kalkül

D_x(x) = 1, wennx $\displaystyle \notin$ A : D_x(A) = 0
D_x(A + B) = D_x(A) + D_x(B)
D_x(A⋅B) = ..., D_x(A/B) = …
D_x(log x) = 1/x, D_x(sin x) = cos x,…