; @origtpdbfilename ./TRS/Rubio/wst99.trs
; @xtcfilename "./TRS_Standard/Rubio_04/wst99.xml"
(format TRS)
(fun din 1)
(fun der 1)
(fun plus 2)
(fun u21 3)
(fun dout 1)
(fun u22 4)
(fun times 2)
(fun u31 3)
(fun u32 4)
(fun u41 2)
(fun u42 3)
(rule (din (der (plus X Y))) (u21 (din (der X)) X Y))
(rule (u21 (dout DX) X Y) (u22 (din (der Y)) X Y DX))
(rule (u22 (dout DY) X Y DX) (dout (plus DX DY)))
(rule (din (der (times X Y))) (u31 (din (der X)) X Y))
(rule (u31 (dout DX) X Y) (u32 (din (der Y)) X Y DX))
(rule (u32 (dout DY) X Y DX) (dout (plus (times X DY) (times Y DX))))
(rule (din (der (der X))) (u41 (din (der X)) X))
(rule (u41 (dout DX) X) (u42 (din (der DX)) X DX))
(rule (u42 (dout DDX) X DX) (dout DDX))