:- op(1150, xfx, <=).
:- op(950,xfy, &).

dsolve(true, D, D).
dsolve(A & B,D0,D) :- dsolve(A,D0,D1), dsolve(B,D1,D).
dsolve(A,    D, [A|D]) :- delay(A).
dsolve(A,    D, D) :- builtin(A), call(A).
dsolve(A,    D0,D) :- (A <= B), dsolve(B,D0,D).

builtin(is(_,_)).   builtin(dif(_,_)).