WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1} / {n__cons/2,n__from/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,cons,from} and constructors {n__cons,n__from ,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1} / {n__cons/2,n__from/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,cons,from} and constructors {n__cons,n__from ,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) activate#(X) -> c_2() activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) cons#(X1,X2) -> c_5() from#(X) -> c_6(cons#(X,n__from(s(X)))) from#(X) -> c_7() Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) activate#(X) -> c_2() activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) cons#(X1,X2) -> c_5() from#(X) -> c_6(cons#(X,n__from(s(X)))) from#(X) -> c_7() - Weak TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1,2nd#/1,activate#/1,cons#/2,from#/1} / {n__cons/2,n__from/1,s/1,c_1/1,c_2/0 ,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,activate#,cons#,from#} and constructors {n__cons ,n__from,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,7} by application of Pre({1,2,5,7}) = {3,4,6}. Here rules are labelled as follows: 1: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) 2: activate#(X) -> c_2() 3: activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) 4: activate#(n__from(X)) -> c_4(from#(X)) 5: cons#(X1,X2) -> c_5() 6: from#(X) -> c_6(cons#(X,n__from(s(X)))) 7: from#(X) -> c_7() * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) from#(X) -> c_6(cons#(X,n__from(s(X)))) - Weak DPs: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) activate#(X) -> c_2() cons#(X1,X2) -> c_5() from#(X) -> c_7() - Weak TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1,2nd#/1,activate#/1,cons#/2,from#/1} / {n__cons/2,n__from/1,s/1,c_1/1,c_2/0 ,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,activate#,cons#,from#} and constructors {n__cons ,n__from,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3} by application of Pre({1,3}) = {2}. Here rules are labelled as follows: 1: activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) 2: activate#(n__from(X)) -> c_4(from#(X)) 3: from#(X) -> c_6(cons#(X,n__from(s(X)))) 4: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) 5: activate#(X) -> c_2() 6: cons#(X1,X2) -> c_5() 7: from#(X) -> c_7() * Step 5: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: activate#(n__from(X)) -> c_4(from#(X)) - Weak DPs: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) activate#(X) -> c_2() activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) cons#(X1,X2) -> c_5() from#(X) -> c_6(cons#(X,n__from(s(X)))) from#(X) -> c_7() - Weak TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1,2nd#/1,activate#/1,cons#/2,from#/1} / {n__cons/2,n__from/1,s/1,c_1/1,c_2/0 ,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,activate#,cons#,from#} and constructors {n__cons ,n__from,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: activate#(n__from(X)) -> c_4(from#(X)) 2: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) 3: activate#(X) -> c_2() 4: activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) 5: cons#(X1,X2) -> c_5() 6: from#(X) -> c_6(cons#(X,n__from(s(X)))) 7: from#(X) -> c_7() * Step 6: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) activate#(X) -> c_2() activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) cons#(X1,X2) -> c_5() from#(X) -> c_6(cons#(X,n__from(s(X)))) from#(X) -> c_7() - Weak TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1,2nd#/1,activate#/1,cons#/2,from#/1} / {n__cons/2,n__from/1,s/1,c_1/1,c_2/0 ,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,activate#,cons#,from#} and constructors {n__cons ,n__from,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) 2:W:activate#(X) -> c_2() 3:W:activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) -->_1 cons#(X1,X2) -> c_5():5 4:W:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_6(cons#(X,n__from(s(X)))):6 -->_1 from#(X) -> c_7():7 5:W:cons#(X1,X2) -> c_5() 6:W:from#(X) -> c_6(cons#(X,n__from(s(X)))) -->_1 cons#(X1,X2) -> c_5():5 7:W:from#(X) -> c_7() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: activate#(n__from(X)) -> c_4(from#(X)) 7: from#(X) -> c_7() 6: from#(X) -> c_6(cons#(X,n__from(s(X)))) 3: activate#(n__cons(X1,X2)) -> c_3(cons#(X1,X2)) 5: cons#(X1,X2) -> c_5() 2: activate#(X) -> c_2() 1: 2nd#(cons(X,n__cons(Y,Z))) -> c_1(activate#(Y)) * Step 7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 2nd(cons(X,n__cons(Y,Z))) -> activate(Y) activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__from(X)) -> from(X) cons(X1,X2) -> n__cons(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) - Signature: {2nd/1,activate/1,cons/2,from/1,2nd#/1,activate#/1,cons#/2,from#/1} / {n__cons/2,n__from/1,s/1,c_1/1,c_2/0 ,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,activate#,cons#,from#} and constructors {n__cons ,n__from,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))