MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: goal(x) -> increase(x) increase(Cons(x,xs)) -> increase(Cons(Cons(Nil(),Nil()),Cons(x,xs))) increase(Nil()) -> number42(Nil()) 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: {goal/1,increase/1,number42/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal,increase,number42} and constructors {Cons,Nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) increase#(Nil()) -> c_3(number42#(Nil())) number42#(x) -> c_4() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) increase#(Nil()) -> c_3(number42#(Nil())) number42#(x) -> c_4() - Weak TRS: goal(x) -> increase(x) increase(Cons(x,xs)) -> increase(Cons(Cons(Nil(),Nil()),Cons(x,xs))) increase(Nil()) -> number42(Nil()) 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: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,number42#} and constructors {Cons,Nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) increase#(Nil()) -> c_3(number42#(Nil())) number42#(x) -> c_4() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) increase#(Nil()) -> c_3(number42#(Nil())) number42#(x) -> c_4() - Signature: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,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}) = {3}. Here rules are labelled as follows: 1: goal#(x) -> c_1(increase#(x)) 2: increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) 3: increase#(Nil()) -> c_3(number42#(Nil())) 4: number42#(x) -> c_4() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) increase#(Nil()) -> c_3(number42#(Nil())) - Weak DPs: number42#(x) -> c_4() - Signature: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,number42#} and constructors {Cons,Nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3} by application of Pre({3}) = {1}. Here rules are labelled as follows: 1: goal#(x) -> c_1(increase#(x)) 2: increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) 3: increase#(Nil()) -> c_3(number42#(Nil())) 4: number42#(x) -> c_4() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) - Weak DPs: increase#(Nil()) -> c_3(number42#(Nil())) number42#(x) -> c_4() - Signature: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,number42#} and constructors {Cons,Nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:goal#(x) -> c_1(increase#(x)) -->_1 increase#(Nil()) -> c_3(number42#(Nil())):3 -->_1 increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))):2 2:S:increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) -->_1 increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))):2 3:W:increase#(Nil()) -> c_3(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: increase#(Nil()) -> c_3(number42#(Nil())) 4: number42#(x) -> c_4() * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: goal#(x) -> c_1(increase#(x)) increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) - Signature: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,number42#} and constructors {Cons,Nil} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:goal#(x) -> c_1(increase#(x)) -->_1 increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))):2 2:S:increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) -->_1 increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))):2 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). [(1,goal#(x) -> c_1(increase#(x)))] * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: increase#(Cons(x,xs)) -> c_2(increase#(Cons(Cons(Nil(),Nil()),Cons(x,xs)))) - Signature: {goal/1,increase/1,number42/1,goal#/1,increase#/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 {goal#,increase#,number42#} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE