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: 5: u31#(dout(DX),X,Y) -> c_6(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) = [1] p(din) = [0] p(dout) = [2] p(plus) = [1] x1 + [1] x2 + [0] p(times) = [0] p(u21) = [4] x1 + [0] p(u22) = [3] p(u31) = [0] p(u32) = [2] x1 + [0] p(u41) = [2] x1 + [0] p(u42) = [4] p(din#) = [5] x1 + [3] p(u21#) = [4] x1 + [0] p(u22#) = [0] p(u31#) = [5] x1 + [0] p(u32#) = [4] x3 + [0] p(u41#) = [4] x1 + [0] p(u42#) = [2] x1 + [1] x2 + [1] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [4] x1 + [1] x2 + [0] p(c_3) = [4] x1 + [1] x2 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] 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) = [10] > [8] = c_6(din#(der(Y))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = [8] >= [8] = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = [8] >= [8] = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = [8] >= [8] = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = [8] >= [8] = c_4(din#(der(Y))) u41#(dout(DX),X) = [8] >= [8] = 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) = [8] >= [3] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [3] >= [2] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [0] >= [0] = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = [4] >= [2] = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = [4] >= [4] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [4] >= [2] = 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))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u31#(dout(DX),X,Y) -> c_6(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))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u31#(dout(DX),X,Y) -> c_6(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: 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))) u21#(dout(DX),X,Y) -> c_4(din#(der(Y))) u41#(dout(DX),X) -> c_8(din#(der(DX))) - Weak DPs: u31#(dout(DX),X,Y) -> c_6(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) = [1] p(plus) = [1] x2 + [2] p(times) = [1] x1 + [2] p(u21) = [0] p(u22) = [5] x1 + [0] p(u31) = [1] x1 + [0] p(u32) = [1] p(u41) = [2] x1 + [0] p(u42) = [2] x1 + [2] p(din#) = [0] p(u21#) = [0] p(u22#) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(u31#) = [0] p(u32#) = [1] x2 + [1] p(u41#) = [7] x1 + [0] p(u42#) = [0] p(c_1) = [1] x1 + [2] x2 + [0] p(c_2) = [1] x1 + [1] x2 + [0] p(c_3) = [2] x1 + [1] x2 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [2] x1 + [0] p(c_7) = [4] p(c_8) = [2] x1 + [6] p(c_9) = [1] Following rules are strictly oriented: u41#(dout(DX),X) = [7] > [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) = [0] >= [0] = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = [0] >= [0] = c_6(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) = [0] >= [0] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [5] >= [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) = [2] >= [2] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [4] >= [1] = 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))) 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: 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))) 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: 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.b:1.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))) 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: 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) = [1] x1 + [0] p(din) = [0] p(dout) = [1] x1 + [1] p(plus) = [1] x1 + [0] p(times) = [0] p(u21) = [6] x1 + [0] p(u22) = [1] x4 + [6] p(u31) = [6] x1 + [0] p(u32) = [4] x1 + [1] x4 + [6] p(u41) = [4] x1 + [0] p(u42) = [1] x1 + [4] x3 + [2] p(din#) = [0] p(u21#) = [5] x1 + [0] p(u22#) = [1] x4 + [0] p(u31#) = [0] p(u32#) = [0] p(u41#) = [6] x1 + [0] p(u42#) = [1] x1 + [1] x3 + [1] p(c_1) = [4] x1 + [4] x2 + [0] p(c_2) = [1] x1 + [2] x2 + [0] p(c_3) = [4] x1 + [4] x2 + [0] p(c_4) = [1] x1 + [1] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [1] p(c_8) = [4] x1 + [6] p(c_9) = [0] Following rules are strictly oriented: u21#(dout(DX),X,Y) = [5] DX + [5] > [1] = 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) = [0] >= [0] = c_6(din#(der(Y))) u41#(dout(DX),X) = [6] DX + [6] >= [6] = 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] DX + [6] >= [1] DX + [6] = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = [1] DX + [6] >= [1] DX + [1] = dout(plus(DX,DY)) u31(dout(DX),X,Y) = [6] DX + [6] >= [1] DX + [6] = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = [1] DX + [4] DY + [10] >= [1] = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = [4] DX + [4] >= [4] DX + [2] = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = [1] DDX + [4] DX + [3] >= [1] DDX + [1] = 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))) 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.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: 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))) 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) = 1 + x1 + x2 p(times) = x1 + x2 p(u21) = 3*x1*x2 p(u22) = 2*x1 + 2*x1*x4 + 3*x2 p(u31) = x1*x2 + x1^2 p(u32) = x1 + x1*x2 + 2*x1*x3 + 3*x1*x4 + 3*x1^2 + x2 + x2*x4 + x4 p(u41) = 3*x1 + x1^2 p(u42) = x1 + x1^2 p(din#) = 2*x1^2 p(u21#) = 2*x1 + 2*x1*x2 + x2*x3 + 2*x3^2 p(u22#) = x1 + x1*x4 + x2 + 2*x2*x3 + 2*x4 p(u31#) = x1 + x1^2 + 2*x2*x3 + 2*x3^2 p(u32#) = x1*x4 + x4 p(u41#) = 2*x1^2 p(u42#) = 1 + x1*x3 + x2 + x2*x3 + 2*x2^2 + 2*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) = 0 p(c_6) = x1 p(c_7) = 2 p(c_8) = x1 p(c_9) = 0 Following rules are strictly oriented: din#(der(plus(X,Y))) = 2 + 4*X + 4*X*Y + 2*X^2 + 4*Y + 2*Y^2 > X*Y + 2*X^2 + 2*Y^2 = 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 >= 2*X^2 = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(times(X,Y))) = 4*X*Y + 2*X^2 + 2*Y^2 >= 2*X*Y + 2*X^2 + 2*Y^2 = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 2 + 2*DX + 2*DX*X + 2*X + X*Y + 2*Y^2 >= 2*Y^2 = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 2 + 3*DX + DX^2 + 2*X*Y + 2*Y^2 >= 2*Y^2 = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2 >= 2*DX^2 = 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) = 3*DX*X + 3*X >= 3*X = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 2 + 2*DX + 2*DX*DY + 2*DY + 3*X >= 2 + DX + DY = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 1 + 2*DX + DX*X + DX^2 + X >= DX + DX*X + X = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 4 + 4*DX + 3*DX*DY + DX*X + 7*DY + DY*X + 2*DY*Y + 3*DY^2 + 2*X + 2*Y >= 2 + DX + DY + X + Y = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 4 + 5*DX + DX^2 >= 0 = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 2 + 3*DDX + DDX^2 >= 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))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(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))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(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(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(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) 3: din#(der(plus(X,Y))) -> c_2(u21#(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,5} 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))) din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))) - Weak DPs: din#(der(plus(X,Y))) -> c_2(u21#(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 + x2 p(times) = 1 + x1 + x2 p(u21) = x1 + x1*x2 + x1^2 p(u22) = 1 + x1 + 2*x1*x4 + x1^2 + x2 + x2*x4 p(u31) = 2*x1 + 3*x1*x2 + 3*x1*x3 + 2*x1^2 p(u32) = 2 + 2*x1 + 2*x1*x4 + x1^2 + 3*x2 + 3*x2*x4 + 2*x3 + 2*x4 + 2*x4^2 p(u41) = x1*x2 + 2*x1^2 p(u42) = 2 + 3*x1 + 2*x1*x2 + x1^2 + x2*x3 p(din#) = x1^2 p(u21#) = 2*x1 + 2*x1*x2 + 2*x1*x3 + x2 + x3 + x3^2 p(u22#) = 1 + x1*x3 + x2 + 2*x2^2 + 2*x3 p(u31#) = x2 + 2*x2*x3 + 2*x3 + x3^2 p(u32#) = x1*x2 + x1*x4 + 2*x3^2 p(u41#) = 2*x1^2 p(u42#) = 2 + x1 + x2*x3 + 2*x3 + x3^2 p(c_1) = x1 + x2 p(c_2) = 2 + x1 + x2 p(c_3) = x1 + x2 p(c_4) = 1 + x1 p(c_5) = 1 p(c_6) = x1 p(c_7) = 1 p(c_8) = 1 + x1 p(c_9) = 0 Following rules are strictly oriented: din#(der(times(X,Y))) = 1 + 2*X + 2*X*Y + X^2 + 2*Y + Y^2 > X + 2*X*Y + X^2 + 2*Y + Y^2 = c_3(u31#(din(der(X)),X,Y),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(der(X))) = X^2 >= X^2 = c_1(u41#(din(der(X)),X),din#(der(X))) din#(der(plus(X,Y))) = 4 + 4*X + 2*X*Y + X^2 + 4*Y + Y^2 >= 2 + X + X^2 + Y + Y^2 = 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 + 3*X + 3*Y + Y^2 >= 1 + Y^2 = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = X + 2*X*Y + 2*Y + Y^2 >= Y^2 = c_6(din#(der(Y))) u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2 >= 1 + DX^2 = 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 + 3*DX + DX*X + DX^2 + X >= 1 + DX*X + X = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 3 + 2*DX + 2*DX*DY + DX*X + 3*DY + DY^2 + X >= 3 + DX + DY = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 4 + 6*DX + 3*DX*X + 3*DX*Y + 2*DX^2 + 3*X + 3*Y >= 2 + 2*DX + 3*DX*X + 2*DX^2 + 3*X + 2*Y = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 5 + 4*DX + 2*DX*DY + 3*DX*X + 2*DX^2 + 4*DY + DY^2 + 3*X + 2*Y >= 5 + DX + DY + X + Y = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 2 + 4*DX + DX*X + 2*DX^2 + X >= 2 + DX*X = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 6 + 5*DDX + 2*DDX*X + DDX^2 + DX*X + 2*X >= 1 + DDX = dout(DDX) ****** Step 5.b:1.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.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.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) = x1 + x2 p(times) = x1 + x2 p(u21) = x1 + 2*x1*x2 + 2*x1*x3 + x1^2 p(u22) = 2*x1*x4 + x1^2 + 2*x2 + 3*x3 + x3*x4 p(u31) = x1 + 2*x1*x2 + 2*x1*x3 p(u32) = 1 + x1 + 2*x1*x2 + 3*x1*x4 + 3*x3 p(u41) = x1 + 2*x1*x2 p(u42) = x1 + 2*x2*x3 p(din#) = 1 + x1^2 p(u21#) = 2*x1 + 2*x1*x3 + 2*x2*x3 + x3^2 p(u22#) = 2*x1*x2 + 2*x2*x3 + x2*x4 p(u31#) = x1*x3 + x1^2 + x3^2 p(u32#) = 2 + x1*x2 + 2*x1*x4 + x1^2 + x2 + 2*x2^2 + x3 + x4 + 2*x4^2 p(u41#) = 2 + 2*x1*x2 + x1^2 + 2*x2 p(u42#) = 2 + 2*x1 + 2*x3 + x3^2 p(c_1) = x1 + x2 p(c_2) = x1 + x2 p(c_3) = x1 + x2 p(c_4) = 2 + x1 p(c_5) = 0 p(c_6) = 1 + x1 p(c_7) = 0 p(c_8) = x1 p(c_9) = 1 Following rules are strictly oriented: din#(der(der(X))) = 5 + 4*X + X^2 > 4 + 4*X + X^2 = c_1(u41#(din(der(X)),X),din#(der(X))) Following rules are (at-least) weakly oriented: din#(der(plus(X,Y))) = 2 + 2*X + 2*X*Y + X^2 + 2*Y + Y^2 >= 2 + 2*X + 2*X*Y + X^2 + Y^2 = c_2(u21#(din(der(X)),X,Y),din#(der(X))) din#(der(times(X,Y))) = 2 + 2*X + 2*X*Y + X^2 + 2*Y + Y^2 >= 2 + 2*X + X^2 + Y^2 = c_3(u31#(din(der(X)),X,Y),din#(der(X))) u21#(dout(DX),X,Y) = 4 + 2*DX + 2*DX*Y + 2*X*Y + 4*Y + Y^2 >= 4 + 2*Y + Y^2 = c_4(din#(der(Y))) u31#(dout(DX),X,Y) = 4 + 4*DX + DX*Y + DX^2 + 2*Y + Y^2 >= 3 + 2*Y + Y^2 = c_6(din#(der(Y))) u41#(dout(DX),X) = 6 + 4*DX + 2*DX*X + DX^2 + 6*X >= 2 + 2*DX + DX^2 = 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 + 5*DX + 2*DX*X + 2*DX*Y + DX^2 + 4*X + 4*Y >= DX*Y + 2*X + 3*Y = u22(din(der(Y)),X,Y,DX) u22(dout(DY),X,Y,DX) = 4 + 4*DX + 2*DX*DY + DX*Y + 4*DY + DY^2 + 2*X + 3*Y >= 2 + DX + DY = dout(plus(DX,DY)) u31(dout(DX),X,Y) = 2 + DX + 2*DX*X + 2*DX*Y + 4*X + 4*Y >= 1 + 3*Y = u32(din(der(Y)),X,Y,DX) u32(dout(DY),X,Y,DX) = 3 + 6*DX + 3*DX*DY + DY + 2*DY*X + 4*X + 3*Y >= 2 + DX + DY + X + Y = dout(plus(times(X,DY),times(Y,DX))) u41(dout(DX),X) = 2 + DX + 2*DX*X + 4*X >= 2*DX*X = u42(din(der(DX)),X,DX) u42(dout(DDX),X,DX) = 2 + DDX + 2*DX*X >= 2 + DDX = dout(DDX) ******* Step 5.b:1.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.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: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))