* Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) - Signature: {plus/2,times/2} / {s/1} - Obligation: runtime complexity wrt. defined symbols {plus,times} and constructors {s} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak dependency pairs: Strict DPs plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) Weak DPs and mark the set of starting terms. * Step 2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) - Strict TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) - Signature: {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/1,c_2/1} - Obligation: runtime complexity wrt. defined symbols {plus#,times#} and constructors {s} + Applied Processor: WeightGap {wgDimension = 2, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnTrs} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(plus) = {2}, uargs(plus#) = {2}, uargs(c_1) = {1}, uargs(c_2) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(plus) = [0 1] x1 + [1 0] x2 + [0] [0 2] [0 1] [2] p(s) = [1 1] x1 + [4] [0 0] [0] p(times) = [1 1] x1 + [1 0] x2 + [5] [2 2] [2 0] [0] p(plus#) = [0 4] x1 + [1 0] x2 + [5] [1 7] [0 1] [0] p(times#) = [1 6] x1 + [2 0] x2 + [0] [0 0] [0 0] [0] p(c_1) = [1 0] x1 + [0] [0 1] [0] p(c_2) = [1 0] x1 + [0] [0 1] [0] Following rules are strictly oriented: plus#(plus(X,Y),Z) = [0 8] X + [0 4] Y + [1 0] Z + [13] [0 15] [1 7] [0 1] [14] > [0 4] X + [0 1] Y + [1 0] Z + [5] [1 7] [0 2] [0 1] [2] = c_1(plus#(X,plus(Y,Z))) plus(plus(X,Y),Z) = [0 2] X + [0 1] Y + [1 0] Z + [2] [0 4] [0 2] [0 1] [6] > [0 1] X + [0 1] Y + [1 0] Z + [0] [0 2] [0 2] [0 1] [4] = plus(X,plus(Y,Z)) times(X,s(Y)) = [1 1] X + [1 1] Y + [9] [2 2] [2 2] [8] > [1 1] X + [1 1] Y + [5] [2 2] [2 2] [2] = plus(X,times(Y,X)) Following rules are (at-least) weakly oriented: times#(X,s(Y)) = [1 6] X + [2 2] Y + [8] [0 0] [0 0] [0] >= [1 4] X + [1 1] Y + [10] [3 7] [2 2] [0] = c_2(plus#(X,times(Y,X))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) - Weak DPs: plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) - Weak TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) - Signature: {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/1,c_2/1} - Obligation: runtime complexity wrt. defined symbols {plus#,times#} and constructors {s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {}. Here rules are labelled as follows: 1: times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) 2: plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) - Weak TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) - Signature: {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/1,c_2/1} - Obligation: runtime complexity wrt. defined symbols {plus#,times#} and constructors {s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) -->_1 plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))):1 2:W:times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) -->_1 plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: times#(X,s(Y)) -> c_2(plus#(X,times(Y,X))) 1: plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z))) * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: plus(plus(X,Y),Z) -> plus(X,plus(Y,Z)) times(X,s(Y)) -> plus(X,times(Y,X)) - Signature: {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/1,c_2/1} - Obligation: runtime complexity wrt. defined symbols {plus#,times#} and constructors {s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))