* Step 1: Sum WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
*(x,0()) -> 0()
*(*(x,y),z) -> *(x,*(y,z))
*(1(),y) -> y
*(i(x),x) -> 1()
- Signature:
{*/2} / {0/0,1/0,i/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
*(x,0()) -> 0()
*(*(x,y),z) -> *(x,*(y,z))
*(1(),y) -> y
*(i(x),x) -> 1()
- Signature:
{*/2} / {0/0,1/0,i/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
*#(x,0()) -> c_1()
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(1(),y) -> c_3()
*#(i(x),x) -> c_4()
Weak DPs
and mark the set of starting terms.
* Step 3: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
*#(x,0()) -> c_1()
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(1(),y) -> c_3()
*#(i(x),x) -> c_4()
- Weak TRS:
*(x,0()) -> 0()
*(*(x,y),z) -> *(x,*(y,z))
*(1(),y) -> y
*(i(x),x) -> 1()
- Signature:
{*/2,*#/2} / {0/0,1/0,i/1,c_1/0,c_2/2,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#} and constructors {0,1,i}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
*#(x,0()) -> c_1()
*#(1(),y) -> c_3()
*#(i(x),x) -> c_4()
* Step 4: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
*#(x,0()) -> c_1()
*#(1(),y) -> c_3()
*#(i(x),x) -> c_4()
- Signature:
{*/2,*#/2} / {0/0,1/0,i/1,c_1/0,c_2/2,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#} and constructors {0,1,i}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:*#(x,0()) -> c_1()
2:S:*#(1(),y) -> c_3()
3:S:*#(i(x),x) -> c_4()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{*/2,*#/2} / {0/0,1/0,i/1,c_1/0,c_2/2,c_3/0,c_4/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#} and constructors {0,1,i}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))