WORST_CASE(?,O(n^1))
* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+Full,f,goal,map} and constructors {+,0,Cons,Nil,S}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
+Full#(0(),y) -> c_1()
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
f#(x) -> c_3(*#(x,x))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
map#(Nil()) -> c_6()
Weak DPs
*#(x,0()) -> c_7()
*#(x,S(0())) -> c_8()
*#(x,S(S(y))) -> c_9(*#(x,S(y)))
*#(0(),y) -> c_10()
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(0(),y) -> c_1()
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
f#(x) -> c_3(*#(x,x))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
map#(Nil()) -> c_6()
- Weak DPs:
*#(x,0()) -> c_7()
*#(x,S(0())) -> c_8()
*#(x,S(S(y))) -> c_9(*#(x,S(y)))
*#(0(),y) -> c_10()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,3,6}
by application of
Pre({1,3,6}) = {2,4,5}.
Here rules are labelled as follows:
1: +Full#(0(),y) -> c_1()
2: +Full#(S(x),y) -> c_2(+Full#(x,S(y)))
3: f#(x) -> c_3(*#(x,x))
4: goal#(xs) -> c_4(map#(xs))
5: map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
6: map#(Nil()) -> c_6()
7: *#(x,0()) -> c_7()
8: *#(x,S(0())) -> c_8()
9: *#(x,S(S(y))) -> c_9(*#(x,S(y)))
10: *#(0(),y) -> c_10()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
- Weak DPs:
*#(x,0()) -> c_7()
*#(x,S(0())) -> c_8()
*#(x,S(S(y))) -> c_9(*#(x,S(y)))
*#(0(),y) -> c_10()
+Full#(0(),y) -> c_1()
f#(x) -> c_3(*#(x,x))
map#(Nil()) -> c_6()
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
-->_1 +Full#(0(),y) -> c_1():8
-->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
2:S:goal#(xs) -> c_4(map#(xs))
-->_1 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
-->_1 map#(Nil()) -> c_6():10
3:S:map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
-->_1 f#(x) -> c_3(*#(x,x)):9
-->_2 map#(Nil()) -> c_6():10
-->_2 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
4:W:*#(x,0()) -> c_7()
5:W:*#(x,S(0())) -> c_8()
6:W:*#(x,S(S(y))) -> c_9(*#(x,S(y)))
-->_1 *#(0(),y) -> c_10():7
-->_1 *#(x,S(S(y))) -> c_9(*#(x,S(y))):6
-->_1 *#(x,S(0())) -> c_8():5
7:W:*#(0(),y) -> c_10()
8:W:+Full#(0(),y) -> c_1()
9:W:f#(x) -> c_3(*#(x,x))
-->_1 *#(0(),y) -> c_10():7
-->_1 *#(x,S(S(y))) -> c_9(*#(x,S(y))):6
-->_1 *#(x,S(0())) -> c_8():5
-->_1 *#(x,0()) -> c_7():4
10:W:map#(Nil()) -> c_6()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
10: map#(Nil()) -> c_6()
9: f#(x) -> c_3(*#(x,x))
4: *#(x,0()) -> c_7()
6: *#(x,S(S(y))) -> c_9(*#(x,S(y)))
5: *#(x,S(0())) -> c_8()
7: *#(0(),y) -> c_10()
8: +Full#(0(),y) -> c_1()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
-->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
2:S:goal#(xs) -> c_4(map#(xs))
-->_1 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
3:S:map#(Cons(x,xs)) -> c_5(f#(x),map#(xs))
-->_2 map#(Cons(x,xs)) -> c_5(f#(x),map#(xs)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
map#(Cons(x,xs)) -> c_5(map#(xs))
* Step 5: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(map#(xs))
- Weak TRS:
*(x,0()) -> 0()
*(x,S(0())) -> x
*(x,S(S(y))) -> +(x,*(x,S(y)))
*(0(),y) -> 0()
+Full(0(),y) -> y
+Full(S(x),y) -> +Full(x,S(y))
f(x) -> *(x,x)
goal(xs) -> map(xs)
map(Cons(x,xs)) -> Cons(f(x),map(xs))
map(Nil()) -> Nil()
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(map#(xs))
* Step 6: RemoveHeads WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
goal#(xs) -> c_4(map#(xs))
map#(Cons(x,xs)) -> c_5(map#(xs))
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
-->_1 +Full#(S(x),y) -> c_2(+Full#(x,S(y))):1
2:S:goal#(xs) -> c_4(map#(xs))
-->_1 map#(Cons(x,xs)) -> c_5(map#(xs)):3
3:S:map#(Cons(x,xs)) -> c_5(map#(xs))
-->_1 map#(Cons(x,xs)) -> c_5(map#(xs)):3
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(2,goal#(xs) -> c_4(map#(xs)))]
* Step 7: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
map#(Cons(x,xs)) -> c_5(map#(xs))
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_5) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = [0]
p(+) = [1] x1 + [1] x2 + [0]
p(+Full) = [0]
p(0) = [0]
p(Cons) = [1] x1 + [1] x2 + [1]
p(Nil) = [0]
p(S) = [1] x1 + [0]
p(f) = [0]
p(goal) = [0]
p(map) = [0]
p(*#) = [0]
p(+Full#) = [0]
p(f#) = [0]
p(goal#) = [0]
p(map#) = [9] x1 + [0]
p(c_1) = [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
Following rules are strictly oriented:
map#(Cons(x,xs)) = [9] x + [9] xs + [9]
> [9] xs + [0]
= c_5(map#(xs))
Following rules are (at-least) weakly oriented:
+Full#(S(x),y) = [0]
>= [0]
= c_2(+Full#(x,S(y)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
- Weak DPs:
map#(Cons(x,xs)) -> c_5(map#(xs))
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_5) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = [0]
p(+) = [1] x1 + [1] x2 + [0]
p(+Full) = [0]
p(0) = [1]
p(Cons) = [1] x1 + [1] x2 + [0]
p(Nil) = [0]
p(S) = [1] x1 + [3]
p(f) = [0]
p(goal) = [0]
p(map) = [0]
p(*#) = [0]
p(+Full#) = [9] x1 + [0]
p(f#) = [0]
p(goal#) = [0]
p(map#) = [2] x1 + [0]
p(c_1) = [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
Following rules are strictly oriented:
+Full#(S(x),y) = [9] x + [27]
> [9] x + [0]
= c_2(+Full#(x,S(y)))
Following rules are (at-least) weakly oriented:
map#(Cons(x,xs)) = [2] x + [2] xs + [0]
>= [2] xs + [0]
= c_5(map#(xs))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
+Full#(S(x),y) -> c_2(+Full#(x,S(y)))
map#(Cons(x,xs)) -> c_5(map#(xs))
- Signature:
{*/2,+Full/2,f/1,goal/1,map/1,*#/2,+Full#/2,f#/1,goal#/1,map#/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c_1/0,c_2/1
,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+Full#,f#,goal#,map#} and constructors {+,0,Cons,Nil
,S}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))