YES TRS: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} DP: Strict: { u21#(dout(DX), X, Y) -> din#(der(Y)), u21#(dout(DX), X, Y) -> u22#(din(der(Y)), X, Y, DX), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u31#(dout(DX), X, Y) -> din#(der(Y)), u31#(dout(DX), X, Y) -> u32#(din(der(Y)), X, Y, DX), u41#(dout(DX), X) -> din#(der(DX)), u41#(dout(DX), X) -> u42#(din(der(DX)), X, DX)} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(der(X))) -> u41#(din(der(X)), X), u41#(dout(DX), X) -> u42#(din(der(DX)), X, DX)) (din#(der(der(X))) -> u41#(din(der(X)), X), u41#(dout(DX), X) -> din#(der(DX))) (din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u31#(dout(DX), X, Y) -> u32#(din(der(Y)), X, Y, DX)) (din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u31#(dout(DX), X, Y) -> din#(der(Y))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> din#(der(X))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> din#(der(X))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X))) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> din#(der(X))) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> din#(der(X))) (u31#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(times(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), u21#(dout(DX), X, Y) -> din#(der(Y))) (din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), u21#(dout(DX), X, Y) -> u22#(din(der(Y)), X, Y, DX))} SCCS: Scc: { u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u31#(dout(DX), X, Y) -> din#(der(Y)), u41#(dout(DX), X) -> din#(der(DX))} SCC: Strict: { u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u31#(dout(DX), X, Y) -> din#(der(Y)), u41#(dout(DX), X) -> din#(der(DX))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} POLY: Argument Filtering: pi(u42) = 0, pi(u41#) = [], pi(u41) = [], pi(u32) = 0, pi(times) = [], pi(u31#) = 0, pi(u31) = 0, pi(dout) = [], pi(u22) = 0, pi(plus) = [], pi(der) = [], pi(din#) = [], pi(din) = [], pi(u21#) = [], pi(u21) = [] Usable Rules: {} Interpretation: [u21#] = 0, [u41#] = 0, [din#] = 0, [dout] = 1, [din] = 0 Strict: { u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y), u41#(dout(DX), X) -> din#(der(DX))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), u21#(dout(DX), X, Y) -> din#(der(Y))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(times(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(plus(X, Y))) -> din#(der(X))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> din#(der(X))) (u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)) (din#(der(der(X))) -> u41#(din(der(X)), X), u41#(dout(DX), X) -> din#(der(DX)))} SCCS: Scc: { u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), u41#(dout(DX), X) -> din#(der(DX))} SCC: Strict: { u21#(dout(DX), X, Y) -> din#(der(Y)), din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), u41#(dout(DX), X) -> din#(der(DX))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} POLY: Argument Filtering: pi(u42) = 0, pi(u41#) = [], pi(u41) = [], pi(u32) = 0, pi(times) = [], pi(u31) = [], pi(dout) = [], pi(u22) = [0], pi(plus) = [], pi(der) = [], pi(din#) = [], pi(din) = [], pi(u21#) = [0], pi(u21) = 0 Usable Rules: {} Interpretation: [u21#](x0) = x0 + 1, [u41#] = 1, [din#] = 1, [dout] = 1, [din] = 0 Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), u41#(dout(DX), X) -> din#(der(DX))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(der(X))) -> u41#(din(der(X)), X)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(plus(X, Y))) -> din#(der(X))) (u41#(dout(DX), X) -> din#(der(DX)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> u41#(din(der(X)), X), u41#(dout(DX), X) -> din#(der(DX)))} SCCS: Scc: { din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), u41#(dout(DX), X) -> din#(der(DX))} SCC: Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)), u41#(dout(DX), X) -> din#(der(DX))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} POLY: Argument Filtering: pi(u42) = [0], pi(u41#) = 0, pi(u41) = 0, pi(u32) = [0,3], pi(times) = [], pi(u31) = 0, pi(dout) = [0], pi(u22) = 0, pi(plus) = [], pi(der) = [], pi(din#) = [], pi(din) = [], pi(u21) = [] Usable Rules: {} Interpretation: [din#] = 0, [dout](x0) = x0 + 1, [din] = 0 Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(der(X))) -> u41#(din(der(X)), X)) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X))) (din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)))} SCCS: Scc: { din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} SCC: Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(plus(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} POLY: Argument Filtering: pi(u42) = [], pi(u41) = [], pi(u32) = [], pi(times) = 0, pi(u31) = [], pi(dout) = [], pi(u22) = [], pi(plus) = [0], pi(der) = 0, pi(din#) = 0, pi(din) = [], pi(u21) = [] Usable Rules: {} Interpretation: [plus](x0) = x0 + 1 Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(times(X, Y))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))) (din#(der(times(X, Y))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X))) (din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X)))} SCCS: Scc: { din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} SCC: Strict: { din#(der(der(X))) -> din#(der(X)), din#(der(times(X, Y))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} POLY: Argument Filtering: pi(u42) = [], pi(u41) = [], pi(u32) = [], pi(times) = [0], pi(u31) = [], pi(dout) = [], pi(u22) = [], pi(plus) = [], pi(der) = 0, pi(din#) = 0, pi(din) = [], pi(u21) = [] Usable Rules: {} Interpretation: [times](x0) = x0 + 1 Strict: {din#(der(der(X))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} EDG: {(din#(der(der(X))) -> din#(der(X)), din#(der(der(X))) -> din#(der(X)))} SCCS: Scc: {din#(der(der(X))) -> din#(der(X))} SCC: Strict: {din#(der(der(X))) -> din#(der(X))} Weak: { u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX), din(der(der(X))) -> u41(din(der(X)), X), din(der(plus(X, Y))) -> u21(din(der(X)), X, Y), din(der(times(X, Y))) -> u31(din(der(X)), X, Y), u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY)), u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX), u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX))), u41(dout(DX), X) -> u42(din(der(DX)), X, DX), u42(dout(DDX), X, DX) -> dout(DDX)} SPSC: Simple Projection: pi(din#) = 0 Strict: {} Qed