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