WORST_CASE(?,O(n^3)) * Step 1: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(5) 0 :: [] -(0)-> A(29) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(31) add :: [A(0) x A(0)] -(2)-> A(0) cons :: [A(0)] -(27)-> A(27) cons :: [A(0)] -(31)-> A(31) cons :: [A(0)] -(3)-> A(3) dbl :: [A(0)] -(21)-> A(0) first :: [A(5) x A(27)] -(0)-> A(0) half :: [A(0)] -(16)-> A(0) nil :: [] -(0)-> A(30) recip :: [A(0)] -(1)-> A(1) s :: [A(0)] -(0)-> A(0) s :: [A(5)] -(5)-> A(5) s :: [A(29)] -(29)-> A(29) sqr :: [A(29)] -(0)-> A(0) terms :: [A(31)] -(31)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(0)] -(1)-> A(1) s_A :: [A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: half(dbl(X)) -> X half(s(0())) -> 0() 2. Weak: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) * Step 2: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Weak TRS: half(dbl(X)) -> X half(s(0())) -> 0() - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(17) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(14) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(31)] -(0)-> A(31) cons :: [A(11)] -(0)-> A(11) cons :: [A(7)] -(0)-> A(7) dbl :: [A(0)] -(0)-> A(0) first :: [A(17) x A(31)] -(15)-> A(0) half :: [A(0)] -(31)-> A(0) nil :: [] -(0)-> A(14) recip :: [A(0)] -(0)-> A(7) s :: [A(0)] -(0)-> A(0) s :: [A(0)] -(17)-> A(17) sqr :: [A(0)] -(7)-> A(0) terms :: [A(30)] -(31)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1)] -(0)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(0)] -(0)-> A(1) s_A :: [A(0)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: first(0(),X) -> nil() half(0()) -> 0() 2. Weak: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(s(X),cons(Y)) -> cons(Y) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) * Step 3: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(s(X),cons(Y)) -> cons(Y) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Weak TRS: first(0(),X) -> nil() half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(7) 0 :: [] -(0)-> A(6) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(15)] -(15)-> A(15) cons :: [A(5)] -(5)-> A(5) cons :: [A(0)] -(0)-> A(0) dbl :: [A(0)] -(15)-> A(0) first :: [A(0) x A(15)] -(13)-> A(2) half :: [A(0)] -(7)-> A(0) nil :: [] -(0)-> A(4) recip :: [A(0)] -(0)-> A(0) s :: [A(0)] -(0)-> A(0) s :: [A(15)] -(15)-> A(15) sqr :: [A(15)] -(0)-> A(0) terms :: [A(15)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(1)] -(1)-> A(1) s_A :: [A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: dbl(0()) -> 0() first(s(X),cons(Y)) -> cons(Y) 2. Weak: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) * Step 4: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Weak TRS: dbl(0()) -> 0() first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(1) 0 :: [] -(0)-> A(7) 0 :: [] -(0)-> A(6) add :: [A(0) x A(0)] -(15)-> A(0) cons :: [A(0)] -(15)-> A(15) cons :: [A(0)] -(2)-> A(2) cons :: [A(0)] -(7)-> A(7) dbl :: [A(0)] -(0)-> A(0) first :: [A(1) x A(15)] -(4)-> A(0) half :: [A(0)] -(3)-> A(0) nil :: [] -(0)-> A(6) recip :: [A(0)] -(0)-> A(2) s :: [A(0)] -(0)-> A(0) s :: [A(15)] -(15)-> A(15) s :: [A(1)] -(1)-> A(1) sqr :: [A(15)] -(0)-> A(0) terms :: [A(15)] -(12)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(0)] -(0)-> A(1) s_A :: [A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: terms(N) -> cons(recip(sqr(N))) 2. Weak: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) * Step 5: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) - Weak TRS: dbl(0()) -> 0() first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(1) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(7) 0 :: [] -(0)-> A(6) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(14)] -(14)-> A(14) cons :: [A(13)] -(13)-> A(13) cons :: [A(2)] -(2)-> A(2) dbl :: [A(0)] -(0)-> A(0) first :: [A(1) x A(14)] -(10)-> A(0) half :: [A(0)] -(0)-> A(0) nil :: [] -(0)-> A(14) recip :: [A(7)] -(0)-> A(7) s :: [A(0)] -(0)-> A(0) s :: [A(0)] -(0)-> A(1) s :: [A(0)] -(0)-> A(4) s :: [A(0)] -(0)-> A(8) s :: [A(0)] -(0)-> A(14) sqr :: [A(0)] -(4)-> A(8) terms :: [A(14)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(1)] -(0)-> A(1) s_A :: [A(0)] -(0)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: sqr(0()) -> 0() 2. Weak: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) * Step 6: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) - Weak TRS: dbl(0()) -> 0() first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0) 0 :: [] -(0)-> A(3) 0 :: [] -(0)-> A(7) add :: [A(0) x A(0)] -(5)-> A(0) cons :: [A(0)] -(15)-> A(15) cons :: [A(0)] -(3)-> A(3) cons :: [A(0)] -(0)-> A(0) dbl :: [A(0)] -(0)-> A(0) first :: [A(3) x A(15)] -(12)-> A(0) half :: [A(0)] -(2)-> A(0) nil :: [] -(0)-> A(6) recip :: [A(0)] -(3)-> A(3) s :: [A(0)] -(0)-> A(0) s :: [A(7)] -(7)-> A(7) s :: [A(3)] -(3)-> A(3) sqr :: [A(7)] -(0)-> A(0) terms :: [A(9)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) recip_A :: [A(0)] -(1)-> A(1) s_A :: [A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: add(0(),X) -> X sqr(s(X)) -> s(add(sqr(X),dbl(X))) 2. Weak: add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) * Step 7: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) half(s(s(X))) -> s(half(X)) - Weak TRS: add(0(),X) -> X dbl(0()) -> 0() first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0, 0) 0 :: [] -(0)-> A(2, 0) 0 :: [] -(0)-> A(8, 1) 0 :: [] -(0)-> A(4, 6) 0 :: [] -(0)-> A(6, 7) 0 :: [] -(0)-> A(6, 6) add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) cons :: [A(0, 6)] -(6)-> A(0, 6) cons :: [A(0, 1)] -(1)-> A(0, 1) cons :: [A(3, 3)] -(3)-> A(3, 3) dbl :: [A(2, 0)] -(1)-> A(0, 0) first :: [A(8, 1) x A(0, 6)] -(2)-> A(0, 0) half :: [A(0, 0)] -(5)-> A(0, 0) nil :: [] -(0)-> A(6, 6) recip :: [A(0, 0)] -(0)-> A(3, 3) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(2, 0)] -(2)-> A(2, 0) s :: [A(9, 1)] -(8)-> A(8, 1) s :: [A(10, 6)] -(4)-> A(4, 6) sqr :: [A(4, 6)] -(4)-> A(0, 0) terms :: [A(10, 8)] -(15)-> A(0, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) dbl :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) half :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) sqr :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) cons_A :: [A(1, 0)] -(0)-> A(1, 0) cons_A :: [A(0, 1)] -(1)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) recip_A :: [A(0, 0)] -(0)-> A(1, 0) recip_A :: [A(0, 0)] -(0)-> A(0, 1) s_A :: [A(1, 0)] -(1)-> A(1, 0) s_A :: [A(1, 1)] -(0)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: dbl(s(X)) -> s(s(dbl(X))) 2. Weak: add(s(X),Y) -> s(add(X,Y)) half(s(s(X))) -> s(half(X)) * Step 8: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(s(X),Y) -> s(add(X,Y)) half(s(s(X))) -> s(half(X)) - Weak TRS: add(0(),X) -> X dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(1, 0) 0 :: [] -(0)-> A(15, 0) 0 :: [] -(0)-> A(0, 10) 0 :: [] -(0)-> A(0, 15) 0 :: [] -(0)-> A(7, 7) add :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) cons :: [A(0, 8)] -(8)-> A(8, 8) cons :: [A(0, 8)] -(8)-> A(12, 8) cons :: [A(0, 1)] -(1)-> A(8, 1) dbl :: [A(15, 0)] -(9)-> A(1, 0) first :: [A(0, 10) x A(8, 8)] -(9)-> A(4, 4) half :: [A(1, 0)] -(1)-> A(0, 0) nil :: [] -(0)-> A(14, 10) recip :: [A(0, 0)] -(0)-> A(6, 6) s :: [A(1, 0)] -(1)-> A(1, 0) s :: [A(15, 0)] -(15)-> A(15, 0) s :: [A(10, 10)] -(10)-> A(0, 10) s :: [A(15, 15)] -(15)-> A(0, 15) s :: [A(0, 0)] -(0)-> A(0, 0) sqr :: [A(0, 15)] -(0)-> A(1, 0) terms :: [A(14, 15)] -(14)-> A(2, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(2, 2) 0 :: [] -(0)-> A_cf(0, 2) 0 :: [] -(0)-> A_cf(2, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) dbl :: [A_cf(0, 2)] -(2)-> A_cf(0, 0) dbl :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) half :: [A_cf(0, 0)] -(1)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(2, 2)] -(2)-> A_cf(0, 2) sqr :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) cons_A :: [A(0, 0)] -(0)-> A(1, 0) cons_A :: [A(0, 1)] -(1)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) recip_A :: [A(0, 0)] -(0)-> A(1, 0) recip_A :: [A(0, 0)] -(0)-> A(0, 1) s_A :: [A(1, 0)] -(1)-> A(1, 0) s_A :: [A(1, 1)] -(1)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: half(s(s(X))) -> s(half(X)) 2. Weak: add(s(X),Y) -> s(add(X,Y)) * Step 9: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(s(X),Y) -> s(add(X,Y)) - Weak TRS: add(0(),X) -> X dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,sqr,terms} and constructors {0,cons ,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 3, maxDegree = 3, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(1, 0, 0) 0 :: [] -(0)-> A(0, 0, 0) 0 :: [] -(0)-> A(9, 3, 0) 0 :: [] -(0)-> A(1, 0, 7) 0 :: [] -(0)-> A(1, 1, 7) add :: [A(1, 0, 0) x A(0, 0, 0)] -(0)-> A(0, 0, 0) cons :: [A(0, 11, 0)] -(6)-> A(1, 5, 6) cons :: [A(0, 11, 0)] -(6)-> A(3, 3, 8) cons :: [A(0, 0, 0)] -(6)-> A(6, 0, 0) dbl :: [A(0, 0, 0)] -(0)-> A(0, 0, 0) first :: [A(9, 3, 0) x A(1, 5, 6)] -(6)-> A(1, 0, 4) half :: [A(0, 0, 0)] -(0)-> A(0, 0, 0) nil :: [] -(0)-> A(4, 0, 10) recip :: [A(0, 0, 0)] -(5)-> A(7, 15, 5) s :: [A(1, 0, 0)] -(1)-> A(1, 0, 0) s :: [A(0, 0, 0)] -(0)-> A(0, 0, 0) s :: [A(12, 3, 0)] -(9)-> A(9, 3, 0) s :: [A(8, 7, 7)] -(1)-> A(1, 0, 7) sqr :: [A(1, 0, 7)] -(1)-> A(0, 0, 0) terms :: [A(15, 14, 9)] -(15)-> A(0, 0, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0, 0) 0 :: [] -(0)-> A_cf(7, 4, 0) 0 :: [] -(0)-> A_cf(12, 3, 2) 0 :: [] -(0)-> A_cf(1, 0, 0) 0 :: [] -(0)-> A_cf(3, 0, 0) 0 :: [] -(0)-> A_cf(7, 14, 2) add :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) add :: [A_cf(1, 0, 0) x A_cf(1, 0, 0)] -(0)-> A_cf(1, 0, 0) dbl :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) dbl :: [A_cf(3, 0, 0)] -(2)-> A_cf(1, 0, 0) half :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) s :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) s :: [A_cf(11, 4, 0)] -(7)-> A_cf(7, 4, 0) s :: [A_cf(1, 0, 0)] -(1)-> A_cf(1, 0, 0) s :: [A_cf(3, 0, 0)] -(3)-> A_cf(3, 0, 0) sqr :: [A_cf(7, 4, 0)] -(0)-> A_cf(1, 0, 0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0, 0) 0_A :: [] -(0)-> A(0, 1, 0) 0_A :: [] -(0)-> A(0, 0, 1) cons_A :: [A(0, 0, 0)] -(1)-> A(1, 0, 0) cons_A :: [A(0, 1, 0)] -(1)-> A(0, 1, 0) cons_A :: [A(0, 1, 0)] -(0)-> A(0, 0, 1) nil_A :: [] -(0)-> A(1, 0, 0) nil_A :: [] -(1)-> A(0, 1, 0) nil_A :: [] -(0)-> A(0, 0, 1) recip_A :: [A(0, 0, 0)] -(0)-> A(1, 0, 0) recip_A :: [A(0, 0, 0)] -(0)-> A(0, 1, 0) recip_A :: [A(0, 0, 0)] -(1)-> A(0, 0, 1) s_A :: [A(1, 0, 0)] -(1)-> A(1, 0, 0) s_A :: [A(1, 1, 0)] -(0)-> A(0, 1, 0) s_A :: [A(1, 1, 1)] -(0)-> A(0, 0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: add(s(X),Y) -> s(add(X,Y)) 2. Weak: * Step 10: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() half(s(s(X))) -> s(half(X)) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N))) - Signature: {add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {add,dbl,first,half,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(n^3))