MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__inf(X)) -> inf(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(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(n__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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(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(n__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#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(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() 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#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(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() 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(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(n__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/2,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(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() 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#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(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() 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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/2,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,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,11,12,13,16,17} by application of Pre({1,2,8,9,11,12,13,16,17}) = {3,4,5,6,7,10,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#(activate(X)),activate#(X)) 5: activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) 6: activate#(n__s(X)) -> c_6(s#(X)) 7: activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(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() 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#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 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)) 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_11() 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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/2,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,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,8} by application of Pre({1,4,8}) = {2,3,5,6,7}. Here rules are labelled as follows: 1: activate#(n__0()) -> c_3(0#()) 2: activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)) 3: activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) 4: activate#(n__s(X)) -> c_6(s#(X)) 5: activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) 7: length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) 8: length#(nil()) -> c_15(0#()) 9: 0#() -> c_1() 10: activate#(X) -> c_2() 11: eq#(X,Y) -> c_8() 12: eq#(n__0(),n__0()) -> c_9() 13: inf#(X) -> c_11() 14: inf#(X) -> c_12() 15: length#(X) -> c_13() 16: s#(X) -> c_16() 17: take#(X1,X2) -> c_17() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 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)) eq#(X,Y) -> c_8() eq#(n__0(),n__0()) -> c_9() inf#(X) -> c_11() 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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/2,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,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__inf(X)) -> c_4(inf#(activate(X)),activate#(X)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):9 -->_2 activate#(n__0()) -> c_3(0#()):8 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_1 inf#(X) -> c_12():13 -->_1 inf#(X) -> c_11():12 -->_2 activate#(X) -> c_2():7 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 2:S:activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) -->_1 length#(nil()) -> c_15(0#()):15 -->_2 activate#(n__s(X)) -> c_6(s#(X)):9 -->_2 activate#(n__0()) -> c_3(0#()):8 -->_1 length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)):5 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_1 length#(X) -> c_13():14 -->_2 activate#(X) -> c_2():7 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 3:S:activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__s(X)) -> c_6(s#(X)):9 -->_2 activate#(n__s(X)) -> c_6(s#(X)):9 -->_3 activate#(n__0()) -> c_3(0#()):8 -->_2 activate#(n__0()) -> c_3(0#()):8 -->_1 take#(X1,X2) -> c_17():17 -->_3 activate#(X) -> c_2():7 -->_2 activate#(X) -> c_2():7 -->_3 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 4:S:eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)) -->_3 activate#(n__s(X)) -> c_6(s#(X)):9 -->_2 activate#(n__s(X)) -> c_6(s#(X)):9 -->_3 activate#(n__0()) -> c_3(0#()):8 -->_2 activate#(n__0()) -> c_3(0#()):8 -->_1 eq#(n__0(),n__0()) -> c_9():11 -->_1 eq#(X,Y) -> c_8():10 -->_3 activate#(X) -> c_2():7 -->_2 activate#(X) -> c_2():7 -->_1 eq#(n__s(X),n__s(Y)) -> c_10(eq#(activate(X),activate(Y)),activate#(X),activate#(Y)):4 -->_3 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 5:S:length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) -->_2 activate#(n__s(X)) -> c_6(s#(X)):9 -->_2 activate#(n__0()) -> c_3(0#()):8 -->_1 s#(X) -> c_16():16 -->_2 activate#(X) -> c_2():7 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 6:W:0#() -> c_1() 7:W:activate#(X) -> c_2() 8:W:activate#(n__0()) -> c_3(0#()) -->_1 0#() -> c_1():6 9:W:activate#(n__s(X)) -> c_6(s#(X)) -->_1 s#(X) -> c_16():16 10:W:eq#(X,Y) -> c_8() 11:W:eq#(n__0(),n__0()) -> c_9() 12:W:inf#(X) -> c_11() 13:W:inf#(X) -> c_12() 14:W:length#(X) -> c_13() 15:W:length#(nil()) -> c_15(0#()) -->_1 0#() -> c_1():6 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() 12: inf#(X) -> c_11() 13: inf#(X) -> c_12() 14: length#(X) -> c_13() 15: length#(nil()) -> c_15(0#()) 7: activate#(X) -> c_2() 17: take#(X1,X2) -> c_17() 8: activate#(n__0()) -> c_3(0#()) 6: 0#() -> c_1() 9: activate#(n__s(X)) -> c_6(s#(X)) 16: s#(X) -> c_16() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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/2,c_5/2,c_6/1,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,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__inf(X)) -> c_4(inf#(activate(X)),activate#(X)) -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 2:S:activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) -->_1 length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)):5 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 3:S:activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 4: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)):4 -->_3 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 5:S:length#(cons(X,L)) -> c_14(s#(n__length(activate(L))),activate#(L)) -->_2 activate#(n__take(X1,X2)) -> c_7(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__inf(X)) -> c_4(inf#(activate(X)),activate#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__inf(X)) -> c_4(activate#(X)) activate#(n__take(X1,X2)) -> c_7(activate#(X1),activate#(X2)) length#(cons(X,L)) -> c_14(activate#(L)) * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__inf(X)) -> c_4(activate#(X)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_7(activate#(X1),activate#(X2)) 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(activate(X)) activate(n__length(X)) -> length(activate(X)) activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) inf(X) -> cons(X,n__inf(n__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/2,c_6/1,c_7/2,c_8/0,c_9/0,c_10/3,c_11/0,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