```* 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))
```