WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/0} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,sqr,terms} and constructors {0,cons,nil ,recip,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/0} - 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 add#(0(),X) -> c_1() add#(s(),Y) -> c_2() 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: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: add#(0(),X) -> c_1() add#(s(),Y) -> c_2() 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: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,cons/1,nil/0,recip/1,s/0 ,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: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,5,6,7,8} by application of Pre({1,2,3,4,5,6,7,8}) = {9}. Here rules are labelled as follows: 1: add#(0(),X) -> c_1() 2: add#(s(),Y) -> c_2() 3: dbl#(0()) -> c_3() 4: dbl#(s()) -> c_4() 5: first#(0(),X) -> c_5() 6: first#(s(),cons(Y)) -> c_6() 7: sqr#(0()) -> c_7() 8: sqr#(s()) -> c_8() 9: terms#(N) -> c_9(sqr#(N)) * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: terms#(N) -> c_9(sqr#(N)) - Weak DPs: add#(0(),X) -> c_1() add#(s(),Y) -> c_2() 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() - Weak TRS: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,cons/1,nil/0,recip/1,s/0 ,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: 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: terms#(N) -> c_9(sqr#(N)) 2: add#(0(),X) -> c_1() 3: add#(s(),Y) -> c_2() 4: dbl#(0()) -> c_3() 5: dbl#(s()) -> c_4() 6: first#(0(),X) -> c_5() 7: first#(s(),cons(Y)) -> c_6() 8: sqr#(0()) -> c_7() 9: sqr#(s()) -> c_8() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: add#(0(),X) -> c_1() add#(s(),Y) -> c_2() 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: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,cons/1,nil/0,recip/1,s/0 ,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:add#(0(),X) -> c_1() 2:W:add#(s(),Y) -> c_2() 3:W:dbl#(0()) -> c_3() 4:W:dbl#(s()) -> c_4() 5:W:first#(0(),X) -> c_5() 6:W:first#(s(),cons(Y)) -> c_6() 7:W:sqr#(0()) -> c_7() 8:W:sqr#(s()) -> c_8() 9:W:terms#(N) -> c_9(sqr#(N)) -->_1 sqr#(s()) -> c_8():8 -->_1 sqr#(0()) -> c_7():7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: terms#(N) -> c_9(sqr#(N)) 8: sqr#(s()) -> c_8() 7: sqr#(0()) -> c_7() 6: first#(s(),cons(Y)) -> c_6() 5: first#(0(),X) -> c_5() 4: dbl#(s()) -> c_4() 3: dbl#(0()) -> c_3() 2: add#(s(),Y) -> c_2() 1: add#(0(),X) -> c_1() * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: add(0(),X) -> X add(s(),Y) -> s() 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: {add/2,dbl/1,first/2,sqr/1,terms/1,add#/2,dbl#/1,first#/2,sqr#/1,terms#/1} / {0/0,cons/1,nil/0,recip/1,s/0 ,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))