MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,cons/2,eq/2,inf/1,length/1,proper/1,s/1,take/2,top/1} / {0/0,false/0,mark/1,nil/0,ok/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {active,cons,eq,inf,length,proper,s,take ,top} and constructors {0,false,mark,nil,ok,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs active#(eq(X,Y)) -> c_1() active#(eq(0(),0())) -> c_2() active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(length(nil())) -> c_8() active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(0(),X)) -> c_11() active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(0()) -> c_19() proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(false()) -> c_22() proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(nil()) -> c_25() proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(true()) -> c_28() s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: active#(eq(X,Y)) -> c_1() active#(eq(0(),0())) -> c_2() active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(length(nil())) -> c_8() active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(0(),X)) -> c_11() active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(0()) -> c_19() proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(false()) -> c_22() proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(nil()) -> c_25() proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(true()) -> c_28() s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) - Weak TRS: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,cons/2,eq/2,inf/1,length/1,proper/1,s/1,take/2,top/1,active#/1,cons#/2,eq#/2,inf#/1,length#/1 ,proper#/1,s#/1,take#/2,top#/1} / {0/0,false/0,mark/1,nil/0,ok/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/3,c_6/2 ,c_7/2,c_8/0,c_9/2,c_10/2,c_11/0,c_12/2,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/3,c_21/3 ,c_22/0,c_23/2,c_24/2,c_25/0,c_26/2,c_27/3,c_28/0,c_29/1,c_30/1,c_31/1,c_32/1,c_33/2,c_34/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,eq#,inf#,length#,proper#,s#,take# ,top#} and constructors {0,false,mark,nil,ok,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) active#(eq(X,Y)) -> c_1() active#(eq(0(),0())) -> c_2() active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(length(nil())) -> c_8() active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(0(),X)) -> c_11() active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(0()) -> c_19() proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(false()) -> c_22() proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(nil()) -> c_25() proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(true()) -> c_28() s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: active#(eq(X,Y)) -> c_1() active#(eq(0(),0())) -> c_2() active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(length(nil())) -> c_8() active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(0(),X)) -> c_11() active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(0()) -> c_19() proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(false()) -> c_22() proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(nil()) -> c_25() proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(true()) -> c_28() s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) - Weak TRS: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) - Signature: {active/1,cons/2,eq/2,inf/1,length/1,proper/1,s/1,take/2,top/1,active#/1,cons#/2,eq#/2,inf#/1,length#/1 ,proper#/1,s#/1,take#/2,top#/1} / {0/0,false/0,mark/1,nil/0,ok/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/3,c_6/2 ,c_7/2,c_8/0,c_9/2,c_10/2,c_11/0,c_12/2,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/3,c_21/3 ,c_22/0,c_23/2,c_24/2,c_25/0,c_26/2,c_27/3,c_28/0,c_29/1,c_30/1,c_31/1,c_32/1,c_33/2,c_34/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,eq#,inf#,length#,proper#,s#,take# ,top#} and constructors {0,false,mark,nil,ok,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,8,11,19,22,25,28} by application of Pre({1,2,8,11,19,22,25,28}) = {4,6,9,10,20,21,23,24,26,27,33,34}. Here rules are labelled as follows: 1: active#(eq(X,Y)) -> c_1() 2: active#(eq(0(),0())) -> c_2() 3: active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) 4: active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) 5: active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) 6: active#(length(X)) -> c_6(length#(active(X)),active#(X)) 7: active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) 8: active#(length(nil())) -> c_8() 9: active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) 10: active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) 11: active#(take(0(),X)) -> c_11() 12: active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) 13: cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) 14: eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) 15: inf#(mark(X)) -> c_15(inf#(X)) 16: inf#(ok(X)) -> c_16(inf#(X)) 17: length#(mark(X)) -> c_17(length#(X)) 18: length#(ok(X)) -> c_18(length#(X)) 19: proper#(0()) -> c_19() 20: proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 21: proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 22: proper#(false()) -> c_22() 23: proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) 24: proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) 25: proper#(nil()) -> c_25() 26: proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) 27: proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 28: proper#(true()) -> c_28() 29: s#(ok(X)) -> c_29(s#(X)) 30: take#(X1,mark(X2)) -> c_30(take#(X1,X2)) 31: take#(mark(X1),X2) -> c_31(take#(X1,X2)) 32: take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) 33: top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) 34: top#(ok(X)) -> c_34(top#(active(X)),active#(X)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) - Weak DPs: active#(eq(X,Y)) -> c_1() active#(eq(0(),0())) -> c_2() active#(length(nil())) -> c_8() active#(take(0(),X)) -> c_11() proper#(0()) -> c_19() proper#(false()) -> c_22() proper#(nil()) -> c_25() proper#(true()) -> c_28() - Weak TRS: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) - Signature: {active/1,cons/2,eq/2,inf/1,length/1,proper/1,s/1,take/2,top/1,active#/1,cons#/2,eq#/2,inf#/1,length#/1 ,proper#/1,s#/1,take#/2,top#/1} / {0/0,false/0,mark/1,nil/0,ok/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/3,c_6/2 ,c_7/2,c_8/0,c_9/2,c_10/2,c_11/0,c_12/2,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/3,c_21/3 ,c_22/0,c_23/2,c_24/2,c_25/0,c_26/2,c_27/3,c_28/0,c_29/1,c_30/1,c_31/1,c_32/1,c_33/2,c_34/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,eq#,inf#,length#,proper#,s#,take# ,top#} and constructors {0,false,mark,nil,ok,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) -->_1 eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)):10 2:S:active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) -->_1 inf#(ok(X)) -> c_16(inf#(X)):12 -->_1 inf#(mark(X)) -> c_15(inf#(X)):11 -->_2 active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)):8 -->_2 active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)):7 -->_2 active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)):6 -->_2 active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)):5 -->_2 active#(length(X)) -> c_6(length#(active(X)),active#(X)):4 -->_2 active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)):3 -->_2 active#(take(0(),X)) -> c_11():30 -->_2 active#(length(nil())) -> c_8():29 -->_2 active#(eq(0(),0())) -> c_2():28 -->_2 active#(eq(X,Y)) -> c_1():27 -->_2 active#(inf(X)) -> c_4(inf#(active(X)),active#(X)):2 -->_2 active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)):1 3:S:active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) -->_3 s#(ok(X)) -> c_29(s#(X)):21 -->_2 inf#(ok(X)) -> c_16(inf#(X)):12 -->_2 inf#(mark(X)) -> c_15(inf#(X)):11 -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):9 4:S:active#(length(X)) -> c_6(length#(active(X)),active#(X)) -->_1 length#(ok(X)) -> c_18(length#(X)):14 -->_1 length#(mark(X)) -> c_17(length#(X)):13 -->_2 active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)):8 -->_2 active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)):7 -->_2 active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)):6 -->_2 active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)):5 -->_2 active#(take(0(),X)) -> c_11():30 -->_2 active#(length(nil())) -> c_8():29 -->_2 active#(eq(0(),0())) -> c_2():28 -->_2 active#(eq(X,Y)) -> c_1():27 -->_2 active#(length(X)) -> c_6(length#(active(X)),active#(X)):4 -->_2 active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)):3 -->_2 active#(inf(X)) -> c_4(inf#(active(X)),active#(X)):2 -->_2 active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)):1 5:S:active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) -->_1 s#(ok(X)) -> c_29(s#(X)):21 -->_2 length#(ok(X)) -> c_18(length#(X)):14 -->_2 length#(mark(X)) -> c_17(length#(X)):13 6:S:active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 -->_2 active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)):8 -->_2 active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)):7 -->_2 active#(take(0(),X)) -> c_11():30 -->_2 active#(length(nil())) -> c_8():29 -->_2 active#(eq(0(),0())) -> c_2():28 -->_2 active#(eq(X,Y)) -> c_1():27 -->_2 active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)):6 -->_2 active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)):5 -->_2 active#(length(X)) -> c_6(length#(active(X)),active#(X)):4 -->_2 active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)):3 -->_2 active#(inf(X)) -> c_4(inf#(active(X)),active#(X)):2 -->_2 active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)):1 7:S:active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 -->_2 active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)):8 -->_2 active#(take(0(),X)) -> c_11():30 -->_2 active#(length(nil())) -> c_8():29 -->_2 active#(eq(0(),0())) -> c_2():28 -->_2 active#(eq(X,Y)) -> c_1():27 -->_2 active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)):7 -->_2 active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)):6 -->_2 active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)):5 -->_2 active#(length(X)) -> c_6(length#(active(X)),active#(X)):4 -->_2 active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)):3 -->_2 active#(inf(X)) -> c_4(inf#(active(X)),active#(X)):2 -->_2 active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)):1 8:S:active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) -->_2 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_2 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_2 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):9 9:S:cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):9 10:S:eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) -->_1 eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)):10 11:S:inf#(mark(X)) -> c_15(inf#(X)) -->_1 inf#(ok(X)) -> c_16(inf#(X)):12 -->_1 inf#(mark(X)) -> c_15(inf#(X)):11 12:S:inf#(ok(X)) -> c_16(inf#(X)) -->_1 inf#(ok(X)) -> c_16(inf#(X)):12 -->_1 inf#(mark(X)) -> c_15(inf#(X)):11 13:S:length#(mark(X)) -> c_17(length#(X)) -->_1 length#(ok(X)) -> c_18(length#(X)):14 -->_1 length#(mark(X)) -> c_17(length#(X)):13 14:S:length#(ok(X)) -> c_18(length#(X)) -->_1 length#(ok(X)) -> c_18(length#(X)):14 -->_1 length#(mark(X)) -> c_17(length#(X)):13 15:S:proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_3 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_3 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_3 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_3 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_3 proper#(true()) -> c_28():34 -->_2 proper#(true()) -> c_28():34 -->_3 proper#(nil()) -> c_25():33 -->_2 proper#(nil()) -> c_25():33 -->_3 proper#(false()) -> c_22():32 -->_2 proper#(false()) -> c_22():32 -->_3 proper#(0()) -> c_19():31 -->_2 proper#(0()) -> c_19():31 -->_3 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):9 16:S:proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_3 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_3 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_3 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_3 proper#(true()) -> c_28():34 -->_2 proper#(true()) -> c_28():34 -->_3 proper#(nil()) -> c_25():33 -->_2 proper#(nil()) -> c_25():33 -->_3 proper#(false()) -> c_22():32 -->_2 proper#(false()) -> c_22():32 -->_3 proper#(0()) -> c_19():31 -->_2 proper#(0()) -> c_19():31 -->_3 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_3 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)):10 17:S:proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(true()) -> c_28():34 -->_2 proper#(nil()) -> c_25():33 -->_2 proper#(false()) -> c_22():32 -->_2 proper#(0()) -> c_19():31 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 inf#(ok(X)) -> c_16(inf#(X)):12 -->_1 inf#(mark(X)) -> c_15(inf#(X)):11 18:S:proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(true()) -> c_28():34 -->_2 proper#(nil()) -> c_25():33 -->_2 proper#(false()) -> c_22():32 -->_2 proper#(0()) -> c_19():31 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 length#(ok(X)) -> c_18(length#(X)):14 -->_1 length#(mark(X)) -> c_17(length#(X)):13 19:S:proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_29(s#(X)):21 -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(true()) -> c_28():34 -->_2 proper#(nil()) -> c_25():33 -->_2 proper#(false()) -> c_22():32 -->_2 proper#(0()) -> c_19():31 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 20:S:proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 -->_3 proper#(true()) -> c_28():34 -->_2 proper#(true()) -> c_28():34 -->_3 proper#(nil()) -> c_25():33 -->_2 proper#(nil()) -> c_25():33 -->_3 proper#(false()) -> c_22():32 -->_2 proper#(false()) -> c_22():32 -->_3 proper#(0()) -> c_19():31 -->_2 proper#(0()) -> c_19():31 -->_3 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_3 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_3 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_3 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_3 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_3 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 21:S:s#(ok(X)) -> c_29(s#(X)) -->_1 s#(ok(X)) -> c_29(s#(X)):21 22:S:take#(X1,mark(X2)) -> c_30(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 23:S:take#(mark(X1),X2) -> c_31(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 24:S:take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) -->_1 take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)):24 -->_1 take#(mark(X1),X2) -> c_31(take#(X1,X2)):23 -->_1 take#(X1,mark(X2)) -> c_30(take#(X1,X2)):22 25:S:top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_34(top#(active(X)),active#(X)):26 -->_2 proper#(true()) -> c_28():34 -->_2 proper#(nil()) -> c_25():33 -->_2 proper#(false()) -> c_22():32 -->_2 proper#(0()) -> c_19():31 -->_1 top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)):25 -->_2 proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)):19 -->_2 proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)):18 -->_2 proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)):17 -->_2 proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 26:S:top#(ok(X)) -> c_34(top#(active(X)),active#(X)) -->_2 active#(take(0(),X)) -> c_11():30 -->_2 active#(length(nil())) -> c_8():29 -->_2 active#(eq(0(),0())) -> c_2():28 -->_2 active#(eq(X,Y)) -> c_1():27 -->_1 top#(ok(X)) -> c_34(top#(active(X)),active#(X)):26 -->_1 top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)):25 -->_2 active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)):8 -->_2 active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)):7 -->_2 active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)):6 -->_2 active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)):5 -->_2 active#(length(X)) -> c_6(length#(active(X)),active#(X)):4 -->_2 active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)):3 -->_2 active#(inf(X)) -> c_4(inf#(active(X)),active#(X)):2 -->_2 active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)):1 27:W:active#(eq(X,Y)) -> c_1() 28:W:active#(eq(0(),0())) -> c_2() 29:W:active#(length(nil())) -> c_8() 30:W:active#(take(0(),X)) -> c_11() 31:W:proper#(0()) -> c_19() 32:W:proper#(false()) -> c_22() 33:W:proper#(nil()) -> c_25() 34:W:proper#(true()) -> c_28() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 31: proper#(0()) -> c_19() 32: proper#(false()) -> c_22() 33: proper#(nil()) -> c_25() 34: proper#(true()) -> c_28() 27: active#(eq(X,Y)) -> c_1() 28: active#(eq(0(),0())) -> c_2() 29: active#(length(nil())) -> c_8() 30: active#(take(0(),X)) -> c_11() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: active#(eq(s(X),s(Y))) -> c_3(eq#(X,Y)) active#(inf(X)) -> c_4(inf#(active(X)),active#(X)) active#(inf(X)) -> c_5(cons#(X,inf(s(X))),inf#(s(X)),s#(X)) active#(length(X)) -> c_6(length#(active(X)),active#(X)) active#(length(cons(X,L))) -> c_7(s#(length(L)),length#(L)) active#(take(X1,X2)) -> c_9(take#(X1,active(X2)),active#(X2)) active#(take(X1,X2)) -> c_10(take#(active(X1),X2),active#(X1)) active#(take(s(X),cons(Y,L))) -> c_12(cons#(Y,take(X,L)),take#(X,L)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) eq#(ok(X1),ok(X2)) -> c_14(eq#(X1,X2)) inf#(mark(X)) -> c_15(inf#(X)) inf#(ok(X)) -> c_16(inf#(X)) length#(mark(X)) -> c_17(length#(X)) length#(ok(X)) -> c_18(length#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(eq(X1,X2)) -> c_21(eq#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(inf(X)) -> c_23(inf#(proper(X)),proper#(X)) proper#(length(X)) -> c_24(length#(proper(X)),proper#(X)) proper#(s(X)) -> c_26(s#(proper(X)),proper#(X)) proper#(take(X1,X2)) -> c_27(take#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(ok(X)) -> c_29(s#(X)) take#(X1,mark(X2)) -> c_30(take#(X1,X2)) take#(mark(X1),X2) -> c_31(take#(X1,X2)) take#(ok(X1),ok(X2)) -> c_32(take#(X1,X2)) top#(mark(X)) -> c_33(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_34(top#(active(X)),active#(X)) - Weak TRS: active(eq(X,Y)) -> mark(false()) active(eq(0(),0())) -> mark(true()) active(eq(s(X),s(Y))) -> mark(eq(X,Y)) active(inf(X)) -> inf(active(X)) active(inf(X)) -> mark(cons(X,inf(s(X)))) active(length(X)) -> length(active(X)) active(length(cons(X,L))) -> mark(s(length(L))) active(length(nil())) -> mark(0()) active(take(X1,X2)) -> take(X1,active(X2)) active(take(X1,X2)) -> take(active(X1),X2) active(take(0(),X)) -> mark(nil()) active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L))) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) eq(ok(X1),ok(X2)) -> ok(eq(X1,X2)) inf(mark(X)) -> mark(inf(X)) inf(ok(X)) -> ok(inf(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(eq(X1,X2)) -> eq(proper(X1),proper(X2)) proper(false()) -> ok(false()) proper(inf(X)) -> inf(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(take(X1,X2)) -> take(proper(X1),proper(X2)) proper(true()) -> ok(true()) s(ok(X)) -> ok(s(X)) take(X1,mark(X2)) -> mark(take(X1,X2)) take(mark(X1),X2) -> mark(take(X1,X2)) take(ok(X1),ok(X2)) -> ok(take(X1,X2)) - Signature: {active/1,cons/2,eq/2,inf/1,length/1,proper/1,s/1,take/2,top/1,active#/1,cons#/2,eq#/2,inf#/1,length#/1 ,proper#/1,s#/1,take#/2,top#/1} / {0/0,false/0,mark/1,nil/0,ok/1,true/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/3,c_6/2 ,c_7/2,c_8/0,c_9/2,c_10/2,c_11/0,c_12/2,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/3,c_21/3 ,c_22/0,c_23/2,c_24/2,c_25/0,c_26/2,c_27/3,c_28/0,c_29/1,c_30/1,c_31/1,c_32/1,c_33/2,c_34/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,eq#,inf#,length#,proper#,s#,take# ,top#} and constructors {0,false,mark,nil,ok,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE