```* Step 1: ToInnermost WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
dbl(0()) -> 0()
dbl(s()) -> s()
first(0(),X) -> nil()
first(s(),cons(Y)) -> cons(Y)
sqr(0()) -> 0()
sqr(s()) -> s()
terms(N) -> cons(recip(sqr(N)))
- Signature:
- Obligation:
runtime complexity wrt. defined symbols {add,dbl,first,sqr,terms} and constructors {0,cons,nil,recip,s}
+ Applied Processor:
ToInnermost
+ Details:
switch to innermost, as the system is overlay and right linear and does not contain weak rules
* Step 2: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
dbl(0()) -> 0()
dbl(s()) -> s()
first(0(),X) -> nil()
first(s(),cons(Y)) -> cons(Y)
sqr(0()) -> 0()
sqr(s()) -> s()
terms(N) -> cons(recip(sqr(N)))
- Signature:
- Obligation:
innermost runtime complexity wrt. defined symbols {add,dbl,first,sqr,terms} and constructors {0,cons,nil
,recip,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:

Strict DPs
dbl#(0()) -> c_3()
dbl#(s()) -> c_4()
first#(0(),X) -> c_5()
first#(s(),cons(Y)) -> c_6()
sqr#(0()) -> c_7()
sqr#(s()) -> c_8()
terms#(N) -> c_9(sqr#(N))
Weak DPs

and mark the set of starting terms.
* Step 3: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
dbl#(0()) -> c_3()
dbl#(s()) -> c_4()
first#(0(),X) -> c_5()
first#(s(),cons(Y)) -> c_6()
sqr#(0()) -> c_7()
sqr#(s()) -> c_8()
terms#(N) -> c_9(sqr#(N))
- Weak TRS:
dbl(0()) -> 0()
dbl(s()) -> s()
first(0(),X) -> nil()
first(s(),cons(Y)) -> cons(Y)
sqr(0()) -> 0()
sqr(s()) -> s()
terms(N) -> cons(recip(sqr(N)))
- Signature:
,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#,dbl#,first#,sqr#,terms#} and constructors {0,cons
,nil,recip,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
dbl#(0()) -> c_3()
dbl#(s()) -> c_4()
first#(0(),X) -> c_5()
first#(s(),cons(Y)) -> c_6()
sqr#(0()) -> c_7()
sqr#(s()) -> c_8()
terms#(N) -> c_9(sqr#(N))
* Step 4: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
dbl#(0()) -> c_3()
dbl#(s()) -> c_4()
first#(0(),X) -> c_5()
first#(s(),cons(Y)) -> c_6()
sqr#(0()) -> c_7()
sqr#(s()) -> c_8()
terms#(N) -> c_9(sqr#(N))
- Signature:
,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#,dbl#,first#,sqr#,terms#} and constructors {0,cons
,nil,recip,s}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph

3:S:dbl#(0()) -> c_3()

4:S:dbl#(s()) -> c_4()

5:S:first#(0(),X) -> c_5()

6:S:first#(s(),cons(Y)) -> c_6()

7:S:sqr#(0()) -> c_7()

8:S:sqr#(s()) -> c_8()

9:S:terms#(N) -> c_9(sqr#(N))
-->_1 sqr#(s()) -> c_8():8
-->_1 sqr#(0()) -> c_7():7

The dependency graph contains no loops, we remove all dependency pairs.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:

- Signature:
,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#,dbl#,first#,sqr#,terms#} and constructors {0,cons
,nil,recip,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(1))
```