MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) eq(X,Y) -> false() eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1 ,n__take/2,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,eq,inf,length,s,take} and constructors {cons ,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. take(0(),X) -> nil() take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L))) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) eq(X,Y) -> false() eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1 ,n__take/2,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,eq,inf,length,s,take} and constructors {cons ,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) eq(X,Y) -> false() eq(n__0(),n__0()) -> true() eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y)) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,8,9,12,13,16,17} by application of Pre({1,2,8,9,12,13,16,17}) = {3,4,5,6,7,10,11,14,15}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: activate#(X) -> c_2() 3: activate#(n__0()) -> c_3(0#()) 4: activate#(n__inf(X)) -> c_4(inf#(X)) 5: activate#(n__length(X)) -> c_5(length#(X)) 6: activate#(n__s(X)) -> c_6(s#(X)) 7: activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) 8: eq#(X,Y) -> c_8() 9: eq#(n__0(),n__0()) -> c_9() 10: eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) 11: inf#(X) -> c_11(s#(X)) 12: inf#(X) -> c_12() 13: length#(X) -> c_13() 14: length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) 15: length#(nil()) -> c_15(0#()) 16: s#(X) -> c_16() 17: take#(X1,X2) -> c_17() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) inf#(X) -> c_11(s#(X)) length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) length#(nil()) -> c_15(0#()) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() inf#(X) -> c_12() length#(X) -> c_13() s#(X) -> c_16() take#(X1,X2) -> c_17() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,5,7,9} by application of Pre({1,4,5,7,9}) = {2,3,6,8}. Here rules are labelled as follows: 1: activate#(n__0()) -> c_3(0#()) 2: activate#(n__inf(X)) -> c_4(inf#(X)) 3: activate#(n__length(X)) -> c_5(length#(X)) 4: activate#(n__s(X)) -> c_6(s#(X)) 5: activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) 6: eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) 7: inf#(X) -> c_11(s#(X)) 8: length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) 9: length#(nil()) -> c_15(0#()) 10: 0#() -> c_1() 11: activate#(X) -> c_2() 12: eq#(X,Y) -> c_8() 13: eq#(n__0(),n__0()) -> c_9() 14: inf#(X) -> c_12() 15: length#(X) -> c_13() 16: s#(X) -> c_16() 17: take#(X1,X2) -> c_17() * Step 6: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__length(X)) -> c_5(length#(X)) eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {3,4}. Here rules are labelled as follows: 1: activate#(n__inf(X)) -> c_4(inf#(X)) 2: activate#(n__length(X)) -> c_5(length#(X)) 3: eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) 4: length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) 5: 0#() -> c_1() 6: activate#(X) -> c_2() 7: activate#(n__0()) -> c_3(0#()) 8: activate#(n__s(X)) -> c_6(s#(X)) 9: activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) 10: eq#(X,Y) -> c_8() 11: eq#(n__0(),n__0()) -> c_9() 12: inf#(X) -> c_11(s#(X)) 13: inf#(X) -> c_12() 14: length#(X) -> c_13() 15: length#(nil()) -> c_15(0#()) 16: s#(X) -> c_16() 17: take#(X1,X2) -> c_17() * Step 7: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__length(X)) -> c_5(length#(X)) eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__inf(X)) -> c_4(inf#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() inf#(X) -> c_11(s#(X)) inf#(X) -> c_12() length#(X) -> c_13() length#(nil()) -> c_15(0#()) s#(X) -> c_16() take#(X1,X2) -> c_17() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__length(X)) -> c_5(length#(X)) -->_1 length#(nil()) -> c_15(0#()):15 -->_1 length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)):3 -->_1 length#(X) -> c_13():14 2:S:eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) -->_3 activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)):9 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)):9 -->_3 activate#(n__s(X)) -> c_6(s#(X)):8 -->_2 activate#(n__s(X)) -> c_6(s#(X)):8 -->_3 activate#(n__inf(X)) -> c_4(inf#(X)):7 -->_2 activate#(n__inf(X)) -> c_4(inf#(X)):7 -->_3 activate#(n__0()) -> c_3(0#()):6 -->_2 activate#(n__0()) -> c_3(0#()):6 -->_1 eq#(n__0(),n__0()) -> c_9():11 -->_1 eq#(X,Y) -> c_8():10 -->_3 activate#(X) -> c_2():5 -->_2 activate#(X) -> c_2():5 -->_1 eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)):2 -->_3 activate#(n__length(X)) -> c_5(length#(X)):1 -->_2 activate#(n__length(X)) -> c_5(length#(X)):1 3:S:length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) -->_2 activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)):9 -->_2 activate#(n__s(X)) -> c_6(s#(X)):8 -->_2 activate#(n__inf(X)) -> c_4(inf#(X)):7 -->_2 activate#(n__0()) -> c_3(0#()):6 -->_1 s#(X) -> c_16():16 -->_2 activate#(X) -> c_2():5 -->_2 activate#(n__length(X)) -> c_5(length#(X)):1 4:W:0#() -> c_1() 5:W:activate#(X) -> c_2() 6:W:activate#(n__0()) -> c_3(0#()) -->_1 0#() -> c_1():4 7:W:activate#(n__inf(X)) -> c_4(inf#(X)) -->_1 inf#(X) -> c_11(s#(X)):12 -->_1 inf#(X) -> c_12():13 8:W:activate#(n__s(X)) -> c_6(s#(X)) -->_1 s#(X) -> c_16():16 9:W:activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) -->_1 take#(X1,X2) -> c_17():17 10:W:eq#(X,Y) -> c_8() 11:W:eq#(n__0(),n__0()) -> c_9() 12:W:inf#(X) -> c_11(s#(X)) -->_1 s#(X) -> c_16():16 13:W:inf#(X) -> c_12() 14:W:length#(X) -> c_13() 15:W:length#(nil()) -> c_15(0#()) -->_1 0#() -> c_1():4 16:W:s#(X) -> c_16() 17:W:take#(X1,X2) -> c_17() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: eq#(X,Y) -> c_8() 11: eq#(n__0(),n__0()) -> c_9() 14: length#(X) -> c_13() 5: activate#(X) -> c_2() 6: activate#(n__0()) -> c_3(0#()) 7: activate#(n__inf(X)) -> c_4(inf#(X)) 13: inf#(X) -> c_12() 12: inf#(X) -> c_11(s#(X)) 8: activate#(n__s(X)) -> c_6(s#(X)) 16: s#(X) -> c_16() 9: activate#(n__take(X1,X2)) -> c_7(take#(X1,X2)) 17: take#(X1,X2) -> c_17() 15: length#(nil()) -> c_15(0#()) 4: 0#() -> c_1() * Step 8: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__length(X)) -> c_5(length#(X)) eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/2,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__length(X)) -> c_5(length#(X)) -->_1 length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)):3 2:S:eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) -->_1 eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)):2 -->_3 activate#(n__length(X)) -> c_5(length#(X)):1 -->_2 activate#(n__length(X)) -> c_5(length#(X)):1 3:S:length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) -->_2 activate#(n__length(X)) -> c_5(length#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: length#(cons(X,L)) -> c_14(activate#(L)) * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__length(X)) -> c_5(length#(X)) eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) length#(cons(X,L)) -> c_14(activate#(L)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(X) activate(n__length(X)) -> length(X) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) inf(X) -> cons(X,n__inf(s(X))) inf(X) -> n__inf(X) length(X) -> n__length(X) length(cons(X,L)) -> s(n__length(activate(L))) length(nil()) -> 0() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Signature: {0/0,activate/1,eq/2,inf/1,length/1,s/1,take/2,0#/0,activate#/1,eq#/2,inf#/1,length#/1,s#/1 ,take#/2} / {cons/2,false/0,n__0/0,n__inf/1,n__length/1,n__s/1,n__take/2,nil/0,true/0,c_1/0,c_2/0,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/3,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,eq#,inf#,length#,s# ,take#} and constructors {cons,false,n__0,n__inf,n__length,n__s,n__take,nil,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE