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