MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) eql(Nil()) -> Nil() goal(x) -> nesteql(x) nesteql(Cons(x,xs)) -> nesteql(eql(Cons(x,xs))) nesteql(Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,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()))))))))))))))))) number17(n) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,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: {eql/1,goal/1,nesteql/1,number17/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql,goal,nesteql,number17} and constructors {Cons,Nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) eql#(Nil()) -> c_2() goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) nesteql#(Nil()) -> c_5() number17#(n) -> c_6() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) eql#(Nil()) -> c_2() goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) nesteql#(Nil()) -> c_5() number17#(n) -> c_6() - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) eql(Nil()) -> Nil() goal(x) -> nesteql(x) nesteql(Cons(x,xs)) -> nesteql(eql(Cons(x,xs))) nesteql(Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,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()))))))))))))))))) number17(n) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,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: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: eql(Cons(x,xs)) -> eql(Cons(x,xs)) eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) eql#(Nil()) -> c_2() goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) nesteql#(Nil()) -> c_5() number17#(n) -> c_6() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) eql#(Nil()) -> c_2() goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) nesteql#(Nil()) -> c_5() number17#(n) -> c_6() - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) - Signature: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,5,6} by application of Pre({2,5,6}) = {3,4}. Here rules are labelled as follows: 1: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) 2: eql#(Nil()) -> c_2() 3: goal#(x) -> c_3(nesteql#(x)) 4: nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) 5: nesteql#(Nil()) -> c_5() 6: number17#(n) -> c_6() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) - Weak DPs: eql#(Nil()) -> c_2() nesteql#(Nil()) -> c_5() number17#(n) -> c_6() - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) - Signature: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) -->_1 eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))):1 2:S:goal#(x) -> c_3(nesteql#(x)) -->_1 nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))):3 -->_1 nesteql#(Nil()) -> c_5():5 3:S:nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) -->_1 nesteql#(Nil()) -> c_5():5 -->_1 nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))):3 -->_2 eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))):1 4:W:eql#(Nil()) -> c_2() 5:W:nesteql#(Nil()) -> c_5() 6:W:number17#(n) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: number17#(n) -> c_6() 4: eql#(Nil()) -> c_2() 5: nesteql#(Nil()) -> c_5() * Step 5: RemoveHeads MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) goal#(x) -> c_3(nesteql#(x)) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) - Signature: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) -->_1 eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))):1 2:S:goal#(x) -> c_3(nesteql#(x)) -->_1 nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))):3 3:S:nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) -->_1 nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))):3 -->_2 eql#(Cons(x,xs)) -> c_1(eql#(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(nesteql#(x)))] * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) - Signature: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(nesteql#) = {1}, uargs(c_1) = {1}, uargs(c_4) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [7] p(Nil) = [0] p(eql) = [0] p(goal) = [0] p(nesteql) = [0] p(number17) = [0] p(eql#) = [0] p(goal#) = [0] p(nesteql#) = [1] x1 + [0] p(number17#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [1] x2 + [0] p(c_5) = [0] p(c_6) = [0] Following rules are strictly oriented: nesteql#(Cons(x,xs)) = [7] > [0] = c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) Following rules are (at-least) weakly oriented: eql#(Cons(x,xs)) = [0] >= [0] = c_1(eql#(Cons(x,xs))) eql(Cons(x,xs)) = [0] >= [0] = eql(Cons(x,xs)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: eql#(Cons(x,xs)) -> c_1(eql#(Cons(x,xs))) - Weak DPs: nesteql#(Cons(x,xs)) -> c_4(nesteql#(eql(Cons(x,xs))),eql#(Cons(x,xs))) - Weak TRS: eql(Cons(x,xs)) -> eql(Cons(x,xs)) - Signature: {eql/1,goal/1,nesteql/1,number17/1,eql#/1,goal#/1,nesteql#/1,number17#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1 ,c_4/2,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {eql#,goal#,nesteql#,number17#} and constructors {Cons ,Nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE