WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum WORST_CASE(Omega(n^1),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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + 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: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: din(der(x)){x -> der(x)} = din(der(der(x))) ->^+ u41(din(der(x)),x) = C[din(der(x)) = din(der(x)){}] ** Step 1.b: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 1.b: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 1.b: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 1.b: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 1.b:5: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(u21) = {1}, uargs(u22) = {1}, uargs(u31) = {1}, uargs(u32) = {1}, uargs(u41) = {1}, uargs(u42) = {1}, uargs(u21#) = {1}, uargs(u31#) = {1}, uargs(u41#) = {1}, 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: all TcT has computed the following interpretation: p(der) = [0] p(din) = [0] p(dout) = [1] x1 + [0] p(plus) = [1] x1 + [1] x2 + [0] p(times) = [1] x2 + [0] p(u21) = [1] x1 + [0] p(u22) = [1] x1 + [1] x4 + [0] p(u31) = [1] x1 + [0] p(u32) = [1] x1 + [1] x4 + [0] p(u41) = [1] x1 + [0] p(u42) = [1] x1 + [1] x3 + [0] p(din#) = [0] p(u21#) = [1] x1 + [0] p(u22#) = [1] x1 + [1] x2 + [2] x4 + [0] p(u31#) = [1] x1 + [1] p(u32#) = [2] x2 + [2] x4 + [2] p(u41#) = [1] x1 + [6] p(u42#) = [1] x1 + [1] x2 + [2] p(c_1) = [1] x1 + [1] x2 + [1] p(c_2) = [1] x1 + [1] x2 + [4] p(c_3) = [1] x1 + [1] x2 + [3] p(c_4) = [1] x1 + [0] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [1] p(c_8) = [1] x1 + [0] p(c_9) = [0] Following rules are strictly oriented: u31#(dout(DX),X,Y) = [1] DX + [1] > [0] = c_6(din#(der(Y))) u41#(dout(DX),X) = [1] DX + [6] > [0] = c_8(din#(der(DX))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = [0] >= [7] = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = [0] >= [4] = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = [0] >= [4] = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = [1] DX + [0] >= [0] = 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) = [1] DX + [0] >= [1] DX + [0] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [1] DX + [1] DY + [0] >= [1] DX + [1] DY + [0] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [1] DX + [0] >= [1] DX + [0] = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = [1] DX + [1] DY + [0] >= [1] DX + [1] DY + [0] = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = [1] DX + [0] >= [1] DX + [0] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [1] DDX + [1] DX + [0] >= [1] DDX + [0] = dout(DDX) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:6: WeightGap 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))) - Weak DPs: 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(u21) = {1}, uargs(u22) = {1}, uargs(u31) = {1}, uargs(u32) = {1}, uargs(u41) = {1}, uargs(u42) = {1}, uargs(u21#) = {1}, uargs(u31#) = {1}, uargs(u41#) = {1}, 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: all TcT has computed the following interpretation: p(der) = [0] p(din) = [0] p(dout) = [1] p(plus) = [1] x2 + [2] p(times) = [1] x1 + [1] x2 + [6] p(u21) = [1] x1 + [0] p(u22) = [1] x1 + [1] p(u31) = [1] x1 + [0] p(u32) = [1] x1 + [0] p(u41) = [1] x1 + [0] p(u42) = [1] x1 + [0] p(din#) = [1] p(u21#) = [1] x1 + [2] p(u22#) = [0] p(u31#) = [1] x1 + [4] p(u32#) = [0] p(u41#) = [1] x1 + [4] p(u42#) = [2] x3 + [1] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [1] x1 + [1] x2 + [0] p(c_3) = [1] x1 + [1] x2 + [4] p(c_4) = [1] x1 + [1] p(c_5) = [0] p(c_6) = [1] x1 + [4] p(c_7) = [0] p(c_8) = [1] x1 + [4] p(c_9) = [0] Following rules are strictly oriented: u21#(dout(DX),X,Y) = [3] > [2] = c_4(din#(der(Y))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = [1] >= [5] = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = [1] >= [3] = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = [1] >= [9] = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u31#(dout(DX),X,Y) = [5] >= [5] = c_6(din#(der(Y))) u41#(dout(DX),X) = [5] >= [5] = 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) = [1] >= [1] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [2] >= [1] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [1] >= [0] = 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) = [1] >= [1] = dout(DDX) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:7: 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 any 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 + x2 p(u21) = x1*x2 + 2*x1*x3 + 2*x1^2 p(u22) = 2 + 2*x1*x2 + 2*x1*x3 + 2*x1*x4 + 2*x1^2 + x2*x4 + x3*x4 p(u31) = 2*x1 + x1*x2 p(u32) = 2 + x1*x2 + 2*x1*x4 + 2*x1^2 + x2*x4 + 2*x4 p(u41) = 3*x1 p(u42) = 2 + 2*x1 + 3*x3 p(din#) = x1 p(u21#) = 2*x1*x2 + x1*x3 p(u22#) = x1 + x1*x2 + 2*x1*x4 + x1^2 + 2*x3 p(u31#) = x1*x3 + 2*x1^2 p(u32#) = 2*x1*x2 + 2*x1*x3 + x1*x4 + x2 + 2*x2*x3 + 2*x2^2 + x4^2 p(u41#) = 2*x1^2 p(u42#) = 1 + 2*x1 + x1*x2 + 2*x1*x3 + x1^2 + 2*x2*x3 + 2*x3^2 p(c_1) = x1 + x2 p(c_2) = x1 + x2 p(c_3) = x1 + x2 p(c_4) = x1 p(c_5) = 1 p(c_6) = 2 + x1 p(c_7) = 0 p(c_8) = x1 p(c_9) = 0 Following rules are strictly oriented: din#(der(times(X,Y))) = 2 + X + Y > X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = X >= X = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = X >= X = c_2(u21#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 2*DX*X + DX*Y + 2*X + Y >= Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 2 + 4*DX + DX*Y + 2*DX^2 + Y >= 2 + Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 4*DX + 2*DX^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) = 2 + 4*DX + DX*X + 2*DX*Y + 2*DX^2 + X + 2*Y >= 2 + DX*X + DX*Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 4 + 2*DX + 2*DX*DY + DX*X + DX*Y + 4*DY + 2*DY*X + 2*DY*Y + 2*DY^2 + 2*X + 2*Y >= 1 + DX = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 2 + 2*DX + DX*X + X >= 2 + 2*DX + DX*X = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 4 + 4*DX + 2*DX*DY + DX*X + 4*DY + DY*X + 2*DY^2 + X >= 3 + DY + X = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 3 + 3*DX >= 2 + 3*DX = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 4 + 2*DDX + 3*DX >= 1 + DDX = dout(DDX) ** Step 1.b:8: 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 any 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) = x1 p(u21) = 2*x1 + 2*x1*x2 + 2*x1*x3 + 2*x1^2 p(u22) = 1 + 2*x1 + x2*x4 + x3 + 2*x3*x4 + 3*x4 + x4^2 p(u31) = x1 + x1*x2 p(u32) = 3*x1 + x1*x4 + x2 + x4 p(u41) = x1 + x1^2 p(u42) = 3*x1*x3 + 2*x1^2 + 3*x3 + x3^2 p(din#) = 2*x1 p(u21#) = 1 + 2*x1*x3 + x1^2 p(u22#) = 1 + x1*x2 + x1^2 + x2*x3 + x4 p(u31#) = 2*x1*x3 p(u32#) = 2 + x1^2 + 2*x2^2 + x3^2 p(u41#) = 2*x1^2 p(u42#) = 2*x1 + 2*x1*x2 + x1^2 + x2 + 2*x2^2 p(c_1) = x1 + x2 p(c_2) = 1 + x1 + x2 p(c_3) = x1 + x2 p(c_4) = 2 + 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(plus(X,Y))) = 4 + 2*X > 2 + 2*X = c_2(u21#(din(der(X)),X,Y),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = 2*X >= 2*X = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(times(X,Y))) = 2*X >= 2*X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 2 + 2*DX + 2*DX*Y + DX^2 + 2*Y >= 2 + 2*Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 2*DX*Y + 2*Y >= 2*Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2 >= 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 + 2*DX*Y + 2*DX^2 + 2*X + 2*Y >= 1 + 3*DX + DX*X + 2*DX*Y + DX^2 + Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 3 + 3*DX + DX*X + 2*DX*Y + DX^2 + 2*DY + Y >= 3 + DX = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 1 + DX + DX*X + X >= DX + X = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 3 + 2*DX + DX*DY + 3*DY + X >= 3 + X = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 2 + 3*DX + DX^2 >= 3*DX + DX^2 = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 2 + 4*DDX + 3*DDX*DX + 2*DDX^2 + 6*DX + DX^2 >= 1 + DDX = dout(DDX) ** Step 1.b:9: 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 any 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) = x1 + x2 p(times) = x1 p(u21) = x1*x3 + x1^2 p(u22) = x1 + x1*x4 + 2*x3 + 3*x4 + x4^2 p(u31) = 2*x1 + 2*x1*x2 p(u32) = 1 + 2*x1 + 2*x1*x2 + x1*x3 + 3*x1*x4 p(u41) = x1^2 p(u42) = 3 + x1*x3 + x1^2 + 2*x3 p(din#) = 3 + x1 p(u21#) = 2*x1 + x3 p(u22#) = x1*x4 + x3*x4 + 2*x4^2 p(u31#) = x1*x3 + x1^2 p(u32#) = 2 + x1*x4 + 2*x1^2 + 2*x2 + 2*x3 + x3*x4 + 2*x3^2 + x4 p(u41#) = 2*x1*x2 + x1^2 p(u42#) = 2 + x1 + 2*x1*x3 + x1^2 + x2*x3 + x2^2 + 2*x3 p(c_1) = x1 + x2 p(c_2) = x1 + x2 p(c_3) = x1 + x2 p(c_4) = x1 p(c_5) = 0 p(c_6) = x1 p(c_7) = 0 p(c_8) = x1 p(c_9) = 0 Following rules are strictly oriented: din#(der(der(X))) = 5 + X > 4 + X = c_1(u41#(din(der(X)),X),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(plus(X,Y))) = 4 + X + Y >= 4 + X + Y = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = 4 + X >= 4 + X = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 4 + 2*DX + Y >= 4 + Y = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 4 + 4*DX + DX*Y + DX^2 + 2*Y >= 4 + Y = c_6(din#(der(Y))) u41#(dout(DX),X) = 4 + 4*DX + 2*DX*X + DX^2 + 4*X >= 4 + 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 + 4*DX + DX*Y + DX^2 + 2*Y >= 3*DX + DX^2 + 2*Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 2 + 5*DX + DX*DY + DX^2 + DY + 2*Y >= 2 + DX + DY = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 4 + 2*DX + 2*DX*X + 4*X >= 1 = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 5 + 6*DX + 3*DX*DY + 2*DY + 2*DY*X + DY*Y + 4*X + 2*Y >= 2 + X + Y = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 4 + 4*DX + DX^2 >= 3 + 2*DX = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 7 + 4*DDX + DDX*DX + DDX^2 + 4*DX >= 2 + DDX = dout(DDX) ** Step 1.b:10: EmptyProcessor 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))