WORST_CASE(?,O(n^1)) * Step 1: Ara WORST_CASE(?,O(n^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: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(14) 0 :: [] -(0)-> A(15) add :: [A(0) x A(12)] -(9)-> A(0) cons :: [A(0)] -(0)-> A(0) cons :: [A(0)] -(0)-> A(12) cons :: [A(0)] -(0)-> A(6) dbl :: [A(0)] -(16)-> A(0) first :: [A(0) x A(0)] -(8)-> A(1) nil :: [] -(0)-> A(1) recip :: [A(12)] -(0)-> A(12) s :: [] -(0)-> A(0) s :: [] -(0)-> A(14) s :: [] -(0)-> A(4) sqr :: [A(0)] -(3)-> A(13) terms :: [A(14)] -(14)-> A(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0)] -(0)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(1)] -(0)-> A(1) s_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - 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} Following problems could not be solved: - 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} WORST_CASE(?,O(n^1))