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