WORST_CASE(?,O(n^1)) * Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease,goal,number42} and constructors {Cons,Nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) decrease#(Nil()) -> c_2(number42#(Nil())) goal#(x) -> c_3(decrease#(x)) number42#(x) -> c_4() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) decrease#(Nil()) -> c_2(number42#(Nil())) goal#(x) -> c_3(decrease#(x)) number42#(x) -> c_4() - Weak TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4} by application of Pre({4}) = {2}. Here rules are labelled as follows: 1: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) 2: decrease#(Nil()) -> c_2(number42#(Nil())) 3: goal#(x) -> c_3(decrease#(x)) 4: number42#(x) -> c_4() * Step 3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) decrease#(Nil()) -> c_2(number42#(Nil())) goal#(x) -> c_3(decrease#(x)) - Weak DPs: number42#(x) -> c_4() - Weak TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {1,3}. Here rules are labelled as follows: 1: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) 2: decrease#(Nil()) -> c_2(number42#(Nil())) 3: goal#(x) -> c_3(decrease#(x)) 4: number42#(x) -> c_4() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) goal#(x) -> c_3(decrease#(x)) - Weak DPs: decrease#(Nil()) -> c_2(number42#(Nil())) number42#(x) -> c_4() - Weak TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) -->_1 decrease#(Nil()) -> c_2(number42#(Nil())):3 -->_1 decrease#(Cons(x,xs)) -> c_1(decrease#(xs)):1 2:S:goal#(x) -> c_3(decrease#(x)) -->_1 decrease#(Nil()) -> c_2(number42#(Nil())):3 -->_1 decrease#(Cons(x,xs)) -> c_1(decrease#(xs)):1 3:W:decrease#(Nil()) -> c_2(number42#(Nil())) -->_1 number42#(x) -> c_4():4 4:W:number42#(x) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: decrease#(Nil()) -> c_2(number42#(Nil())) 4: number42#(x) -> c_4() * Step 5: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) goal#(x) -> c_3(decrease#(x)) - Weak TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) -->_1 decrease#(Cons(x,xs)) -> c_1(decrease#(xs)):1 2:S:goal#(x) -> c_3(decrease#(x)) -->_1 decrease#(Cons(x,xs)) -> c_1(decrease#(xs)):1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(2,goal#(x) -> c_3(decrease#(x)))] * Step 6: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) - Weak TRS: decrease(Cons(x,xs)) -> decrease(xs) decrease(Nil()) -> number42(Nil()) goal(x) -> decrease(x) number42(x) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) * Step 7: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [3] p(Nil) = [0] p(decrease) = [0] p(goal) = [0] p(number42) = [0] p(decrease#) = [7] x1 + [2] p(goal#) = [0] p(number42#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] Following rules are strictly oriented: decrease#(Cons(x,xs)) = [7] x + [7] xs + [23] > [7] xs + [2] = c_1(decrease#(xs)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: decrease#(Cons(x,xs)) -> c_1(decrease#(xs)) - Signature: {decrease/1,goal/1,number42/1,decrease#/1,goal#/1,number42#/1} / {Cons/2,Nil/0,c_1/1,c_2/1,c_3/1,c_4/0} - Obligation: innermost runtime complexity wrt. defined symbols {decrease#,goal#,number42#} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))