WORST_CASE(?,O(n^3)) * Step 1: WeightGap 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))) 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,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,sqr,terms} and constructors {0 ,cons,n__first,n__terms,nil,recip,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {1,2}, uargs(cons) = {1,2}, uargs(n__first) = {2}, uargs(recip) = {1}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [8] x1 + [7] p(add) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(dbl) = [0] p(first) = [4] x1 + [8] x2 + [0] p(n__first) = [1] x1 + [1] x2 + [3] p(n__terms) = [1] x1 + [1] p(nil) = [0] p(recip) = [1] x1 + [0] p(s) = [1] x1 + [0] p(sqr) = [4] x1 + [0] p(terms) = [8] x1 + [2] Following rules are strictly oriented: activate(X) = [8] X + [7] > [1] X + [0] = X activate(n__first(X1,X2)) = [8] X1 + [8] X2 + [31] > [4] X1 + [8] X2 + [0] = first(X1,X2) activate(n__terms(X)) = [8] X + [15] > [8] X + [2] = terms(X) terms(N) = [8] N + [2] > [5] N + [1] = cons(recip(sqr(N)),n__terms(s(N))) terms(X) = [8] X + [2] > [1] X + [1] = n__terms(X) Following rules are (at-least) weakly oriented: add(0(),X) = [1] X + [0] >= [1] X + [0] = X add(s(X),Y) = [1] X + [1] Y + [0] >= [1] X + [1] Y + [0] = s(add(X,Y)) dbl(0()) = [0] >= [0] = 0() dbl(s(X)) = [0] >= [0] = s(s(dbl(X))) first(X1,X2) = [4] X1 + [8] X2 + [0] >= [1] X1 + [1] X2 + [3] = n__first(X1,X2) first(0(),X) = [8] X + [0] >= [0] = nil() first(s(X),cons(Y,Z)) = [4] X + [8] Y + [8] Z + [0] >= [1] X + [1] Y + [8] Z + [10] = cons(Y,n__first(X,activate(Z))) sqr(0()) = [0] >= [0] = 0() sqr(s(X)) = [4] X + [0] >= [4] X + [0] = s(add(sqr(X),dbl(X))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap 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(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) sqr(0()) -> 0() 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) terms(N) -> cons(recip(sqr(N)),n__terms(s(N))) terms(X) -> n__terms(X) - Signature: {activate/1,add/2,dbl/1,first/2,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,sqr,terms} and constructors {0 ,cons,n__first,n__terms,nil,recip,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {1,2}, uargs(cons) = {1,2}, uargs(n__first) = {2}, uargs(recip) = {1}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [7] x1 + [0] p(add) = [1] x1 + [1] x2 + [4] p(cons) = [1] x1 + [1] x2 + [2] p(dbl) = [1] p(first) = [7] x2 + [0] p(n__first) = [1] x2 + [0] p(n__terms) = [1] x1 + [1] p(nil) = [2] p(recip) = [1] x1 + [1] p(s) = [1] x1 + [2] p(sqr) = [6] x1 + [1] p(terms) = [7] x1 + [7] Following rules are strictly oriented: add(0(),X) = [1] X + [4] > [1] X + [0] = X dbl(0()) = [1] > [0] = 0() first(s(X),cons(Y,Z)) = [7] Y + [7] Z + [14] > [1] Y + [7] Z + [2] = cons(Y,n__first(X,activate(Z))) sqr(0()) = [1] > [0] = 0() sqr(s(X)) = [6] X + [13] > [6] X + [8] = s(add(sqr(X),dbl(X))) Following rules are (at-least) weakly oriented: activate(X) = [7] X + [0] >= [1] X + [0] = X activate(n__first(X1,X2)) = [7] X2 + [0] >= [7] X2 + [0] = first(X1,X2) activate(n__terms(X)) = [7] X + [7] >= [7] X + [7] = terms(X) add(s(X),Y) = [1] X + [1] Y + [6] >= [1] X + [1] Y + [6] = s(add(X,Y)) dbl(s(X)) = [1] >= [5] = s(s(dbl(X))) first(X1,X2) = [7] X2 + [0] >= [1] X2 + [0] = n__first(X1,X2) first(0(),X) = [7] X + [0] >= [2] = nil() terms(N) = [7] N + [7] >= [7] N + [7] = cons(recip(sqr(N)),n__terms(s(N))) terms(X) = [7] X + [7] >= [1] X + [1] = n__terms(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: add(s(X),Y) -> s(add(X,Y)) dbl(s(X)) -> s(s(dbl(X))) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() - 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(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) 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,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,sqr,terms} and constructors {0 ,cons,n__first,n__terms,nil,recip,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {1,2}, uargs(cons) = {1,2}, uargs(n__first) = {2}, uargs(recip) = {1}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [2] p(add) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(dbl) = [0] p(first) = [1] x2 + [6] p(n__first) = [1] x2 + [4] p(n__terms) = [2] p(nil) = [4] p(recip) = [1] x1 + [0] p(s) = [1] x1 + [0] p(sqr) = [2] p(terms) = [4] Following rules are strictly oriented: first(X1,X2) = [1] X2 + [6] > [1] X2 + [4] = n__first(X1,X2) first(0(),X) = [1] X + [6] > [4] = nil() Following rules are (at-least) weakly oriented: activate(X) = [1] X + [2] >= [1] X + [0] = X activate(n__first(X1,X2)) = [1] X2 + [6] >= [1] X2 + [6] = first(X1,X2) activate(n__terms(X)) = [4] >= [4] = terms(X) add(0(),X) = [1] X + [0] >= [1] X + [0] = X add(s(X),Y) = [1] X + [1] Y + [0] >= [1] X + [1] Y + [0] = s(add(X,Y)) dbl(0()) = [0] >= [0] = 0() dbl(s(X)) = [0] >= [0] = s(s(dbl(X))) first(s(X),cons(Y,Z)) = [1] Y + [1] Z + [6] >= [1] Y + [1] Z + [6] = cons(Y,n__first(X,activate(Z))) sqr(0()) = [2] >= [0] = 0() sqr(s(X)) = [2] >= [2] = s(add(sqr(X),dbl(X))) terms(N) = [4] >= [4] = cons(recip(sqr(N)),n__terms(s(N))) terms(X) = [4] >= [2] = n__terms(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: 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))) 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,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,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(3, 0) 0 :: [] -(0)-> A(13, 0) 0 :: [] -(0)-> A(1, 0) 0 :: [] -(0)-> A(0, 14) 0 :: [] -(0)-> A(11, 6) 0 :: [] -(0)-> A(5, 6) activate :: [A(9, 14)] -(14)-> A(0, 0) add :: [A(3, 0) x A(4, 0)] -(3)-> A(3, 0) cons :: [A(0, 14) x A(14, 14)] -(14)-> A(0, 14) cons :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) cons :: [A(1, 0) x A(1, 0)] -(0)-> A(1, 0) dbl :: [A(13, 0)] -(0)-> A(4, 0) first :: [A(1, 0) x A(0, 14)] -(11)-> A(0, 0) n__first :: [A(9, 0) x A(9, 14)] -(0)-> A(9, 14) n__first :: [A(0, 0) x A(0, 8)] -(0)-> A(0, 8) n__first :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) n__terms :: [A(9, 14)] -(9)-> A(9, 14) n__terms :: [A(1, 0)] -(1)-> A(1, 0) n__terms :: [A(2, 12)] -(2)-> A(2, 12) nil :: [] -(0)-> A(6, 6) recip :: [A(0, 0)] -(0)-> A(1, 3) s :: [A(3, 0)] -(3)-> A(3, 0) s :: [A(13, 0)] -(13)-> A(13, 0) s :: [A(1, 0)] -(1)-> A(1, 0) s :: [A(14, 14)] -(14)-> A(0, 14) s :: [A(4, 0)] -(4)-> A(4, 0) s :: [A(2, 0)] -(2)-> A(2, 0) sqr :: [A(0, 14)] -(4)-> A(3, 0) terms :: [A(3, 14)] -(15)-> A(1, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) 0 :: [] -(0)-> A_cf(8, 0) 0 :: [] -(0)-> A_cf(3, 2) 0 :: [] -(0)-> A_cf(3, 0) 0 :: [] -(0)-> A_cf(1, 0) 0 :: [] -(0)-> A_cf(4, 0) 0 :: [] -(0)-> A_cf(2, 2) activate :: [A_cf(9, 0)] -(4)-> A_cf(0, 0) activate :: [A_cf(5, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(9, 0) x A_cf(9, 0)] -(0)-> A_cf(9, 0) cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) cons :: [A_cf(5, 0) x A_cf(5, 0)] -(0)-> A_cf(5, 0) dbl :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) first :: [A_cf(8, 0) x A_cf(9, 0)] -(0)-> A_cf(0, 0) first :: [A_cf(1, 0) x A_cf(5, 0)] -(0)-> A_cf(0, 0) n__first :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) n__first :: [A_cf(9, 0) x A_cf(9, 0)] -(0)-> A_cf(9, 0) n__first :: [A_cf(5, 0) x A_cf(5, 0)] -(0)-> A_cf(5, 0) n__terms :: [A_cf(9, 0)] -(9)-> A_cf(9, 0) n__terms :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) n__terms :: [A_cf(4, 0)] -(4)-> A_cf(4, 0) n__terms :: [A_cf(5, 0)] -(5)-> A_cf(5, 0) nil :: [] -(0)-> A_cf(2, 0) nil :: [] -(0)-> A_cf(2, 2) recip :: [A_cf(0, 0)] -(0)-> A_cf(1, 3) recip :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(8, 0)] -(8)-> A_cf(8, 0) s :: [A_cf(1, 0)] -(1)-> A_cf(1, 0) s :: [A_cf(4, 0)] -(4)-> A_cf(4, 0) sqr :: [A_cf(0, 0)] -(10)-> A_cf(0, 0) sqr :: [A_cf(4, 0)] -(0)-> A_cf(0, 0) sqr :: [A_cf(0, 0)] -(5)-> A_cf(0, 0) terms :: [A_cf(8, 0)] -(13)-> A_cf(0, 0) terms :: [A_cf(4, 0)] -(2)-> 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) x A(1, 0)] -(0)-> A(1, 0) cons_A :: [A(0, 1) x A(1, 1)] -(1)-> A(0, 1) n__first_A :: [A(0) x A(0)] -(0)-> A(1, 0) n__first_A :: [A(0) x A(0)] -(0)-> A(0, 1) n__terms_A :: [A(0)] -(1)-> A(1, 0) n__terms_A :: [A(0)] -(0)-> 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: dbl(s(X)) -> s(s(dbl(X))) 2. Weak: add(s(X),Y) -> s(add(X,Y)) * Step 5: 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))) 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,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,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(4, 2, 0) 0 :: [] -(0)-> A(12, 0, 0) 0 :: [] -(0)-> A(4, 0, 8) 0 :: [] -(0)-> A(4, 1, 6) 0 :: [] -(0)-> A(1, 1, 6) 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(5, 0, 0) x A(5, 10, 15)] -(10)-> A(5, 10, 15) cons :: [A(3, 0, 0) x A(3, 0, 0)] -(0)-> A(3, 0, 0) cons :: [A(1, 0, 0) x A(1, 0, 0)] -(0)-> A(1, 0, 0) dbl :: [A(4, 2, 0)] -(2)-> A(1, 0, 0) first :: [A(12, 0, 0) x A(5, 10, 15)] -(8)-> A(0, 0, 0) n__first :: [A(15, 0, 0) x A(15, 15, 15)] -(15)-> A(0, 0, 15) n__first :: [A(1, 0, 0) x A(4, 3, 0)] -(1)-> A(1, 3, 0) n__first :: [A(4, 0, 0) x A(4, 0, 0)] -(4)-> A(4, 0, 0) n__terms :: [A(15, 15, 15)] -(15)-> A(0, 0, 15) n__terms :: [A(0, 0, 0)] -(0)-> A(1, 0, 0) n__terms :: [A(6, 6, 0)] -(6)-> A(7, 6, 0) nil :: [] -(0)-> A(1, 1, 6) recip :: [A(0, 0, 0)] -(0)-> A(10, 8, 3) s :: [A(2, 0, 0)] -(2)-> A(2, 0, 0) s :: [A(6, 2, 0)] -(4)-> A(4, 2, 0) s :: [A(12, 0, 0)] -(12)-> A(12, 0, 0) s :: [A(12, 8, 8)] -(4)-> A(4, 0, 8) s :: [A(1, 0, 0)] -(1)-> A(1, 0, 0) s :: [A(0, 0, 0)] -(0)-> A(0, 0, 0) s :: [A(3, 2, 0)] -(1)-> A(1, 2, 0) sqr :: [A(4, 0, 8)] -(2)-> A(0, 0, 0) terms :: [A(7, 14, 12)] -(15)-> A(1, 0, 0) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0, 0) 0 :: [] -(0)-> A_cf(3, 0, 0) 0 :: [] -(0)-> A_cf(4, 5, 0) 0 :: [] -(0)-> A_cf(1, 3, 2) 0 :: [] -(0)-> A_cf(5, 0, 0) 0 :: [] -(0)-> A_cf(15, 10, 0) 0 :: [] -(0)-> A_cf(2, 0, 0) 0 :: [] -(0)-> A_cf(1, 0, 2) 0 :: [] -(0)-> A_cf(6, 2, 0) 0 :: [] -(0)-> A_cf(13, 3, 2) 0 :: [] -(0)-> A_cf(1, 0, 0) 0 :: [] -(0)-> A_cf(5, 14, 2) 0 :: [] -(0)-> A_cf(3, 4, 0) 0 :: [] -(0)-> A_cf(13, 12, 2) 0 :: [] -(0)-> A_cf(4, 0, 0) 0 :: [] -(0)-> A_cf(9, 6, 2) activate :: [A_cf(5, 5, 0)] -(7)-> A_cf(0, 0, 0) activate :: [A_cf(5, 10, 0)] -(0)-> A_cf(5, 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)] -(1)-> A_cf(0, 0, 0) add :: [A_cf(2, 0, 0) x A_cf(2, 0, 0)] -(0)-> A_cf(2, 0, 0) cons :: [A_cf(10, 0, 0) x A_cf(10, 5, 0)] -(5)-> A_cf(10, 5, 0) cons :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) cons :: [A_cf(10, 0, 0) x A_cf(10, 10, 0)] -(10)-> A_cf(10, 10, 0) cons :: [A_cf(5, 0, 0) x A_cf(5, 0, 0)] -(0)-> A_cf(5, 0, 0) dbl :: [A_cf(5, 0, 0)] -(0)-> A_cf(0, 0, 0) dbl :: [A_cf(2, 0, 0)] -(1)-> A_cf(1, 0, 0) dbl :: [A_cf(1, 0, 0)] -(3)-> A_cf(0, 0, 0) dbl :: [A_cf(4, 0, 0)] -(0)-> A_cf(2, 0, 0) first :: [A_cf(3, 0, 0) x A_cf(10, 5, 0)] -(2)-> A_cf(0, 0, 0) first :: [A_cf(5, 0, 0) x A_cf(10, 10, 0)] -(5)-> A_cf(5, 0, 0) n__first :: [A_cf(0, 0, 0) x A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) n__first :: [A_cf(5, 0, 0) x A_cf(10, 5, 0)] -(5)-> A_cf(5, 5, 0) n__first :: [A_cf(5, 0, 0) x A_cf(15, 10, 0)] -(5)-> A_cf(5, 10, 0) n__first :: [A_cf(5, 0, 0) x A_cf(9, 4, 0)] -(5)-> A_cf(5, 4, 0) n__first :: [A_cf(5, 0, 0) x A_cf(5, 0, 0)] -(5)-> A_cf(5, 0, 0) n__terms :: [A_cf(5, 5, 0)] -(5)-> A_cf(5, 5, 0) n__terms :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) n__terms :: [A_cf(3, 3, 0)] -(3)-> A_cf(12, 3, 0) n__terms :: [A_cf(10, 10, 0)] -(10)-> A_cf(5, 10, 0) n__terms :: [A_cf(1, 1, 0)] -(1)-> A_cf(5, 1, 0) n__terms :: [A_cf(2, 2, 0)] -(2)-> A_cf(8, 2, 0) nil :: [] -(0)-> A_cf(2, 3, 2) nil :: [] -(0)-> A_cf(5, 3, 2) recip :: [A_cf(0, 0, 0)] -(0)-> A_cf(15, 5, 5) recip :: [A_cf(0, 0, 0)] -(0)-> A_cf(12, 4, 6) s :: [A_cf(0, 0, 0)] -(0)-> A_cf(0, 0, 0) s :: [A_cf(3, 0, 0)] -(3)-> A_cf(3, 0, 0) s :: [A_cf(9, 5, 0)] -(4)-> A_cf(4, 5, 0) s :: [A_cf(5, 0, 0)] -(5)-> A_cf(5, 0, 0) s :: [A_cf(1, 0, 0)] -(1)-> A_cf(1, 0, 0) s :: [A_cf(2, 0, 0)] -(2)-> A_cf(2, 0, 0) s :: [A_cf(8, 2, 0)] -(6)-> A_cf(6, 2, 0) s :: [A_cf(2, 1, 0)] -(1)-> A_cf(1, 1, 0) s :: [A_cf(7, 4, 0)] -(3)-> A_cf(3, 4, 0) s :: [A_cf(4, 0, 0)] -(4)-> A_cf(4, 0, 0) sqr :: [A_cf(4, 5, 0)] -(0)-> A_cf(0, 0, 0) sqr :: [A_cf(6, 2, 0)] -(0)-> A_cf(0, 0, 0) sqr :: [A_cf(3, 4, 0)] -(1)-> A_cf(2, 0, 0) terms :: [A_cf(5, 5, 0)] -(12)-> A_cf(0, 0, 0) terms :: [A_cf(10, 10, 0)] -(2)-> A_cf(5, 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(1, 0, 0) x A(1, 0, 0)] -(0)-> A(1, 0, 0) cons_A :: [A(0, 0, 0) x A(0, 1, 0)] -(1)-> A(0, 1, 0) cons_A :: [A(0, 0, 0) x A(0, 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)] -(1)-> 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)] -(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 6: 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))) 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,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,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))