WORST_CASE(?,O(n^3)) * Step 1: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(48) 0 :: [] -(0)-> A(44) 0 :: [] -(0)-> A(30) activate :: [A(48)] -(5)-> A(0) add :: [A(0) x A(0)] -(7)-> A(0) cons :: [A(0) x A(48)] -(48)-> A(48) cons :: [A(0) x A(0)] -(0)-> A(0) dbl :: [A(0)] -(3)-> A(0) first :: [A(48) x A(48)] -(4)-> A(0) half :: [A(0)] -(31)-> A(0) n__first :: [A(48) x A(48)] -(0)-> A(48) n__first :: [A(1) x A(1)] -(0)-> A(1) n__first :: [A(0) x A(0)] -(0)-> A(0) n__terms :: [A(48)] -(48)-> A(48) n__terms :: [A(0)] -(0)-> A(0) n__terms :: [A(31)] -(31)-> A(31) nil :: [] -(0)-> A(30) recip :: [A(0)] -(0)-> A(46) s :: [A(0)] -(0)-> A(0) s :: [A(48)] -(48)-> A(48) s :: [A(44)] -(44)-> A(44) sqr :: [A(44)] -(15)-> A(0) terms :: [A(48)] -(47)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) n__first_A :: [A(0) x A(0)] -(0)-> A(1) n__terms_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: activate(n__terms(X)) -> terms(X) first(X1,X2) -> n__first(X1,X2) first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() 2. Weak: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) 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() half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) * Step 2: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) 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() half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) - Weak TRS: activate(n__terms(X)) -> terms(X) first(X1,X2) -> n__first(X1,X2) first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(31) 0 :: [] -(0)-> A(28) 0 :: [] -(0)-> A(15) 0 :: [] -(0)-> A(14) activate :: [A(31)] -(8)-> A(2) add :: [A(0) x A(0)] -(10)-> A(0) cons :: [A(0) x A(31)] -(31)-> A(31) cons :: [A(0) x A(2)] -(2)-> A(2) dbl :: [A(0)] -(0)-> A(0) first :: [A(31) x A(31)] -(8)-> A(2) half :: [A(0)] -(31)-> A(0) n__first :: [A(31) x A(31)] -(0)-> A(31) n__first :: [A(7) x A(7)] -(0)-> A(7) n__first :: [A(2) x A(2)] -(0)-> A(2) n__terms :: [A(31)] -(31)-> A(31) n__terms :: [A(2)] -(2)-> A(2) n__terms :: [A(15)] -(15)-> A(15) nil :: [] -(0)-> A(12) recip :: [A(0)] -(0)-> A(13) s :: [A(0)] -(0)-> A(0) s :: [A(28)] -(28)-> A(28) s :: [A(31)] -(31)-> A(31) s :: [A(2)] -(2)-> A(2) sqr :: [A(28)] -(0)-> A(0) terms :: [A(31)] -(31)-> A(2) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) n__first_A :: [A(0) x A(0)] -(0)-> A(1) n__terms_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: activate(X) -> X add(0(),X) -> X 2. Weak: activate(n__first(X1,X2)) -> first(X1,X2) add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) * Step 3: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: activate(n__first(X1,X2)) -> first(X1,X2) add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(0(),X) -> nil() half(s(s(X))) -> s(half(X)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) - Weak TRS: activate(X) -> X activate(n__terms(X)) -> terms(X) add(0(),X) -> X first(X1,X2) -> n__first(X1,X2) first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(7) activate :: [A(12)] -(15)-> A(0) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(12)] -(12)-> A(12) cons :: [A(0) x A(0)] -(0)-> A(0) dbl :: [A(0)] -(2)-> A(0) first :: [A(0) x A(12)] -(9)-> A(0) half :: [A(0)] -(15)-> A(0) n__first :: [A(0) x A(12)] -(0)-> A(12) n__first :: [A(0) x A(0)] -(0)-> A(0) n__terms :: [A(12)] -(0)-> A(12) n__terms :: [A(0)] -(0)-> A(0) nil :: [] -(0)-> A(6) recip :: [A(0)] -(0)-> A(3) s :: [A(0)] -(0)-> A(0) s :: [A(7)] -(7)-> A(7) s :: [A(1)] -(1)-> A(1) sqr :: [A(7)] -(7)-> A(0) terms :: [A(12)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) n__first_A :: [A(0) x A(0)] -(0)-> A(1) n__terms_A :: [A(0)] -(0)-> 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: dbl(0()) -> 0() first(0(),X) -> nil() 2. Weak: activate(n__first(X1,X2)) -> first(X1,X2) 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))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) * Step 4: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: activate(n__first(X1,X2)) -> first(X1,X2) 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))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) - Weak TRS: activate(X) -> X activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(6) activate :: [A(15)] -(5)-> A(0) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(15)-> A(15) cons :: [A(0) x A(0)] -(0)-> A(0) dbl :: [A(0)] -(0)-> A(0) first :: [A(0) x A(15)] -(4)-> A(0) half :: [A(0)] -(15)-> A(0) n__first :: [A(0) x A(15)] -(15)-> A(15) n__first :: [A(0) x A(3)] -(3)-> A(3) n__first :: [A(0) x A(0)] -(0)-> A(0) n__terms :: [A(15)] -(15)-> A(15) n__terms :: [A(0)] -(0)-> A(0) n__terms :: [A(7)] -(7)-> A(7) nil :: [] -(0)-> A(6) recip :: [A(0)] -(1)-> A(1) s :: [A(0)] -(0)-> A(0) s :: [A(6)] -(6)-> A(6) sqr :: [A(6)] -(5)-> A(0) terms :: [A(15)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) n__first_A :: [A(0) x A(0)] -(1)-> A(1) n__terms_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: activate(n__first(X1,X2)) -> first(X1,X2) terms(X) -> n__terms(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)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) * Step 5: 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)) sqr(s(X)) -> s(add(sqr(X),dbl(X))) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) - Weak TRS: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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) activate :: [A(15)] -(3)-> A(0) add :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(15)-> A(15) cons :: [A(0) x A(0)] -(0)-> A(0) dbl :: [A(0)] -(0)-> A(0) first :: [A(15) x A(15)] -(9)-> A(0) half :: [A(0)] -(5)-> A(0) n__first :: [A(15) x A(15)] -(15)-> A(15) n__first :: [A(3) x A(3)] -(3)-> A(3) n__first :: [A(0) x A(0)] -(0)-> A(0) n__terms :: [A(15)] -(15)-> A(15) n__terms :: [A(0)] -(0)-> A(0) n__terms :: [A(1)] -(1)-> A(1) nil :: [] -(0)-> A(6) recip :: [A(0)] -(0)-> A(5) s :: [A(0)] -(0)-> A(0) s :: [A(15)] -(15)-> A(15) sqr :: [A(15)] -(4)-> A(0) terms :: [A(15)] -(7)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(1)-> A(1) n__first_A :: [A(0) x A(0)] -(1)-> A(1) n__terms_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)),n__terms(s(N))) 2. Weak: 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(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: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) half(0()) -> 0() half(dbl(X)) -> X half(s(0())) -> 0() sqr(0()) -> 0() terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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) activate :: [A(15)] -(8)-> A(0) add :: [A(0) x A(0)] -(4)-> A(0) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(0)] -(0)-> A(0) dbl :: [A(0)] -(0)-> A(0) first :: [A(0) x A(15)] -(10)-> A(0) half :: [A(0)] -(5)-> A(0) n__first :: [A(0) x A(15)] -(15)-> A(15) n__first :: [A(0) x A(3)] -(3)-> A(3) n__first :: [A(0) x A(0)] -(0)-> A(0) n__terms :: [A(15)] -(15)-> A(15) n__terms :: [A(0)] -(0)-> A(0) n__terms :: [A(2)] -(2)-> A(2) nil :: [] -(0)-> A(6) recip :: [A(0)] -(0)-> A(2) s :: [A(0)] -(0)-> A(0) s :: [A(15)] -(15)-> A(15) sqr :: [A(15)] -(1)-> A(0) terms :: [A(15)] -(15)-> A(0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) activate :: [A_cf(0)] -(0)-> A_cf(0) add :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) dbl :: [A_cf(0)] -(0)-> A_cf(0) first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) half :: [A_cf(0)] -(0)-> A_cf(0) n__first :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__terms :: [A_cf(0)] -(0)-> A_cf(0) nil :: [] -(0)-> A_cf(0) recip :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) sqr :: [A_cf(0)] -(0)-> A_cf(0) terms :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__first_A :: [A(0) x A(0)] -(1)-> A(1) n__terms_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: 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: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(6, 0) 0 :: [] -(0)-> A(3, 0) 0 :: [] -(0)-> A(0, 7) 0 :: [] -(0)-> A(5, 7) 0 :: [] -(0)-> A(7, 7) activate :: [A(0, 9)] -(4)-> A(0, 0) add :: [A(0, 0) x A(1, 0)] -(0)-> A(0, 0) cons :: [A(0, 9) x A(15, 9)] -(6)-> A(6, 9) cons :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) dbl :: [A(6, 0)] -(0)-> A(3, 0) first :: [A(6, 0) x A(6, 9)] -(6)-> A(0, 0) half :: [A(3, 0)] -(13)-> A(0, 0) n__first :: [A(9, 0) x A(9, 9)] -(9)-> A(0, 9) n__first :: [A(1, 0) x A(1, 1)] -(1)-> A(0, 1) n__first :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) n__terms :: [A(9, 9)] -(9)-> A(0, 9) n__terms :: [A(0, 0)] -(0)-> A(0, 0) n__terms :: [A(8, 0)] -(8)-> A(8, 0) nil :: [] -(0)-> A(6, 6) recip :: [A(0, 0)] -(0)-> A(0, 4) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(6, 0)] -(6)-> A(6, 0) s :: [A(3, 0)] -(3)-> A(3, 0) s :: [A(7, 7)] -(7)-> A(0, 7) sqr :: [A(0, 7)] -(0)-> A(0, 0) terms :: [A(9, 7)] -(10)-> A(0, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(3, 3) 0 :: [] -(0)-> A_cf(4, 0) 0 :: [] -(0)-> A_cf(1, 1) 0 :: [] -(0)-> A_cf(3, 2) 0 :: [] -(0)-> A_cf(3, 0) 0 :: [] -(0)-> A_cf(2, 2) 0 :: [] -(0)-> A_cf(2, 0) activate :: [A_cf(3, 0)] -(5)-> A_cf(0, 0) activate :: [A_cf(15, 0)] -(1)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(0, 0) x A_cf(3, 0)] -(3)-> A_cf(3, 0) cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(0, 0) x A_cf(15, 0)] -(15)-> A_cf(15, 0) dbl :: [A_cf(4, 0)] -(2)-> A_cf(0, 0) dbl :: [A_cf(4, 0)] -(0)-> A_cf(0, 0) dbl :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) first :: [A_cf(3, 0) x A_cf(3, 0)] -(1)-> A_cf(0, 0) first :: [A_cf(4, 0) x A_cf(15, 0)] -(1)-> A_cf(0, 0) half :: [A_cf(0, 0)] -(1)-> A_cf(0, 0) n__first :: [A_cf(1, 0) x A_cf(1, 0)] -(0)-> A_cf(1, 0) n__first :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) n__first :: [A_cf(3, 0) x A_cf(3, 0)] -(0)-> A_cf(3, 0) n__first :: [A_cf(15, 0) x A_cf(15, 0)] -(0)-> A_cf(15, 0) n__first :: [A_cf(4, 0) x A_cf(4, 0)] -(0)-> A_cf(4, 0) n__terms :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) n__terms :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) n__terms :: [A_cf(15, 0)] -(15)-> A_cf(15, 0) n__terms :: [A_cf(4, 0)] -(4)-> A_cf(4, 0) nil :: [] -(0)-> A_cf(2, 2) recip :: [A_cf(0, 0)] -(0)-> A_cf(11, 1) recip :: [A_cf(0, 0)] -(0)-> A_cf(11, 11) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(4, 0)] -(4)-> A_cf(4, 0) s :: [A_cf(3, 0)] -(3)-> A_cf(3, 0) s :: [A_cf(2, 0)] -(2)-> A_cf(2, 0) sqr :: [A_cf(3, 0)] -(2)-> A_cf(0, 0) sqr :: [A_cf(2, 0)] -(0)-> A_cf(0, 0) sqr :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) terms :: [A_cf(3, 0)] -(8)-> A_cf(0, 0) terms :: [A_cf(4, 0)] -(9)-> 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) x A(1, 0)] -(1)-> A(1, 0) cons_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) n__first_A :: [A(0) x A(0)] -(0)-> A(1, 0) n__first_A :: [A(0) x A(0)] -(1)-> A(0, 1) n__terms_A :: [A(0)] -(1)-> A(1, 0) n__terms_A :: [A(0)] -(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)) dbl(s(X)) -> s(s(dbl(X))) * Step 8: 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))) - Weak TRS: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,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(8, 0) 0 :: [] -(0)-> A(7, 8) 0 :: [] -(0)-> A(7, 6) activate :: [A(2, 13)] -(0)-> A(0, 0) add :: [A(0, 0) x A(0, 0)] -(3)-> A(0, 0) cons :: [A(0, 13) x A(14, 13)] -(1)-> A(1, 13) cons :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) dbl :: [A(8, 0)] -(0)-> A(0, 0) first :: [A(0, 0) x A(1, 13)] -(13)-> A(0, 0) half :: [A(0, 0)] -(2)-> A(0, 0) n__first :: [A(0, 0) x A(15, 13)] -(13)-> A(2, 13) n__first :: [A(0, 0) x A(1, 0)] -(0)-> A(1, 0) n__first :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) n__terms :: [A(15, 13)] -(13)-> A(2, 13) n__terms :: [A(0, 0)] -(0)-> A(0, 0) nil :: [] -(0)-> A(6, 6) recip :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(8, 0)] -(8)-> A(8, 0) s :: [A(15, 8)] -(7)-> A(7, 8) sqr :: [A(7, 8)] -(7)-> A(0, 0) terms :: [A(7, 11)] -(13)-> A(0, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(5, 0) 0 :: [] -(0)-> A_cf(3, 2) 0 :: [] -(0)-> A_cf(1, 2) 0 :: [] -(0)-> A_cf(4, 0) 0 :: [] -(0)-> A_cf(2, 2) activate :: [A_cf(14, 0)] -(13)-> A_cf(0, 0) activate :: [A_cf(12, 0)] -(14)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(0, 0) x A_cf(14, 0)] -(14)-> A_cf(14, 0) cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(0, 0) x A_cf(12, 0)] -(12)-> A_cf(12, 0) dbl :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) first :: [A_cf(0, 0) x A_cf(14, 0)] -(0)-> A_cf(0, 0) first :: [A_cf(0, 0) x A_cf(12, 0)] -(10)-> A_cf(0, 0) half :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) n__first :: [A_cf(0, 0) x A_cf(7, 0)] -(0)-> A_cf(7, 0) n__first :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) n__first :: [A_cf(0, 0) x A_cf(14, 0)] -(0)-> A_cf(14, 0) n__first :: [A_cf(0, 0) x A_cf(12, 0)] -(0)-> A_cf(12, 0) n__terms :: [A_cf(14, 0)] -(0)-> A_cf(14, 0) n__terms :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) n__terms :: [A_cf(12, 0)] -(0)-> A_cf(12, 0) n__terms :: [A_cf(2, 0)] -(0)-> A_cf(2, 0) n__terms :: [A_cf(7, 0)] -(0)-> A_cf(7, 0) nil :: [] -(0)-> A_cf(2, 2) recip :: [A_cf(0, 0)] -(0)-> A_cf(4, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(5, 0)] -(5)-> A_cf(5, 0) s :: [A_cf(1, 0)] -(1)-> A_cf(1, 0) s :: [A_cf(4, 0)] -(4)-> A_cf(4, 0) sqr :: [A_cf(5, 0)] -(7)-> A_cf(0, 0) sqr :: [A_cf(4, 0)] -(6)-> A_cf(0, 0) sqr :: [A_cf(0, 0)] -(1)-> A_cf(0, 0) terms :: [A_cf(12, 0)] -(11)-> A_cf(0, 0) terms :: [A_cf(12, 0)] -(14)-> 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) x A(1, 0)] -(1)-> A(1, 0) cons_A :: [A(0, 1) x A(1, 1)] -(0)-> A(0, 1) n__first_A :: [A(0) x A(0)] -(0)-> A(1, 0) n__first_A :: [A(0) x A(0)] -(1)-> A(0, 1) n__terms_A :: [A(0)] -(0)-> A(1, 0) n__terms_A :: [A(0)] -(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(1, 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)) * Step 9: Ara WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(s(X),Y) -> s(add(X,Y)) - Weak TRS: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,nil,recip,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 3, maxDegree = 3, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2, 0, 0) 0 :: [] -(0)-> A(12, 0, 0) 0 :: [] -(0)-> A(0, 0, 15) 0 :: [] -(0)-> A(1, 0, 0) 0 :: [] -(0)-> A(0, 0, 13) 0 :: [] -(0)-> A(8, 9, 7) 0 :: [] -(0)-> A(1, 1, 7) 0 :: [] -(0)-> A(4, 1, 7) activate :: [A(0, 0, 15)] -(0)-> A(0, 0, 0) add :: [A(2, 0, 0) x A(1, 0, 0)] -(0)-> A(1, 0, 0) cons :: [A(0, 0, 15) x A(15, 0, 15)] -(0)-> A(0, 0, 15) cons :: [A(0, 0, 0) x A(0, 0, 0)] -(0)-> A(0, 0, 0) cons :: [A(0, 0, 0) x A(5, 0, 0)] -(5)-> A(5, 7, 0) dbl :: [A(12, 0, 0)] -(0)-> A(1, 0, 0) first :: [A(0, 0, 15) x A(0, 0, 15)] -(0)-> A(0, 0, 0) half :: [A(1, 0, 0)] -(10)-> A(0, 0, 0) n__first :: [A(0, 0, 15) x A(0, 0, 15)] -(15)-> A(0, 0, 15) n__first :: [A(0, 0, 0) x A(0, 0, 0)] -(0)-> A(0, 0, 0) n__first :: [A(0, 0, 0) x A(0, 0, 0)] -(0)-> A(0, 8, 0) n__terms :: [A(15, 15, 15)] -(15)-> A(0, 0, 15) n__terms :: [A(5, 0, 0)] -(0)-> A(5, 0, 0) n__terms :: [A(10, 1, 1)] -(1)-> A(8, 1, 1) nil :: [] -(0)-> A(1, 1, 6) recip :: [A(0, 0, 0)] -(0)-> A(5, 0, 8) s :: [A(2, 0, 0)] -(2)-> A(2, 0, 0) s :: [A(12, 0, 0)] -(12)-> A(12, 0, 0) s :: [A(15, 15, 15)] -(15)-> A(0, 0, 15) s :: [A(1, 0, 0)] -(1)-> A(1, 0, 0) s :: [A(13, 13, 13)] -(13)-> A(0, 0, 13) s :: [A(0, 0, 0)] -(0)-> A(0, 0, 0) s :: [A(14, 5, 0)] -(9)-> A(9, 5, 0) sqr :: [A(0, 0, 13)] -(0)-> A(1, 0, 0) terms :: [A(15, 8, 15)] -(15)-> A(0, 1, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0, 0) 0 :: [] -(0)-> A_cf(14, 14, 0) 0 :: [] -(0)-> A_cf(15, 14, 2) 0 :: [] -(0)-> A_cf(11, 0, 0) 0 :: [] -(0)-> A_cf(1, 3, 2) 0 :: [] -(0)-> A_cf(15, 8, 2) 0 :: [] -(0)-> A_cf(14, 6, 2) 0 :: [] -(0)-> A_cf(0, 1, 0) 0 :: [] -(0)-> A_cf(12, 8, 0) 0 :: [] -(0)-> A_cf(14, 14, 2) 0 :: [] -(0)-> A_cf(1, 8, 0) 0 :: [] -(0)-> A_cf(15, 15, 2) 0 :: [] -(0)-> A_cf(1, 0, 0) 0 :: [] -(0)-> A_cf(7, 0, 0) 0 :: [] -(0)-> A_cf(7, 2, 2) activate :: [A_cf(0, 0, 0)] -(15)-> A_cf(0, 0, 0) activate :: [A_cf(15, 0, 0)] -(14)-> A_cf(1, 0, 0) add :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) add :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(2)-> A_cf(0, 0, 0) add :: [A_cf(1, 0, 0) x A_cf(1, 0, 0)] -(0)-> A_cf(1, 0, 0) cons :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) cons :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 12, 0) cons :: [A_cf(0, 0, 0) x A_cf(15, 0, 0)] -(15)-> A_cf(15, 0, 0) cons :: [A_cf(0, 0, 0) x A_cf(1, 0, 0)] -(1)-> A_cf(1, 7, 0) cons :: [A_cf(0, 0, 0) x A_cf(1, 0, 0)] -(1)-> A_cf(1, 1, 0) dbl :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) dbl :: [A_cf(0, 0, 0)] -(7)-> A_cf(0, 0, 0) dbl :: [A_cf(0, 1, 0)] -(2)-> A_cf(0, 0, 0) dbl :: [A_cf(0, 1, 0)] -(9)-> A_cf(0, 0, 0) dbl :: [A_cf(7, 0, 0)] -(0)-> A_cf(1, 0, 0) first :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(15)-> A_cf(0, 0, 0) first :: [A_cf(0, 0, 0) x A_cf(15, 0, 0)] -(8)-> A_cf(1, 1, 0) half :: [A_cf(0, 0, 0)] -(1)-> A_cf(0, 0, 0) n__first :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 3, 0) n__first :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 12, 0) n__first :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) n__first :: [A_cf(0, 0, 0) x A_cf(15, 0, 0)] -(15)-> A_cf(15, 0, 0) n__first :: [A_cf(0, 0, 0) x A_cf(8, 0, 0)] -(8)-> A_cf(8, 1, 0) n__first :: [A_cf(0, 0, 0) x A_cf(1, 0, 0)] -(1)-> A_cf(1, 11, 0) n__terms :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) n__terms :: [A_cf(15, 0, 0)] -(0)-> A_cf(15, 0, 0) n__terms :: [A_cf(2, 0, 0)] -(0)-> A_cf(1, 1, 0) nil :: [] -(0)-> A_cf(8, 8, 2) nil :: [] -(0)-> A_cf(9, 12, 2) recip :: [A_cf(0, 0, 0)] -(0)-> A_cf(12, 5, 1) recip :: [A_cf(0, 0, 0)] -(0)-> A_cf(13, 5, 4) s :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) s :: [A_cf(11, 0, 0)] -(11)-> A_cf(11, 0, 0) s :: [A_cf(4, 0, 0)] -(4)-> A_cf(4, 0, 0) s :: [A_cf(1, 1, 0)] -(0)-> A_cf(0, 1, 0) s :: [A_cf(9, 8, 0)] -(1)-> A_cf(1, 8, 0) s :: [A_cf(1, 0, 0)] -(1)-> A_cf(1, 0, 0) s :: [A_cf(7, 0, 0)] -(7)-> A_cf(7, 0, 0) sqr :: [A_cf(0, 0, 0)] -(1)-> A_cf(0, 0, 0) sqr :: [A_cf(11, 0, 0)] -(1)-> A_cf(0, 0, 0) sqr :: [A_cf(1, 8, 0)] -(1)-> A_cf(1, 0, 0) terms :: [A_cf(0, 0, 0)] -(15)-> A_cf(0, 0, 0) terms :: [A_cf(15, 0, 0)] -(14)-> 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) x A(1, 0, 0)] -(1)-> A(1, 0, 0) cons_A :: [A(0, 0, 0) x A(0, 0, 0)] -(0)-> A(0, 1, 0) cons_A :: [A(0, 0, 1) x A(1, 0, 1)] -(0)-> A(0, 0, 1) n__first_A :: [A(0) x A(0)] -(1)-> A(1, 0, 0) n__first_A :: [A(0) x A(0)] -(0)-> A(0, 1, 0) n__first_A :: [A(0) x A(0)] -(1)-> A(0, 0, 1) n__terms_A :: [A(0)] -(0)-> A(1, 0, 0) n__terms_A :: [A(0)] -(0)-> A(0, 1, 0) n__terms_A :: [A(0)] -(1)-> A(0, 0, 1) nil_A :: [] -(0)-> A(1, 0, 0) nil_A :: [] -(0)-> 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)] -(0)-> 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)] -(1)-> 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: activate(X) -> X activate(n__first(X1,X2)) -> first(X1,X2) activate(n__terms(X)) -> terms(X) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,half/1,sqr/1,terms/1} / {0/0,cons/2,n__first/2,n__terms/1,nil/0,recip/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,dbl,first,half,sqr ,terms} and constructors {0,cons,n__first,n__terms,nil,recip,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))