exp : type.
id : name_type.
const : int -> exp.
var : id -> exp.
plus : exp -> exp -> exp.
times : exp -> exp -> exp.
sin : exp -> exp.
cos : exp -> exp.
neg : exp -> exp.
pred diff id exp exp.
diff X (const C) (const 0).
diff X (var X) (const 1).
diff X (var Y) (var Y) :- not(X = Y).
diff X (plus E1 E2) (plus E1' E2')
:- diff X (E1) (E1'), diff X (E2) (E2').
diff X (times E1 E2) ( plus (times E1' E2) (times E1 E2'))
:- diff X (E1) (E1'), diff X (E2) (E2').
diff X (sin E) ( times (cos E) E') :- diff X (E) (E').
diff X (cos E) ( times (neg (sin E)) E') :- diff X (E) (E').
diff X (neg E) ( neg E') :- diff X (E) (E').
?diff x (times (var x) (var x)) E .