WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3} / {der/1,dout/1,plus/2,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {din,u21,u22,u31,u32,u41,u42} and constructors {der,dout ,plus,times} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) u22#(dout(DY),X,Y,DX) -> c_5() u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) u32#(dout(DY),X,Y,DX) -> c_7() u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) u42#(dout(DDX),X,DX) -> c_9() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) u22#(dout(DY),X,Y,DX) -> c_5() u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) u32#(dout(DY),X,Y,DX) -> c_7() u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) u42#(dout(DDX),X,DX) -> c_9() - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5,7,9} by application of Pre({5,7,9}) = {4,6,8}. Here rules are labelled as follows: 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 4: u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) 5: u22#(dout(DY),X,Y,DX) -> c_5() 6: u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) 7: u32#(dout(DY),X,Y,DX) -> c_7() 8: u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) 9: u42#(dout(DDX),X,DX) -> c_9() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) - Weak DPs: u22#(dout(DY),X,Y,DX) -> c_5() u32#(dout(DY),X,Y,DX) -> c_7() u42#(dout(DDX),X,DX) -> c_9() - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) -->_1 u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))):6 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 2:S:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) -->_1 u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))):4 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 3:S:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) -->_1 u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))):5 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 4:S:u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) -->_1 u22#(dout(DY),X,Y,DX) -> c_5():7 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 5:S:u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) -->_1 u32#(dout(DY),X,Y,DX) -> c_7():8 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 6:S:u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) -->_1 u42#(dout(DDX),X,DX) -> c_9():9 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 7:W:u22#(dout(DY),X,Y,DX) -> c_5() 8:W:u32#(dout(DY),X,Y,DX) -> c_7() 9:W:u42#(dout(DDX),X,DX) -> c_9() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: u22#(dout(DY),X,Y,DX) -> c_5() 8: u32#(dout(DY),X,Y,DX) -> c_7() 9: u42#(dout(DDX),X,DX) -> c_9() * Step 4: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) -->_1 u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))):6 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 2:S:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) -->_1 u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))):4 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 3:S:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) -->_1 u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))):5 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 4:S:u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))) -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 5:S:u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))) -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 6:S:u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))) -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) * Step 5: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 4: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) The strictly oriented rules are moved into the weak component. ** Step 5.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#} TcT has computed the following interpretation: p(der) = [0] p(din) = [0] p(dout) = [1] p(plus) = [1] x2 + [0] p(times) = [1] x2 + [1] p(u21) = [0] p(u22) = [1] x1 + [0] p(u31) = [1] x1 + [0] p(u32) = [1] p(u41) = [1] x1 + [0] p(u42) = [7] x1 + [0] p(din#) = [0] p(u21#) = [2] x1 + [0] p(u22#) = [4] x4 + [1] p(u31#) = [6] x1 + [0] p(u32#) = [1] x1 + [2] x3 + [2] x4 + [1] p(u41#) = [0] p(u42#) = [0] p(c_1) = [4] x1 + [2] x2 + [0] p(c_2) = [1] x1 + [1] x2 + [0] p(c_3) = [1] x1 + [2] x2 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [2] x1 + [6] p(c_7) = [1] p(c_8) = [4] x1 + [0] p(c_9) = [1] Following rules are strictly oriented: u21#(dout(DX),X,Y) = [2] > [0] = c_4(din#(der(Y))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = [0] >= [0] = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = [0] >= [0] = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = [0] >= [0] = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u31#(dout(DX),X,Y) = [6] >= [6] = c_6(din#(der(Y))) u41#(dout(DX),X) = [0] >= [0] = c_8(din#(der(DX))) din(der(der(X))) = [0] >= [0] = u41(din(der(X)),X) din(der(plus(X,Y))) = [0] >= [0] = u21(din(der(X)),X,Y) din(der(times(X,Y))) = [0] >= [0] = u31(din(der(X)),X,Y) u21(dout(DX),X,Y) = [0] >= [0] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [1] >= [1] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [1] >= [1] = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = [1] >= [1] = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = [1] >= [0] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [7] >= [1] = dout(DDX) ** Step 5.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ** Step 5.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 4: u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) 5: u41#(dout(DX),X) -> c_8(din#(der(DX))) The strictly oriented rules are moved into the weak component. *** Step 5.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#} TcT has computed the following interpretation: p(der) = [0] p(din) = [0] p(dout) = [2] p(plus) = [1] x2 + [1] p(times) = [6] p(u21) = [3] x1 + [0] p(u22) = [4] x1 + [5] p(u31) = [4] x1 + [0] p(u32) = [1] x1 + [3] p(u41) = [1] x1 + [0] p(u42) = [1] x1 + [0] p(din#) = [0] p(u21#) = [3] x1 + [0] p(u22#) = [1] x1 + [1] x2 + [1] p(u31#) = [4] x1 + [0] p(u32#) = [2] x3 + [2] p(u41#) = [4] x1 + [0] p(u42#) = [4] x2 + [1] x3 + [0] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [4] x1 + [4] x2 + [0] p(c_3) = [4] x1 + [2] x2 + [0] p(c_4) = [1] x1 + [6] p(c_5) = [2] p(c_6) = [4] x1 + [0] p(c_7) = [1] p(c_8) = [4] x1 + [6] p(c_9) = [1] Following rules are strictly oriented: u31#(dout(DX),X,Y) = [8] > [0] = c_6(din#(der(Y))) u41#(dout(DX),X) = [8] > [6] = c_8(din#(der(DX))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = [0] >= [0] = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = [0] >= [0] = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = [0] >= [0] = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = [6] >= [6] = c_4(din#(der(Y))) din(der(der(X))) = [0] >= [0] = u41(din(der(X)),X) din(der(plus(X,Y))) = [0] >= [0] = u21(din(der(X)),X,Y) din(der(times(X,Y))) = [0] >= [0] = u31(din(der(X)),X,Y) u21(dout(DX),X,Y) = [6] >= [5] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [13] >= [2] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [8] >= [3] = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = [5] >= [2] = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = [2] >= [0] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [2] >= [2] = dout(DDX) *** Step 5.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 5.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) Consider the set of all dependency pairs 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 4: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) 5: u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) 6: u41#(dout(DX),X) -> c_8(din#(der(DX))) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {3} These cover all (indirect) predecessors of dependency pairs {3,5} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 5.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#} TcT has computed the following interpretation: p(der) = x1 p(din) = 0 p(dout) = 1 + x1 p(plus) = x1 p(times) = 2 + x1 p(u21) = 2*x1 + 2*x1*x2 + 3*x1*x3 + 2*x1^2 p(u22) = 2*x1 + 3*x1*x2 + 2*x1^2 + 2*x2*x4 + 3*x3 + x4 + x4^2 p(u31) = 3*x1*x3 + 2*x1^2 p(u32) = x1 + x1*x2 + 2*x1*x3 + 2*x1^2 + 3*x3 + x3*x4 p(u41) = 2*x1*x2 + x1^2 p(u42) = 1 + 2*x1 + 2*x1*x2 + 2*x1^2 + 2*x2 + x2*x3 + x3 p(din#) = 1 + 2*x1 p(u21#) = 2*x1 + 2*x1*x2 + 2*x1*x3 p(u22#) = x3^2 p(u31#) = 3 + x1 + 2*x1*x2 + 2*x1*x3 + x1^2 p(u32#) = x1 + 2*x1*x2 + x1*x3 + 2*x2*x3 + 2*x3 p(u41#) = 2*x1 p(u42#) = 2 + x1 + 2*x2 + 2*x2^2 p(c_1) = x1 + x2 p(c_2) = x1 + x2 p(c_3) = x1 + x2 p(c_4) = 1 + x1 p(c_5) = 0 p(c_6) = x1 p(c_7) = 0 p(c_8) = x1 p(c_9) = 1 Following rules are strictly oriented: din#(der(times(X,Y))) = 5 + 2*X > 4 + 2*X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = 1 + 2*X >= 1 + 2*X = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = 1 + 2*X >= 1 + 2*X = c_2(u21#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 2 + 2*DX + 2*DX*X + 2*DX*Y + 2*X + 2*Y >= 2 + 2*Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 5 + 3*DX + 2*DX*X + 2*DX*Y + DX^2 + 2*X + 2*Y >= 1 + 2*Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 2*DX >= 1 + 2*DX = c_8(din#(der(DX))) din(der(der(X))) = 0 >= 0 = u41(din(der(X)),X) din(der(plus(X,Y))) = 0 >= 0 = u21(din(der(X)),X,Y) din(der(times(X,Y))) = 0 >= 0 = u31(din(der(X)),X,Y) u21(dout(DX),X,Y) = 4 + 6*DX + 2*DX*X + 3*DX*Y + 2*DX^2 + 2*X + 3*Y >= DX + 2*DX*X + DX^2 + 3*Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 4 + DX + 2*DX*X + DX^2 + 6*DY + 3*DY*X + 2*DY^2 + 3*X + 3*Y >= 1 + DX = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 2 + 4*DX + 3*DX*Y + 2*DX^2 + 3*Y >= DX*Y + 3*Y = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 3 + DX*Y + 5*DY + DY*X + 2*DY*Y + 2*DY^2 + X + 5*Y >= 3 + X = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 1 + 2*DX + 2*DX*X + DX^2 + 2*X >= 1 + DX + DX*X + 2*X = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 5 + 6*DDX + 2*DDX*X + 2*DDX^2 + DX + DX*X + 4*X >= 1 + DDX = dout(DDX) **** Step 5.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 5.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) Consider the set of all dependency pairs 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 4: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) 5: u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) 6: u41#(dout(DX),X) -> c_8(din#(der(DX))) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {2} These cover all (indirect) predecessors of dependency pairs {2,4} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ***** Step 5.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#} TcT has computed the following interpretation: p(der) = x1 p(din) = 0 p(dout) = 1 + x1 p(plus) = 2 + x1 p(times) = 2 + x1 p(u21) = x1 + 3*x1*x2 + 2*x1*x3 + 3*x1^2 p(u22) = 3 + x1*x2 + 3*x1*x3 + 3*x1*x4 + 3*x2 + 3*x2*x4 + x3 + x3*x4 + 3*x4 p(u31) = 2*x1*x2 + x1^2 p(u32) = 1 + 3*x1 + x1^2 + 2*x2 + 2*x4 p(u41) = 3*x1*x2 p(u42) = x1 + x1*x2 + 3*x1^2 + 3*x2 p(din#) = 3*x1 p(u21#) = 2*x1 + 3*x1*x3 + x1^2 p(u22#) = 2*x4 + x4^2 p(u31#) = 3 + 3*x1*x3 p(u32#) = x2^2 p(u41#) = 2*x1^2 p(u42#) = 1 + x1^2 + x2^2 + 2*x3^2 p(c_1) = x1 + x2 p(c_2) = x1 + x2 p(c_3) = 3 + x1 + x2 p(c_4) = 3 + x1 p(c_5) = 1 p(c_6) = x1 p(c_7) = 0 p(c_8) = x1 p(c_9) = 0 Following rules are strictly oriented: din#(der(plus(X,Y))) = 6 + 3*X > 3*X = c_2(u21#(din(der(X)),X,Y),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = 3*X >= 3*X = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(times(X,Y))) = 6 + 3*X >= 6 + 3*X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 3 + 4*DX + 3*DX*Y + DX^2 + 3*Y >= 3 + 3*Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 3 + 3*DX*Y + 3*Y >= 3*Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2 >= 3*DX = c_8(din#(der(DX))) din(der(der(X))) = 0 >= 0 = u41(din(der(X)),X) din(der(plus(X,Y))) = 0 >= 0 = u21(din(der(X)),X,Y) din(der(times(X,Y))) = 0 >= 0 = u31(din(der(X)),X,Y) u21(dout(DX),X,Y) = 4 + 7*DX + 3*DX*X + 2*DX*Y + 3*DX^2 + 3*X + 2*Y >= 3 + 3*DX + 3*DX*X + DX*Y + 3*X + Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 3 + 6*DX + 3*DX*DY + 3*DX*X + DX*Y + DY*X + 3*DY*Y + 4*X + 4*Y >= 3 + DX = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 1 + 2*DX + 2*DX*X + DX^2 + 2*X >= 1 + 2*DX + 2*X = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 5 + 2*DX + 5*DY + DY^2 + 2*X >= 5 + X = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 3*DX*X + 3*X >= 3*X = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 4 + 7*DDX + DDX*X + 3*DDX^2 + 4*X >= 1 + DDX = dout(DDX) ***** Step 5.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 5.b:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) Consider the set of all dependency pairs 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 4: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) 5: u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) 6: u41#(dout(DX),X) -> c_8(din#(der(DX))) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,6} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ****** Step 5.b:1.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1} Following symbols are considered usable: {din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#} TcT has computed the following interpretation: p(der) = 1 + x1 p(din) = 0 p(dout) = 2 + x1 p(plus) = 1 + x1 p(times) = x1 + x2 p(u21) = 3*x1 p(u22) = 3 + 3*x4 p(u31) = x1^2 p(u32) = 3*x1 + x1*x2 + x4 p(u41) = 2*x1 + x1*x2 p(u42) = x1 + x2*x3 + 2*x3 p(din#) = 3*x1 p(u21#) = 2 + 2*x1 + 2*x1*x3 p(u22#) = 2*x1 + x1*x3 + 2*x1^2 + 2*x2^2 p(u31#) = 2*x1 + 2*x1*x3 p(u32#) = 1 + 2*x1 + 2*x1*x2 + x2 + x4 p(u41#) = x1^2 p(u42#) = 2 + x1*x2 + 2*x1*x3 + 2*x1^2 + x2 + x3 p(c_1) = 1 + x1 + x2 p(c_2) = 1 + x1 + x2 p(c_3) = x1 + x2 p(c_4) = x1 p(c_5) = 0 p(c_6) = 1 + x1 p(c_7) = 0 p(c_8) = 1 + x1 p(c_9) = 1 Following rules are strictly oriented: din#(der(der(X))) = 6 + 3*X > 4 + 3*X = c_1(u41#(din(der(X)),X),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(plus(X,Y))) = 6 + 3*X >= 6 + 3*X = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = 3 + 3*X + 3*Y >= 3 + 3*X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 6 + 2*DX + 2*DX*Y + 4*Y >= 3 + 3*Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 4 + 2*DX + 2*DX*Y + 4*Y >= 4 + 3*Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 4 + 4*DX + DX^2 >= 4 + 3*DX = c_8(din#(der(DX))) din(der(der(X))) = 0 >= 0 = u41(din(der(X)),X) din(der(plus(X,Y))) = 0 >= 0 = u21(din(der(X)),X,Y) din(der(times(X,Y))) = 0 >= 0 = u31(din(der(X)),X,Y) u21(dout(DX),X,Y) = 6 + 3*DX >= 3 + 3*DX = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 3 + 3*DX >= 3 + DX = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 4 + 4*DX + DX^2 >= DX = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 6 + DX + 3*DY + DY*X + 2*X >= 3 + DY + X = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 4 + 2*DX + DX*X + 2*X >= 2*DX + DX*X = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 2 + DDX + 2*DX + DX*X >= 2 + DDX = dout(DDX) ****** Step 5.b:1.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 5.b:1.b:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) -->_1 u41#(dout(DX),X) -> c_8(din#(der(DX))):6 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 2:W:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) -->_1 u21#(dout(DX),X,Y) -> c_4(din#(der(Y))):4 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 3:W:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) -->_1 u31#(dout(DX),X,Y) -> c_6(din#(der(Y))):5 -->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 4:W:u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) -->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 5:W:u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) -->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 6:W:u41#(dout(DX),X) -> c_8(din#(der(DX))) -->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3 -->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2 -->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))) 6: u41#(dout(DX),X) -> c_8(din#(der(DX))) 5: u31#(dout(DX),X,Y) -> c_6(din#(der(Y))) 3: din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 4: u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) 2: din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))) ****** Step 5.b:1.b:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 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) u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX) 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) - Signature: {din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1 ,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der ,dout,plus,times} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))