WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: A__EQ(z0,z1) -> c2() A__EQ(z0,z1) -> c3() A__EQ(0(),0()) -> c() A__EQ(s(z0),s(z1)) -> c1(A__EQ(z0,z1)) A__INF(z0) -> c4() A__INF(z0) -> c5() A__LENGTH(z0) -> c11() A__LENGTH(cons(z0,z1)) -> c10() A__LENGTH(nil()) -> c9() A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c21() MARK(eq(z0,z1)) -> c12(A__EQ(z0,z1)) MARK(false()) -> c20() MARK(inf(z0)) -> c13(A__INF(mark(z0)),MARK(z0)) MARK(length(z0)) -> c16(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c22() MARK(s(z0)) -> c19() MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c15(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(true()) -> c18() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ,A__INF,A__LENGTH,A__TAKE,MARK,a__eq,a__inf ,a__length,a__take,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3 ,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__EQ(z0,z1) -> c2() A__EQ(z0,z1) -> c3() A__EQ(0(),0()) -> c() A__EQ(s(z0),s(z1)) -> c1(A__EQ(z0,z1)) A__INF(z0) -> c4() A__INF(z0) -> c5() A__LENGTH(z0) -> c11() A__LENGTH(cons(z0,z1)) -> c10() A__LENGTH(nil()) -> c9() A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c21() MARK(eq(z0,z1)) -> c12(A__EQ(z0,z1)) MARK(false()) -> c20() MARK(inf(z0)) -> c13(A__INF(mark(z0)),MARK(z0)) MARK(length(z0)) -> c16(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c22() MARK(s(z0)) -> c19() MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c15(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(true()) -> c18() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ,A__INF,A__LENGTH,A__TAKE,MARK,a__eq,a__inf ,a__length,a__take,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3 ,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__EQ(z0,z1) -> c2() A__EQ(z0,z1) -> c3() A__EQ(0(),0()) -> c() A__EQ(s(z0),s(z1)) -> c1(A__EQ(z0,z1)) A__INF(z0) -> c4() A__INF(z0) -> c5() A__LENGTH(z0) -> c11() A__LENGTH(cons(z0,z1)) -> c10() A__LENGTH(nil()) -> c9() A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c21() MARK(eq(z0,z1)) -> c12(A__EQ(z0,z1)) MARK(false()) -> c20() MARK(inf(z0)) -> c13(A__INF(mark(z0)),MARK(z0)) MARK(length(z0)) -> c16(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c22() MARK(s(z0)) -> c19() MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c15(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(true()) -> c18() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ,A__INF,A__LENGTH,A__TAKE,MARK,a__eq,a__inf ,a__length,a__take,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3 ,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__EQ(x,y){x -> s(x),y -> s(y)} = A__EQ(s(x),s(y)) ->^+ c1(A__EQ(x,y)) = C[A__EQ(x,y) = A__EQ(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: A__EQ(z0,z1) -> c2() A__EQ(z0,z1) -> c3() A__EQ(0(),0()) -> c() A__EQ(s(z0),s(z1)) -> c1(A__EQ(z0,z1)) A__INF(z0) -> c4() A__INF(z0) -> c5() A__LENGTH(z0) -> c11() A__LENGTH(cons(z0,z1)) -> c10() A__LENGTH(nil()) -> c9() A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c21() MARK(eq(z0,z1)) -> c12(A__EQ(z0,z1)) MARK(false()) -> c20() MARK(inf(z0)) -> c13(A__INF(mark(z0)),MARK(z0)) MARK(length(z0)) -> c16(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c22() MARK(s(z0)) -> c19() MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c15(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(true()) -> c18() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ,A__INF,A__LENGTH,A__TAKE,MARK,a__eq,a__inf ,a__length,a__take,mark} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c3 ,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs A__EQ#(z0,z1) -> c_1() A__EQ#(z0,z1) -> c_2() A__EQ#(0(),0()) -> c_3() A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) A__INF#(z0) -> c_5() A__INF#(z0) -> c_6() A__LENGTH#(z0) -> c_7() A__LENGTH#(cons(z0,z1)) -> c_8() A__LENGTH#(nil()) -> c_9() A__TAKE#(z0,z1) -> c_10() A__TAKE#(0(),z0) -> c_11() A__TAKE#(s(z0),cons(z1,z2)) -> c_12() MARK#(0()) -> c_13() MARK#(cons(z0,z1)) -> c_14() MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(false()) -> c_16() MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(nil()) -> c_19() MARK#(s(z0)) -> c_20() MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) MARK#(true()) -> c_23() Weak DPs a__eq#(z0,z1) -> c_24() a__eq#(z0,z1) -> c_25() a__eq#(0(),0()) -> c_26() a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) a__inf#(z0) -> c_28() a__inf#(z0) -> c_29() a__length#(z0) -> c_30() a__length#(cons(z0,z1)) -> c_31() a__length#(nil()) -> c_32() a__take#(z0,z1) -> c_33() a__take#(0(),z0) -> c_34() a__take#(s(z0),cons(z1,z2)) -> c_35() mark#(0()) -> c_36() mark#(cons(z0,z1)) -> c_37() mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) mark#(false()) -> c_39() mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) mark#(length(z0)) -> c_41(a__length#(mark(z0))) mark#(nil()) -> c_42() mark#(s(z0)) -> c_43() mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) mark#(true()) -> c_45() and mark the set of starting terms. ** Step 1.b:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(z0,z1) -> c_1() A__EQ#(z0,z1) -> c_2() A__EQ#(0(),0()) -> c_3() A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) A__INF#(z0) -> c_5() A__INF#(z0) -> c_6() A__LENGTH#(z0) -> c_7() A__LENGTH#(cons(z0,z1)) -> c_8() A__LENGTH#(nil()) -> c_9() A__TAKE#(z0,z1) -> c_10() A__TAKE#(0(),z0) -> c_11() A__TAKE#(s(z0),cons(z1,z2)) -> c_12() MARK#(0()) -> c_13() MARK#(cons(z0,z1)) -> c_14() MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(false()) -> c_16() MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(nil()) -> c_19() MARK#(s(z0)) -> c_20() MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) MARK#(true()) -> c_23() - Strict TRS: A__EQ(z0,z1) -> c2() A__EQ(z0,z1) -> c3() A__EQ(0(),0()) -> c() A__EQ(s(z0),s(z1)) -> c1(A__EQ(z0,z1)) A__INF(z0) -> c4() A__INF(z0) -> c5() A__LENGTH(z0) -> c11() A__LENGTH(cons(z0,z1)) -> c10() A__LENGTH(nil()) -> c9() A__TAKE(z0,z1) -> c8() A__TAKE(0(),z0) -> c6() A__TAKE(s(z0),cons(z1,z2)) -> c7() MARK(0()) -> c17() MARK(cons(z0,z1)) -> c21() MARK(eq(z0,z1)) -> c12(A__EQ(z0,z1)) MARK(false()) -> c20() MARK(inf(z0)) -> c13(A__INF(mark(z0)),MARK(z0)) MARK(length(z0)) -> c16(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c22() MARK(s(z0)) -> c19() MARK(take(z0,z1)) -> c14(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c15(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(true()) -> c18() - Weak DPs: a__eq#(z0,z1) -> c_24() a__eq#(z0,z1) -> c_25() a__eq#(0(),0()) -> c_26() a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) a__inf#(z0) -> c_28() a__inf#(z0) -> c_29() a__length#(z0) -> c_30() a__length#(cons(z0,z1)) -> c_31() a__length#(nil()) -> c_32() a__take#(z0,z1) -> c_33() a__take#(0(),z0) -> c_34() a__take#(s(z0),cons(z1,z2)) -> c_35() mark#(0()) -> c_36() mark#(cons(z0,z1)) -> c_37() mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) mark#(false()) -> c_39() mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) mark#(length(z0)) -> c_41(a__length#(mark(z0))) mark#(nil()) -> c_42() mark#(s(z0)) -> c_43() mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) mark#(true()) -> c_45() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/2 ,c_22/2,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() A__EQ#(z0,z1) -> c_1() A__EQ#(z0,z1) -> c_2() A__EQ#(0(),0()) -> c_3() A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) A__INF#(z0) -> c_5() A__INF#(z0) -> c_6() A__LENGTH#(z0) -> c_7() A__LENGTH#(cons(z0,z1)) -> c_8() A__LENGTH#(nil()) -> c_9() A__TAKE#(z0,z1) -> c_10() A__TAKE#(0(),z0) -> c_11() A__TAKE#(s(z0),cons(z1,z2)) -> c_12() MARK#(0()) -> c_13() MARK#(cons(z0,z1)) -> c_14() MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(false()) -> c_16() MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(nil()) -> c_19() MARK#(s(z0)) -> c_20() MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) MARK#(true()) -> c_23() a__eq#(z0,z1) -> c_24() a__eq#(z0,z1) -> c_25() a__eq#(0(),0()) -> c_26() a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) a__inf#(z0) -> c_28() a__inf#(z0) -> c_29() a__length#(z0) -> c_30() a__length#(cons(z0,z1)) -> c_31() a__length#(nil()) -> c_32() a__take#(z0,z1) -> c_33() a__take#(0(),z0) -> c_34() a__take#(s(z0),cons(z1,z2)) -> c_35() mark#(0()) -> c_36() mark#(cons(z0,z1)) -> c_37() mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) mark#(false()) -> c_39() mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) mark#(length(z0)) -> c_41(a__length#(mark(z0))) mark#(nil()) -> c_42() mark#(s(z0)) -> c_43() mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) mark#(true()) -> c_45() ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(z0,z1) -> c_1() A__EQ#(z0,z1) -> c_2() A__EQ#(0(),0()) -> c_3() A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) A__INF#(z0) -> c_5() A__INF#(z0) -> c_6() A__LENGTH#(z0) -> c_7() A__LENGTH#(cons(z0,z1)) -> c_8() A__LENGTH#(nil()) -> c_9() A__TAKE#(z0,z1) -> c_10() A__TAKE#(0(),z0) -> c_11() A__TAKE#(s(z0),cons(z1,z2)) -> c_12() MARK#(0()) -> c_13() MARK#(cons(z0,z1)) -> c_14() MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(false()) -> c_16() MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(nil()) -> c_19() MARK#(s(z0)) -> c_20() MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) MARK#(true()) -> c_23() - Weak DPs: a__eq#(z0,z1) -> c_24() a__eq#(z0,z1) -> c_25() a__eq#(0(),0()) -> c_26() a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) a__inf#(z0) -> c_28() a__inf#(z0) -> c_29() a__length#(z0) -> c_30() a__length#(cons(z0,z1)) -> c_31() a__length#(nil()) -> c_32() a__take#(z0,z1) -> c_33() a__take#(0(),z0) -> c_34() a__take#(s(z0),cons(z1,z2)) -> c_35() mark#(0()) -> c_36() mark#(cons(z0,z1)) -> c_37() mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) mark#(false()) -> c_39() mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) mark#(length(z0)) -> c_41(a__length#(mark(z0))) mark#(nil()) -> c_42() mark#(s(z0)) -> c_43() mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) mark#(true()) -> c_45() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/2 ,c_22/2,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,5,6,7,8,9,10,11,12,13,14,16,19,20,23} by application of Pre({1,2,3,5,6,7,8,9,10,11,12,13,14,16,19,20,23}) = {4,15,17,18,21,22}. Here rules are labelled as follows: 1: A__EQ#(z0,z1) -> c_1() 2: A__EQ#(z0,z1) -> c_2() 3: A__EQ#(0(),0()) -> c_3() 4: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) 5: A__INF#(z0) -> c_5() 6: A__INF#(z0) -> c_6() 7: A__LENGTH#(z0) -> c_7() 8: A__LENGTH#(cons(z0,z1)) -> c_8() 9: A__LENGTH#(nil()) -> c_9() 10: A__TAKE#(z0,z1) -> c_10() 11: A__TAKE#(0(),z0) -> c_11() 12: A__TAKE#(s(z0),cons(z1,z2)) -> c_12() 13: MARK#(0()) -> c_13() 14: MARK#(cons(z0,z1)) -> c_14() 15: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) 16: MARK#(false()) -> c_16() 17: MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) 18: MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) 19: MARK#(nil()) -> c_19() 20: MARK#(s(z0)) -> c_20() 21: MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) 22: MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) 23: MARK#(true()) -> c_23() 24: a__eq#(z0,z1) -> c_24() 25: a__eq#(z0,z1) -> c_25() 26: a__eq#(0(),0()) -> c_26() 27: a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) 28: a__inf#(z0) -> c_28() 29: a__inf#(z0) -> c_29() 30: a__length#(z0) -> c_30() 31: a__length#(cons(z0,z1)) -> c_31() 32: a__length#(nil()) -> c_32() 33: a__take#(z0,z1) -> c_33() 34: a__take#(0(),z0) -> c_34() 35: a__take#(s(z0),cons(z1,z2)) -> c_35() 36: mark#(0()) -> c_36() 37: mark#(cons(z0,z1)) -> c_37() 38: mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) 39: mark#(false()) -> c_39() 40: mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) 41: mark#(length(z0)) -> c_41(a__length#(mark(z0))) 42: mark#(nil()) -> c_42() 43: mark#(s(z0)) -> c_43() 44: mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) 45: mark#(true()) -> c_45() ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) - Weak DPs: A__EQ#(z0,z1) -> c_1() A__EQ#(z0,z1) -> c_2() A__EQ#(0(),0()) -> c_3() A__INF#(z0) -> c_5() A__INF#(z0) -> c_6() A__LENGTH#(z0) -> c_7() A__LENGTH#(cons(z0,z1)) -> c_8() A__LENGTH#(nil()) -> c_9() A__TAKE#(z0,z1) -> c_10() A__TAKE#(0(),z0) -> c_11() A__TAKE#(s(z0),cons(z1,z2)) -> c_12() MARK#(0()) -> c_13() MARK#(cons(z0,z1)) -> c_14() MARK#(false()) -> c_16() MARK#(nil()) -> c_19() MARK#(s(z0)) -> c_20() MARK#(true()) -> c_23() a__eq#(z0,z1) -> c_24() a__eq#(z0,z1) -> c_25() a__eq#(0(),0()) -> c_26() a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) a__inf#(z0) -> c_28() a__inf#(z0) -> c_29() a__length#(z0) -> c_30() a__length#(cons(z0,z1)) -> c_31() a__length#(nil()) -> c_32() a__take#(z0,z1) -> c_33() a__take#(0(),z0) -> c_34() a__take#(s(z0),cons(z1,z2)) -> c_35() mark#(0()) -> c_36() mark#(cons(z0,z1)) -> c_37() mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) mark#(false()) -> c_39() mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) mark#(length(z0)) -> c_41(a__length#(mark(z0))) mark#(nil()) -> c_42() mark#(s(z0)) -> c_43() mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) mark#(true()) -> c_45() - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/2 ,c_22/2,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) -->_1 A__EQ#(0(),0()) -> c_3():9 -->_1 A__EQ#(z0,z1) -> c_2():8 -->_1 A__EQ#(z0,z1) -> c_1():7 -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 2:S:MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) -->_1 A__EQ#(0(),0()) -> c_3():9 -->_1 A__EQ#(z0,z1) -> c_2():8 -->_1 A__EQ#(z0,z1) -> c_1():7 -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 3:S:MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(true()) -> c_23():23 -->_2 MARK#(s(z0)) -> c_20():22 -->_2 MARK#(nil()) -> c_19():21 -->_2 MARK#(false()) -> c_16():20 -->_2 MARK#(cons(z0,z1)) -> c_14():19 -->_2 MARK#(0()) -> c_13():18 -->_1 A__INF#(z0) -> c_6():11 -->_1 A__INF#(z0) -> c_5():10 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 4:S:MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(true()) -> c_23():23 -->_2 MARK#(s(z0)) -> c_20():22 -->_2 MARK#(nil()) -> c_19():21 -->_2 MARK#(false()) -> c_16():20 -->_2 MARK#(cons(z0,z1)) -> c_14():19 -->_2 MARK#(0()) -> c_13():18 -->_1 A__LENGTH#(nil()) -> c_9():14 -->_1 A__LENGTH#(cons(z0,z1)) -> c_8():13 -->_1 A__LENGTH#(z0) -> c_7():12 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 5:S:MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(true()) -> c_23():23 -->_2 MARK#(s(z0)) -> c_20():22 -->_2 MARK#(nil()) -> c_19():21 -->_2 MARK#(false()) -> c_16():20 -->_2 MARK#(cons(z0,z1)) -> c_14():19 -->_2 MARK#(0()) -> c_13():18 -->_1 A__TAKE#(s(z0),cons(z1,z2)) -> c_12():17 -->_1 A__TAKE#(0(),z0) -> c_11():16 -->_1 A__TAKE#(z0,z1) -> c_10():15 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 6:S:MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) -->_2 MARK#(true()) -> c_23():23 -->_2 MARK#(s(z0)) -> c_20():22 -->_2 MARK#(nil()) -> c_19():21 -->_2 MARK#(false()) -> c_16():20 -->_2 MARK#(cons(z0,z1)) -> c_14():19 -->_2 MARK#(0()) -> c_13():18 -->_1 A__TAKE#(s(z0),cons(z1,z2)) -> c_12():17 -->_1 A__TAKE#(0(),z0) -> c_11():16 -->_1 A__TAKE#(z0,z1) -> c_10():15 -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 7:W:A__EQ#(z0,z1) -> c_1() 8:W:A__EQ#(z0,z1) -> c_2() 9:W:A__EQ#(0(),0()) -> c_3() 10:W:A__INF#(z0) -> c_5() 11:W:A__INF#(z0) -> c_6() 12:W:A__LENGTH#(z0) -> c_7() 13:W:A__LENGTH#(cons(z0,z1)) -> c_8() 14:W:A__LENGTH#(nil()) -> c_9() 15:W:A__TAKE#(z0,z1) -> c_10() 16:W:A__TAKE#(0(),z0) -> c_11() 17:W:A__TAKE#(s(z0),cons(z1,z2)) -> c_12() 18:W:MARK#(0()) -> c_13() 19:W:MARK#(cons(z0,z1)) -> c_14() 20:W:MARK#(false()) -> c_16() 21:W:MARK#(nil()) -> c_19() 22:W:MARK#(s(z0)) -> c_20() 23:W:MARK#(true()) -> c_23() 24:W:a__eq#(z0,z1) -> c_24() 25:W:a__eq#(z0,z1) -> c_25() 26:W:a__eq#(0(),0()) -> c_26() 27:W:a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) -->_1 a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)):27 -->_1 a__eq#(0(),0()) -> c_26():26 -->_1 a__eq#(z0,z1) -> c_25():25 -->_1 a__eq#(z0,z1) -> c_24():24 28:W:a__inf#(z0) -> c_28() 29:W:a__inf#(z0) -> c_29() 30:W:a__length#(z0) -> c_30() 31:W:a__length#(cons(z0,z1)) -> c_31() 32:W:a__length#(nil()) -> c_32() 33:W:a__take#(z0,z1) -> c_33() 34:W:a__take#(0(),z0) -> c_34() 35:W:a__take#(s(z0),cons(z1,z2)) -> c_35() 36:W:mark#(0()) -> c_36() 37:W:mark#(cons(z0,z1)) -> c_37() 38:W:mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) -->_1 a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)):27 -->_1 a__eq#(0(),0()) -> c_26():26 -->_1 a__eq#(z0,z1) -> c_25():25 -->_1 a__eq#(z0,z1) -> c_24():24 39:W:mark#(false()) -> c_39() 40:W:mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) -->_1 a__inf#(z0) -> c_29():29 -->_1 a__inf#(z0) -> c_28():28 41:W:mark#(length(z0)) -> c_41(a__length#(mark(z0))) -->_1 a__length#(nil()) -> c_32():32 -->_1 a__length#(cons(z0,z1)) -> c_31():31 -->_1 a__length#(z0) -> c_30():30 42:W:mark#(nil()) -> c_42() 43:W:mark#(s(z0)) -> c_43() 44:W:mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) -->_1 a__take#(s(z0),cons(z1,z2)) -> c_35():35 -->_1 a__take#(0(),z0) -> c_34():34 -->_1 a__take#(z0,z1) -> c_33():33 45:W:mark#(true()) -> c_45() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 45: mark#(true()) -> c_45() 44: mark#(take(z0,z1)) -> c_44(a__take#(mark(z0),mark(z1))) 43: mark#(s(z0)) -> c_43() 42: mark#(nil()) -> c_42() 41: mark#(length(z0)) -> c_41(a__length#(mark(z0))) 40: mark#(inf(z0)) -> c_40(a__inf#(mark(z0))) 39: mark#(false()) -> c_39() 38: mark#(eq(z0,z1)) -> c_38(a__eq#(z0,z1)) 37: mark#(cons(z0,z1)) -> c_37() 36: mark#(0()) -> c_36() 35: a__take#(s(z0),cons(z1,z2)) -> c_35() 34: a__take#(0(),z0) -> c_34() 33: a__take#(z0,z1) -> c_33() 32: a__length#(nil()) -> c_32() 31: a__length#(cons(z0,z1)) -> c_31() 30: a__length#(z0) -> c_30() 29: a__inf#(z0) -> c_29() 28: a__inf#(z0) -> c_28() 27: a__eq#(s(z0),s(z1)) -> c_27(a__eq#(z0,z1)) 26: a__eq#(0(),0()) -> c_26() 25: a__eq#(z0,z1) -> c_25() 24: a__eq#(z0,z1) -> c_24() 10: A__INF#(z0) -> c_5() 11: A__INF#(z0) -> c_6() 12: A__LENGTH#(z0) -> c_7() 13: A__LENGTH#(cons(z0,z1)) -> c_8() 14: A__LENGTH#(nil()) -> c_9() 15: A__TAKE#(z0,z1) -> c_10() 16: A__TAKE#(0(),z0) -> c_11() 17: A__TAKE#(s(z0),cons(z1,z2)) -> c_12() 18: MARK#(0()) -> c_13() 19: MARK#(cons(z0,z1)) -> c_14() 20: MARK#(false()) -> c_16() 21: MARK#(nil()) -> c_19() 22: MARK#(s(z0)) -> c_20() 23: MARK#(true()) -> c_23() 7: A__EQ#(z0,z1) -> c_1() 8: A__EQ#(z0,z1) -> c_2() 9: A__EQ#(0(),0()) -> c_3() ** Step 1.b:5: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/0,c_20/0,c_21/2 ,c_22/2,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 2:S:MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 3:S:MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 4:S:MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 5:S:MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 6:S:MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)) -->_2 MARK#(take(z0,z1)) -> c_22(A__TAKE#(mark(z0),mark(z1)),MARK#(z1)):6 -->_2 MARK#(take(z0,z1)) -> c_21(A__TAKE#(mark(z0),mark(z1)),MARK#(z0)):5 -->_2 MARK#(length(z0)) -> c_18(A__LENGTH#(mark(z0)),MARK#(z0)):4 -->_2 MARK#(inf(z0)) -> c_17(A__INF#(mark(z0)),MARK#(z0)):3 -->_2 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) ** Step 1.b:6: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak TRS: a__eq(z0,z1) -> eq(z0,z1) a__eq(z0,z1) -> false() a__eq(0(),0()) -> true() a__eq(s(z0),s(z1)) -> a__eq(z0,z1) a__inf(z0) -> cons(z0,inf(s(z0))) a__inf(z0) -> inf(z0) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> s(length(z1)) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> nil() a__take(s(z0),cons(z1,z2)) -> cons(z1,take(z0,z2)) mark(0()) -> 0() mark(cons(z0,z1)) -> cons(z0,z1) mark(eq(z0,z1)) -> a__eq(z0,z1) mark(false()) -> false() mark(inf(z0)) -> a__inf(mark(z0)) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(z0) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(true()) -> true() - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) ** Step 1.b:7: Decompose. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) - Weak DPs: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0 ,c6/0,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0 ,c_20/0,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0 ,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21 ,c22,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} Problem (S) - Strict DPs: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0 ,c6/0,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1 ,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0 ,c_20/0,c_21/1,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0 ,c_35/0,c_36/0,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21 ,c22,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} *** Step 1.b:7.a:1: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) - Weak DPs: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) The strictly oriented rules are moved into the weak component. **** Step 1.b:7.a:1.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) - Weak DPs: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_15) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_21) = {1}, uargs(c_22) = {1} Following symbols are considered usable: {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf#,a__length#,a__take#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__EQ) = [0] p(A__INF) = [0] p(A__LENGTH) = [0] p(A__TAKE) = [0] p(MARK) = [0] p(a__eq) = [0] p(a__inf) = [0] p(a__length) = [0] p(a__take) = [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [0] p(c14) = [0] p(c15) = [1] p(c16) = [1] p(c17) = [0] p(c18) = [2] p(c19) = [1] p(c2) = [1] p(c20) = [1] p(c21) = [8] p(c22) = [0] p(c3) = [0] p(c4) = [8] p(c5) = [0] p(c6) = [8] p(c7) = [4] p(c8) = [4] p(c9) = [1] p(cons) = [2] p(eq) = [1] x1 + [1] x2 + [3] p(false) = [4] p(inf) = [1] x1 + [3] p(length) = [1] x1 + [2] p(mark) = [4] x1 + [0] p(nil) = [2] p(s) = [1] x1 + [2] p(take) = [1] x1 + [1] x2 + [5] p(true) = [1] p(A__EQ#) = [4] x1 + [8] p(A__INF#) = [2] x1 + [1] p(A__LENGTH#) = [8] x1 + [1] p(A__TAKE#) = [1] x1 + [1] x2 + [1] p(MARK#) = [4] x1 + [0] p(a__eq#) = [1] x2 + [8] p(a__inf#) = [0] p(a__length#) = [1] x1 + [4] p(a__take#) = [1] x1 + [8] x2 + [1] p(mark#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [2] p(c_4) = [1] x1 + [0] p(c_5) = [4] p(c_6) = [1] p(c_7) = [0] p(c_8) = [2] p(c_9) = [1] p(c_10) = [1] p(c_11) = [0] p(c_12) = [1] p(c_13) = [4] p(c_14) = [1] p(c_15) = [1] x1 + [4] p(c_16) = [1] p(c_17) = [1] x1 + [12] p(c_18) = [1] x1 + [1] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] x1 + [4] p(c_22) = [1] x1 + [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [2] x1 + [0] p(c_28) = [1] p(c_29) = [4] p(c_30) = [1] p(c_31) = [0] p(c_32) = [2] p(c_33) = [0] p(c_34) = [1] p(c_35) = [4] p(c_36) = [1] p(c_37) = [1] p(c_38) = [2] x1 + [0] p(c_39) = [8] p(c_40) = [1] p(c_41) = [1] x1 + [0] p(c_42) = [8] p(c_43) = [2] p(c_44) = [0] p(c_45) = [4] Following rules are strictly oriented: A__EQ#(s(z0),s(z1)) = [4] z0 + [16] > [4] z0 + [8] = c_4(A__EQ#(z0,z1)) Following rules are (at-least) weakly oriented: MARK#(eq(z0,z1)) = [4] z0 + [4] z1 + [12] >= [4] z0 + [12] = c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) = [4] z0 + [12] >= [4] z0 + [12] = c_17(MARK#(z0)) MARK#(length(z0)) = [4] z0 + [8] >= [4] z0 + [1] = c_18(MARK#(z0)) MARK#(take(z0,z1)) = [4] z0 + [4] z1 + [20] >= [4] z0 + [4] = c_21(MARK#(z0)) MARK#(take(z0,z1)) = [4] z0 + [4] z1 + [20] >= [4] z1 + [2] = c_22(MARK#(z1)) **** Step 1.b:7.a:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:7.a:1.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 2:W:MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):1 3:W:MARK#(inf(z0)) -> c_17(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):6 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):5 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):4 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):3 -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 4:W:MARK#(length(z0)) -> c_18(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):6 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):5 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):4 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):3 -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 5:W:MARK#(take(z0,z1)) -> c_21(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):6 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):5 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):4 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):3 -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 6:W:MARK#(take(z0,z1)) -> c_22(MARK#(z1)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):6 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):5 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):4 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):3 -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: MARK#(inf(z0)) -> c_17(MARK#(z0)) 6: MARK#(take(z0,z1)) -> c_22(MARK#(z1)) 5: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) 4: MARK#(length(z0)) -> c_18(MARK#(z0)) 2: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) 1: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) **** Step 1.b:7.a:1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:7.b:1: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2,3,4,5}. Here rules are labelled as follows: 1: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) 2: MARK#(inf(z0)) -> c_17(MARK#(z0)) 3: MARK#(length(z0)) -> c_18(MARK#(z0)) 4: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) 5: MARK#(take(z0,z1)) -> c_22(MARK#(z1)) 6: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) *** Step 1.b:7.b:2: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:MARK#(inf(z0)) -> c_17(MARK#(z0)) -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):6 -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 2:S:MARK#(length(z0)) -> c_18(MARK#(z0)) -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):6 -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 3:S:MARK#(take(z0,z1)) -> c_21(MARK#(z0)) -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):6 -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 4:S:MARK#(take(z0,z1)) -> c_22(MARK#(z1)) -->_1 MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)):6 -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 5:W:A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):5 6:W:MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) -->_1 A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: MARK#(eq(z0,z1)) -> c_15(A__EQ#(z0,z1)) 5: A__EQ#(s(z0),s(z1)) -> c_4(A__EQ#(z0,z1)) *** Step 1.b:7.b:3: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: MARK#(length(z0)) -> c_18(MARK#(z0)) The strictly oriented rules are moved into the weak component. **** Step 1.b:7.b:3.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_21) = {1}, uargs(c_22) = {1} Following symbols are considered usable: {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf#,a__length#,a__take#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__EQ) = [2] p(A__INF) = [0] p(A__LENGTH) = [1] x1 + [1] p(A__TAKE) = [1] x1 + [1] x2 + [1] p(MARK) = [1] p(a__eq) = [2] x2 + [0] p(a__inf) = [1] x1 + [1] p(a__length) = [1] p(a__take) = [1] p(c) = [2] p(c1) = [4] p(c10) = [0] p(c11) = [4] p(c12) = [1] p(c13) = [1] x2 + [0] p(c14) = [1] p(c15) = [2] p(c16) = [0] p(c17) = [8] p(c18) = [0] p(c19) = [8] p(c2) = [0] p(c20) = [4] p(c21) = [0] p(c22) = [0] p(c3) = [0] p(c4) = [1] p(c5) = [2] p(c6) = [1] p(c7) = [1] p(c8) = [1] p(c9) = [1] p(cons) = [1] x2 + [0] p(eq) = [1] x2 + [0] p(false) = [2] p(inf) = [1] x1 + [0] p(length) = [1] x1 + [2] p(mark) = [0] p(nil) = [1] p(s) = [1] p(take) = [1] x1 + [1] x2 + [0] p(true) = [1] p(A__EQ#) = [2] x2 + [1] p(A__INF#) = [1] x1 + [1] p(A__LENGTH#) = [1] x1 + [1] p(A__TAKE#) = [1] x2 + [1] p(MARK#) = [8] x1 + [0] p(a__eq#) = [1] x2 + [1] p(a__inf#) = [1] p(a__length#) = [1] p(a__take#) = [1] x2 + [0] p(mark#) = [2] x1 + [8] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] p(c_4) = [4] x1 + [1] p(c_5) = [1] p(c_6) = [0] p(c_7) = [1] p(c_8) = [1] p(c_9) = [8] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [8] p(c_19) = [1] p(c_20) = [1] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [0] p(c_24) = [1] p(c_25) = [1] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] p(c_29) = [1] p(c_30) = [0] p(c_31) = [0] p(c_32) = [1] p(c_33) = [1] p(c_34) = [1] p(c_35) = [0] p(c_36) = [1] p(c_37) = [1] p(c_38) = [8] p(c_39) = [1] p(c_40) = [1] x1 + [2] p(c_41) = [1] x1 + [1] p(c_42) = [1] p(c_43) = [0] p(c_44) = [1] x1 + [0] p(c_45) = [1] Following rules are strictly oriented: MARK#(length(z0)) = [8] z0 + [16] > [8] z0 + [8] = c_18(MARK#(z0)) Following rules are (at-least) weakly oriented: MARK#(inf(z0)) = [8] z0 + [0] >= [8] z0 + [0] = c_17(MARK#(z0)) MARK#(take(z0,z1)) = [8] z0 + [8] z1 + [0] >= [8] z0 + [0] = c_21(MARK#(z0)) MARK#(take(z0,z1)) = [8] z0 + [8] z1 + [0] >= [8] z1 + [0] = c_22(MARK#(z1)) **** Step 1.b:7.b:3.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:7.b:3.b:1: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: MARK#(inf(z0)) -> c_17(MARK#(z0)) The strictly oriented rules are moved into the weak component. ***** Step 1.b:7.b:3.b:1.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_21) = {1}, uargs(c_22) = {1} Following symbols are considered usable: {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf#,a__length#,a__take#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__EQ) = [4] x1 + [0] p(A__INF) = [1] x1 + [0] p(A__LENGTH) = [8] p(A__TAKE) = [2] x1 + [1] p(MARK) = [2] x1 + [1] p(a__eq) = [1] x1 + [1] x2 + [1] p(a__inf) = [1] p(a__length) = [1] p(a__take) = [1] x1 + [2] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [1] x2 + [0] p(c14) = [1] x1 + [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [0] p(eq) = [1] x2 + [0] p(false) = [0] p(inf) = [1] x1 + [7] p(length) = [1] x1 + [0] p(mark) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(true) = [0] p(A__EQ#) = [0] p(A__INF#) = [0] p(A__LENGTH#) = [0] p(A__TAKE#) = [0] p(MARK#) = [2] x1 + [2] p(a__eq#) = [0] p(a__inf#) = [0] p(a__length#) = [0] p(a__take#) = [0] p(mark#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [1] x1 + [9] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [4] p(c_24) = [1] p(c_25) = [1] p(c_26) = [0] p(c_27) = [8] x1 + [0] p(c_28) = [0] p(c_29) = [4] p(c_30) = [1] p(c_31) = [1] p(c_32) = [2] p(c_33) = [0] p(c_34) = [1] p(c_35) = [1] p(c_36) = [2] p(c_37) = [1] p(c_38) = [8] p(c_39) = [0] p(c_40) = [1] x1 + [0] p(c_41) = [1] p(c_42) = [1] p(c_43) = [1] p(c_44) = [1] x1 + [1] p(c_45) = [0] Following rules are strictly oriented: MARK#(inf(z0)) = [2] z0 + [16] > [2] z0 + [11] = c_17(MARK#(z0)) Following rules are (at-least) weakly oriented: MARK#(length(z0)) = [2] z0 + [2] >= [2] z0 + [2] = c_18(MARK#(z0)) MARK#(take(z0,z1)) = [2] z0 + [2] z1 + [2] >= [2] z0 + [2] = c_21(MARK#(z0)) MARK#(take(z0,z1)) = [2] z0 + [2] z1 + [2] >= [2] z1 + [2] = c_22(MARK#(z1)) ***** Step 1.b:7.b:3.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ***** Step 1.b:7.b:3.b:1.b:1: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) 2: MARK#(take(z0,z1)) -> c_22(MARK#(z1)) The strictly oriented rules are moved into the weak component. ****** Step 1.b:7.b:3.b:1.b:1.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Weak DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_21) = {1}, uargs(c_22) = {1} Following symbols are considered usable: {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf#,a__length#,a__take#,mark#} TcT has computed the following interpretation: p(0) = [0] p(A__EQ) = [0] p(A__INF) = [0] p(A__LENGTH) = [0] p(A__TAKE) = [0] p(MARK) = [0] p(a__eq) = [0] p(a__inf) = [0] p(a__length) = [0] p(a__take) = [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c16) = [1] x1 + [1] x2 + [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(eq) = [1] x1 + [1] x2 + [0] p(false) = [0] p(inf) = [1] x1 + [0] p(length) = [1] x1 + [0] p(mark) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [1] p(true) = [0] p(A__EQ#) = [0] p(A__INF#) = [0] p(A__LENGTH#) = [0] p(A__TAKE#) = [0] p(MARK#) = [1] x1 + [0] p(a__eq#) = [0] p(a__inf#) = [1] x1 + [4] p(a__length#) = [1] x1 + [1] p(a__take#) = [8] p(mark#) = [1] x1 + [4] p(c_1) = [8] p(c_2) = [1] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [0] p(c_7) = [1] p(c_8) = [1] p(c_9) = [0] p(c_10) = [2] p(c_11) = [2] p(c_12) = [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [2] p(c_20) = [1] p(c_21) = [1] x1 + [0] p(c_22) = [1] x1 + [0] p(c_23) = [1] p(c_24) = [1] p(c_25) = [2] p(c_26) = [1] p(c_27) = [2] x1 + [0] p(c_28) = [0] p(c_29) = [1] p(c_30) = [2] p(c_31) = [0] p(c_32) = [1] p(c_33) = [2] p(c_34) = [2] p(c_35) = [1] p(c_36) = [8] p(c_37) = [4] p(c_38) = [8] p(c_39) = [0] p(c_40) = [0] p(c_41) = [1] x1 + [0] p(c_42) = [1] p(c_43) = [4] p(c_44) = [2] x1 + [1] p(c_45) = [1] Following rules are strictly oriented: MARK#(take(z0,z1)) = [1] z0 + [1] z1 + [1] > [1] z0 + [0] = c_21(MARK#(z0)) MARK#(take(z0,z1)) = [1] z0 + [1] z1 + [1] > [1] z1 + [0] = c_22(MARK#(z1)) Following rules are (at-least) weakly oriented: MARK#(inf(z0)) = [1] z0 + [0] >= [1] z0 + [0] = c_17(MARK#(z0)) MARK#(length(z0)) = [1] z0 + [0] >= [1] z0 + [0] = c_18(MARK#(z0)) ****** Step 1.b:7.b:3.b:1.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ****** Step 1.b:7.b:3.b:1.b:1.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: MARK#(inf(z0)) -> c_17(MARK#(z0)) MARK#(length(z0)) -> c_18(MARK#(z0)) MARK#(take(z0,z1)) -> c_21(MARK#(z0)) MARK#(take(z0,z1)) -> c_22(MARK#(z1)) - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:MARK#(inf(z0)) -> c_17(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 2:W:MARK#(length(z0)) -> c_18(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 3:W:MARK#(take(z0,z1)) -> c_21(MARK#(z0)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 4:W:MARK#(take(z0,z1)) -> c_22(MARK#(z1)) -->_1 MARK#(take(z0,z1)) -> c_22(MARK#(z1)):4 -->_1 MARK#(take(z0,z1)) -> c_21(MARK#(z0)):3 -->_1 MARK#(length(z0)) -> c_18(MARK#(z0)):2 -->_1 MARK#(inf(z0)) -> c_17(MARK#(z0)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: MARK#(inf(z0)) -> c_17(MARK#(z0)) 4: MARK#(take(z0,z1)) -> c_22(MARK#(z1)) 3: MARK#(take(z0,z1)) -> c_21(MARK#(z0)) 2: MARK#(length(z0)) -> c_18(MARK#(z0)) ****** Step 1.b:7.b:3.b:1.b:1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {A__EQ/2,A__INF/1,A__LENGTH/1,A__TAKE/2,MARK/1,a__eq/2,a__inf/1,a__length/1,a__take/2,mark/1,A__EQ#/2 ,A__INF#/1,A__LENGTH#/1,A__TAKE#/2,MARK#/1,a__eq#/2,a__inf#/1,a__length#/1,a__take#/2,mark#/1} / {0/0,c/0 ,c1/1,c10/0,c11/0,c12/1,c13/2,c14/2,c15/2,c16/2,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c3/0,c4/0,c5/0,c6/0 ,c7/0,c8/0,c9/0,cons/2,eq/2,false/0,inf/1,length/1,nil/0,s/1,take/2,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/0 ,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/0,c_20/0,c_21/1 ,c_22/1,c_23/0,c_24/0,c_25/0,c_26/0,c_27/1,c_28/0,c_29/0,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0 ,c_37/0,c_38/1,c_39/0,c_40/1,c_41/1,c_42/0,c_43/0,c_44/1,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__EQ#,A__INF#,A__LENGTH#,A__TAKE#,MARK#,a__eq#,a__inf# ,a__length#,a__take#,mark#} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c3,c4,c5,c6,c7,c8,c9,cons,eq,false,inf,length,nil,s,take,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))