* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2} / {0/0,s/1,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11,U12,U21,U22,activate,plus,x} and constructors {0,s
,tt}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2} / {0/0,s/1,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11,U12,U21,U22,activate,plus,x} and constructors {0,s
,tt}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
activate#(X) -> c_5()
plus#(N,0()) -> c_6()
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,0()) -> c_8()
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
Weak DPs
and mark the set of starting terms.
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
activate#(X) -> c_5()
plus#(N,0()) -> c_6()
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,0()) -> c_8()
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/3,c_2/3,c_3/3,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{5,6,8}
by application of
Pre({5,6,8}) = {1,2,3,4}.
Here rules are labelled as follows:
1: U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
2: U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
3: U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
4: U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
5: activate#(X) -> c_5()
6: plus#(N,0()) -> c_6()
7: plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
8: x#(N,0()) -> c_8()
9: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak DPs:
activate#(X) -> c_5()
plus#(N,0()) -> c_6()
x#(N,0()) -> c_8()
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/3,c_2/3,c_3/3,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
-->_1 U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M)):2
-->_3 activate#(X) -> c_5():7
-->_2 activate#(X) -> c_5():7
2:S:U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
-->_1 plus#(N,0()) -> c_6():8
-->_3 activate#(X) -> c_5():7
-->_2 activate#(X) -> c_5():7
3:S:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
-->_1 U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N)):4
-->_3 activate#(X) -> c_5():7
-->_2 activate#(X) -> c_5():7
4:S:U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
-->_2 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):6
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
-->_2 x#(N,0()) -> c_8():9
-->_1 plus#(N,0()) -> c_6():8
-->_5 activate#(X) -> c_5():7
-->_4 activate#(X) -> c_5():7
-->_3 activate#(X) -> c_5():7
5:S:plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
-->_1 U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N)):1
6:S:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N)):3
7:W:activate#(X) -> c_5()
8:W:plus#(N,0()) -> c_6()
9:W:x#(N,0()) -> c_8()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: x#(N,0()) -> c_8()
7: activate#(X) -> c_5()
8: plus#(N,0()) -> c_6()
* Step 5: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/3,c_2/3,c_3/3,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
-->_1 U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M)):2
2:S:U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)),activate#(N),activate#(M))
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
3:S:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N))
-->_1 U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N)):4
4:S:U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N))
,x#(activate(N),activate(M))
,activate#(N)
,activate#(M)
,activate#(N))
-->_2 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):6
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
5:S:plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
-->_1 U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)),activate#(M),activate#(N)):1
6:S:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)),activate#(M),activate#(N)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
* Step 6: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
- Weak DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2
,x#/2} / {0/0,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
Problem (S)
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2
,x#/2} / {0/0,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
** Step 6.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
- Weak DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ 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:
5: plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
Consider the set of all dependency pairs
1: U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
2: U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
3: U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
4: U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
5: plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
6: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
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
{5}
These cover all (indirect) predecessors of dependency pairs
{1,2,5}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** Step 6.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
- Weak DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ 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},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1,2},
uargs(c_7) = {1},
uargs(c_9) = {1}
Following symbols are considered usable:
{activate,U11#,U12#,U21#,U22#,activate#,plus#,x#}
TcT has computed the following interpretation:
p(0) = 0
p(U11) = 0
p(U12) = x2*x3 + x3^2
p(U21) = x3^2
p(U22) = 1 + x2^2
p(activate) = x1
p(plus) = 1 + x1 + x1*x2 + x2 + x2^2
p(s) = 1 + x1
p(tt) = 1
p(x) = 0
p(U11#) = 1 + x2
p(U12#) = 1 + x1*x2
p(U21#) = 1 + x1*x3 + x2 + x2*x3 + x3 + x3^2
p(U22#) = 1 + x1*x2 + x1*x3 + x2*x3 + x3 + x3^2
p(activate#) = 0
p(plus#) = 1 + x2
p(x#) = x1 + x1*x2 + x1^2 + x2
p(c_1) = x1
p(c_2) = x1
p(c_3) = x1
p(c_4) = x1 + x2
p(c_5) = 0
p(c_6) = 0
p(c_7) = x1
p(c_8) = 0
p(c_9) = x1
Following rules are strictly oriented:
plus#(N,s(M)) = 2 + M
> 1 + M
= c_7(U11#(tt(),M,N))
Following rules are (at-least) weakly oriented:
U11#(tt(),M,N) = 1 + M
>= 1 + M
= c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) = 1 + M
>= 1 + M
= c_2(plus#(activate(N),activate(M)))
U21#(tt(),M,N) = 1 + M + M*N + 2*N + N^2
>= 1 + M + M*N + 2*N + N^2
= c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) = 1 + M + M*N + 2*N + N^2
>= 1 + M + M*N + 2*N + N^2
= c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) = 1 + M + M*N + 2*N + N^2
>= 1 + M + M*N + 2*N + N^2
= c_9(U21#(tt(),M,N))
activate(X) = X
>= X
= X
*** Step 6.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
- Weak DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 6.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
-->_1 U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M))):2
2:W:U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
3:W:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
-->_1 U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M))):4
4:W:U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
-->_2 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):6
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):5
5:W:plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
-->_1 U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N))):1
6:W:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N))):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
6: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
4: U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
1: U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
5: plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
2: U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
*** Step 6.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 6.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak DPs:
U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
-->_1 U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M))):2
2:S:U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):6
-->_2 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):3
3:S:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N))):1
4:W:U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
-->_1 U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M))):5
5:W:U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
-->_1 plus#(N,s(M)) -> c_7(U11#(tt(),M,N)):6
6:W:plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
-->_1 U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N))):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
6: plus#(N,s(M)) -> c_7(U11#(tt(),M,N))
5: U12#(tt(),M,N) -> c_2(plus#(activate(N),activate(M)))
4: U11#(tt(),M,N) -> c_1(U12#(tt(),activate(M),activate(N)))
** Step 6.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
-->_1 U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M))):2
2:S:U22#(tt(),M,N) -> c_4(plus#(x(activate(N),activate(M)),activate(N)),x#(activate(N),activate(M)))
-->_2 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):3
3:S:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N))):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
** Step 6.b:3: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
U11(tt(),M,N) -> U12(tt(),activate(M),activate(N))
U12(tt(),M,N) -> s(plus(activate(N),activate(M)))
U21(tt(),M,N) -> U22(tt(),activate(M),activate(N))
U22(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
activate(X) -> X
plus(N,0()) -> N
plus(N,s(M)) -> U11(tt(),M,N)
x(N,0()) -> 0()
x(N,s(M)) -> U21(tt(),M,N)
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
activate(X) -> X
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
** Step 6.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
activate(X) -> X
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ 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:
2: U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
3: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
Consider the set of all dependency pairs
1: U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
2: U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
3: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{2,3}
These cover all (indirect) predecessors of dependency pairs
{1,2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** Step 6.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
activate(X) -> X
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ 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_3) = {1},
uargs(c_4) = {1},
uargs(c_9) = {1}
Following symbols are considered usable:
{activate,U11#,U12#,U21#,U22#,activate#,plus#,x#}
TcT has computed the following interpretation:
p(0) = [1]
p(U11) = [1] x3 + [1]
p(U12) = [2] x3 + [1]
p(U21) = [1] x1 + [8] x3 + [1]
p(U22) = [1] x2 + [1]
p(activate) = [1] x1 + [0]
p(plus) = [1] x1 + [1]
p(s) = [1] x1 + [2]
p(tt) = [8]
p(x) = [1] x1 + [0]
p(U11#) = [0]
p(U12#) = [1] x1 + [2] x2 + [8] x3 + [1]
p(U21#) = [2] x1 + [8] x2 + [7]
p(U22#) = [1] x1 + [8] x2 + [11]
p(activate#) = [0]
p(plus#) = [1] x1 + [4]
p(x#) = [8] x2 + [12]
p(c_1) = [8] x1 + [2]
p(c_2) = [2]
p(c_3) = [1] x1 + [4]
p(c_4) = [1] x1 + [4]
p(c_5) = [0]
p(c_6) = [2]
p(c_7) = [1] x1 + [0]
p(c_8) = [0]
p(c_9) = [1] x1 + [4]
Following rules are strictly oriented:
U22#(tt(),M,N) = [8] M + [19]
> [8] M + [16]
= c_4(x#(activate(N),activate(M)))
x#(N,s(M)) = [8] M + [28]
> [8] M + [27]
= c_9(U21#(tt(),M,N))
Following rules are (at-least) weakly oriented:
U21#(tt(),M,N) = [8] M + [23]
>= [8] M + [23]
= c_3(U22#(tt(),activate(M),activate(N)))
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
*** Step 6.b:4.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
- Weak DPs:
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
activate(X) -> X
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 6.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
x#(N,s(M)) -> c_9(U21#(tt(),M,N))
- Weak TRS:
activate(X) -> X
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
-->_1 U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M))):2
2:W:U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
-->_1 x#(N,s(M)) -> c_9(U21#(tt(),M,N)):3
3:W:x#(N,s(M)) -> c_9(U21#(tt(),M,N))
-->_1 U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: U21#(tt(),M,N) -> c_3(U22#(tt(),activate(M),activate(N)))
3: x#(N,s(M)) -> c_9(U21#(tt(),M,N))
2: U22#(tt(),M,N) -> c_4(x#(activate(N),activate(M)))
*** Step 6.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
activate(X) -> X
- Signature:
{U11/3,U12/3,U21/3,U22/3,activate/1,plus/2,x/2,U11#/3,U12#/3,U21#/3,U22#/3,activate#/1,plus#/2,x#/2} / {0/0
,s/1,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {U11#,U12#,U21#,U22#,activate#,plus#
,x#} and constructors {0,s,tt}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))