WORST_CASE(?,O(n^10)) * Step 1: DependencyPairs WORST_CASE(?,O(n^10)) + Considered Problem: - Strict TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) f_10(x) -> g_10(x,x) f_2(x) -> g_2(x,x) f_3(x) -> g_3(x,x) f_4(x) -> g_4(x,x) f_5(x) -> g_5(x,x) f_6(x) -> g_6(x,x) f_7(x) -> g_7(x,x) f_8(x) -> g_8(x,x) f_9(x) -> g_9(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2} / {a/0,b/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f_0,f_1,f_10,f_2,f_3,f_4,f_5,f_6,f_7,f_8,f_9,g_1,g_10,g_2 ,g_3,g_4,g_5,g_6,g_7,g_8,g_9} and constructors {a,b,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f_0#(x) -> c_1() f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_0#(x) -> c_1() f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) f_10(x) -> g_10(x,x) f_2(x) -> g_2(x,x) f_3(x) -> g_3(x,x) f_4(x) -> g_4(x,x) f_5(x) -> g_5(x,x) f_6(x) -> g_6(x,x) f_7(x) -> g_7(x,x) f_8(x) -> g_8(x,x) f_9(x) -> g_9(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {12}. Here rules are labelled as follows: 1: f_0#(x) -> c_1() 2: f_1#(x) -> c_2(g_1#(x,x)) 3: f_10#(x) -> c_3(g_10#(x,x)) 4: f_2#(x) -> c_4(g_2#(x,x)) 5: f_3#(x) -> c_5(g_3#(x,x)) 6: f_4#(x) -> c_6(g_4#(x,x)) 7: f_5#(x) -> c_7(g_5#(x,x)) 8: f_6#(x) -> c_8(g_6#(x,x)) 9: f_7#(x) -> c_9(g_7#(x,x)) 10: f_8#(x) -> c_10(g_8#(x,x)) 11: f_9#(x) -> c_11(g_9#(x,x)) 12: g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) 13: g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) 14: g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) 15: g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) 16: g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) 17: g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) 18: g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) 19: g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) 20: g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) 21: g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak DPs: f_0#(x) -> c_1() - Weak TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) f_10(x) -> g_10(x,x) f_2(x) -> g_2(x,x) f_3(x) -> g_3(x,x) f_4(x) -> g_4(x,x) f_5(x) -> g_5(x,x) f_6(x) -> g_6(x,x) f_7(x) -> g_7(x,x) f_8(x) -> g_8(x,x) f_9(x) -> g_9(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f_1#(x) -> c_2(g_1#(x,x)) -->_1 g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)):11 2:S:f_10#(x) -> c_3(g_10#(x,x)) -->_1 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 3:S:f_2#(x) -> c_4(g_2#(x,x)) -->_1 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 4:S:f_3#(x) -> c_5(g_3#(x,x)) -->_1 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 5:S:f_4#(x) -> c_6(g_4#(x,x)) -->_1 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 6:S:f_5#(x) -> c_7(g_5#(x,x)) -->_1 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 7:S:f_6#(x) -> c_8(g_6#(x,x)) -->_1 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 8:S:f_7#(x) -> c_9(g_7#(x,x)) -->_1 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 9:S:f_8#(x) -> c_10(g_8#(x,x)) -->_1 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 10:S:f_9#(x) -> c_11(g_9#(x,x)) -->_1 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 11:S:g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) -->_1 f_0#(x) -> c_1():21 -->_2 g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)):11 12:S:g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) -->_2 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 -->_1 f_9#(x) -> c_11(g_9#(x,x)):10 13:S:g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) -->_2 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 -->_1 f_1#(x) -> c_2(g_1#(x,x)):1 14:S:g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) -->_2 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 -->_1 f_2#(x) -> c_4(g_2#(x,x)):3 15:S:g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) -->_2 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 -->_1 f_3#(x) -> c_5(g_3#(x,x)):4 16:S:g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) -->_2 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 -->_1 f_4#(x) -> c_6(g_4#(x,x)):5 17:S:g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) -->_2 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 -->_1 f_5#(x) -> c_7(g_5#(x,x)):6 18:S:g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) -->_2 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 -->_1 f_6#(x) -> c_8(g_6#(x,x)):7 19:S:g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) -->_2 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 -->_1 f_7#(x) -> c_9(g_7#(x,x)):8 20:S:g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) -->_2 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 -->_1 f_8#(x) -> c_10(g_8#(x,x)):9 21:W:f_0#(x) -> c_1() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 21: f_0#(x) -> c_1() * Step 4: SimplifyRHS WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) f_10(x) -> g_10(x,x) f_2(x) -> g_2(x,x) f_3(x) -> g_3(x,x) f_4(x) -> g_4(x,x) f_5(x) -> g_5(x,x) f_6(x) -> g_6(x,x) f_7(x) -> g_7(x,x) f_8(x) -> g_8(x,x) f_9(x) -> g_9(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/2,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_1#(x) -> c_2(g_1#(x,x)) -->_1 g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)):11 2:S:f_10#(x) -> c_3(g_10#(x,x)) -->_1 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 3:S:f_2#(x) -> c_4(g_2#(x,x)) -->_1 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 4:S:f_3#(x) -> c_5(g_3#(x,x)) -->_1 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 5:S:f_4#(x) -> c_6(g_4#(x,x)) -->_1 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 6:S:f_5#(x) -> c_7(g_5#(x,x)) -->_1 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 7:S:f_6#(x) -> c_8(g_6#(x,x)) -->_1 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 8:S:f_7#(x) -> c_9(g_7#(x,x)) -->_1 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 9:S:f_8#(x) -> c_10(g_8#(x,x)) -->_1 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 10:S:f_9#(x) -> c_11(g_9#(x,x)) -->_1 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 11:S:g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)) -->_2 g_1#(s(x),y) -> c_12(f_0#(y),g_1#(x,y)):11 12:S:g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) -->_2 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 -->_1 f_9#(x) -> c_11(g_9#(x,x)):10 13:S:g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) -->_2 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 -->_1 f_1#(x) -> c_2(g_1#(x,x)):1 14:S:g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) -->_2 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 -->_1 f_2#(x) -> c_4(g_2#(x,x)):3 15:S:g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) -->_2 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 -->_1 f_3#(x) -> c_5(g_3#(x,x)):4 16:S:g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) -->_2 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 -->_1 f_4#(x) -> c_6(g_4#(x,x)):5 17:S:g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) -->_2 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 -->_1 f_5#(x) -> c_7(g_5#(x,x)):6 18:S:g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) -->_2 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 -->_1 f_6#(x) -> c_8(g_6#(x,x)):7 19:S:g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) -->_2 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 -->_1 f_7#(x) -> c_9(g_7#(x,x)):8 20:S:g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) -->_2 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 -->_1 f_8#(x) -> c_10(g_8#(x,x)):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_1#(s(x),y) -> c_12(g_1#(x,y)) * Step 5: UsableRules WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) f_10(x) -> g_10(x,x) f_2(x) -> g_2(x,x) f_3(x) -> g_3(x,x) f_4(x) -> g_4(x,x) f_5(x) -> g_5(x,x) f_6(x) -> g_6(x,x) f_7(x) -> g_7(x,x) f_8(x) -> g_8(x,x) f_9(x) -> g_9(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) * Step 6: RemoveHeads WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_10#(x) -> c_3(g_10#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:f_1#(x) -> c_2(g_1#(x,x)) -->_1 g_1#(s(x),y) -> c_12(g_1#(x,y)):11 2:S:f_10#(x) -> c_3(g_10#(x,x)) -->_1 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 3:S:f_2#(x) -> c_4(g_2#(x,x)) -->_1 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 4:S:f_3#(x) -> c_5(g_3#(x,x)) -->_1 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 5:S:f_4#(x) -> c_6(g_4#(x,x)) -->_1 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 6:S:f_5#(x) -> c_7(g_5#(x,x)) -->_1 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 7:S:f_6#(x) -> c_8(g_6#(x,x)) -->_1 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 8:S:f_7#(x) -> c_9(g_7#(x,x)) -->_1 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 9:S:f_8#(x) -> c_10(g_8#(x,x)) -->_1 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 10:S:f_9#(x) -> c_11(g_9#(x,x)) -->_1 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 11:S:g_1#(s(x),y) -> c_12(g_1#(x,y)) -->_1 g_1#(s(x),y) -> c_12(g_1#(x,y)):11 12:S:g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) -->_2 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):12 -->_1 f_9#(x) -> c_11(g_9#(x,x)):10 13:S:g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) -->_2 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):13 -->_1 f_1#(x) -> c_2(g_1#(x,x)):1 14:S:g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) -->_2 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):14 -->_1 f_2#(x) -> c_4(g_2#(x,x)):3 15:S:g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) -->_2 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):15 -->_1 f_3#(x) -> c_5(g_3#(x,x)):4 16:S:g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) -->_2 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):16 -->_1 f_4#(x) -> c_6(g_4#(x,x)):5 17:S:g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) -->_2 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):17 -->_1 f_5#(x) -> c_7(g_5#(x,x)):6 18:S:g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) -->_2 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):18 -->_1 f_6#(x) -> c_8(g_6#(x,x)):7 19:S:g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) -->_2 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):19 -->_1 f_7#(x) -> c_9(g_7#(x,x)):8 20:S:g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) -->_2 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):20 -->_1 f_8#(x) -> c_10(g_8#(x,x)):9 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(2,f_10#(x) -> c_3(g_10#(x,x)))] * Step 7: DecomposeDG WORST_CASE(?,O(n^10)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) Further, following extension rules are added to the lower component. g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)) -->_2 g_10#(s(x),y) -> c_13(f_9#(y),g_10#(x,y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_10#(s(x),y) -> c_13(g_10#(x,y)) ** Step 7.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_10#(s(x),y) -> c_13(g_10#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_13) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [1] p(f_10) = [0] p(f_2) = [0] p(f_3) = [2] p(f_4) = [0] p(f_5) = [1] x1 + [0] p(f_6) = [8] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [1] x2 + [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [4] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [2] x1 + [0] p(f_3#) = [1] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [0] p(f_9#) = [0] p(g_1#) = [0] p(g_10#) = [4] x1 + [0] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [0] p(g_8#) = [0] p(g_9#) = [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) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [2] x1 + [4] x2 + [0] Following rules are strictly oriented: g_10#(s(x),y) = [4] x + [16] > [4] x + [0] = c_13(g_10#(x,y)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: g_10#(s(x),y) -> c_13(g_10#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: DecomposeDG WORST_CASE(?,O(n^9)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> c_11(g_9#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak DPs: g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_9#(x) -> c_11(g_9#(x,x)) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) Further, following extension rules are added to the lower component. f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) *** Step 7.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_9#(x) -> c_11(g_9#(x,x)) g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) - Weak DPs: g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_9#(x) -> c_11(g_9#(x,x)) -->_1 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):2 2:S:g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)) -->_2 g_9#(s(x),y) -> c_21(f_8#(y),g_9#(x,y)):2 3:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> c_11(g_9#(x,x)):1 4:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):4 -->_1 g_10#(s(x),y) -> f_9#(y):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_9#(s(x),y) -> c_21(g_9#(x,y)) *** Step 7.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_9#(x) -> c_11(g_9#(x,x)) g_9#(s(x),y) -> c_21(g_9#(x,y)) - Weak DPs: g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1}, uargs(c_21) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [1] x2 + [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [5] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [0] p(f_9#) = [1] x1 + [0] p(g_1#) = [0] p(g_10#) = [1] x2 + [0] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [0] p(g_8#) = [0] p(g_9#) = [1] x1 + [10] 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) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] x1 + [0] Following rules are strictly oriented: g_9#(s(x),y) = [1] x + [15] > [1] x + [10] = c_21(g_9#(x,y)) Following rules are (at-least) weakly oriented: f_9#(x) = [1] x + [0] >= [1] x + [10] = c_11(g_9#(x,x)) g_10#(s(x),y) = [1] y + [0] >= [1] y + [0] = f_9#(y) g_10#(s(x),y) = [1] y + [0] >= [1] y + [0] = g_10#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_9#(x) -> c_11(g_9#(x,x)) - Weak DPs: g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> c_21(g_9#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_11) = {1}, uargs(c_21) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [0] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [0] p(f_9#) = [1] p(g_1#) = [0] p(g_10#) = [1] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [0] p(g_8#) = [0] p(g_9#) = [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) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [1] x1 + [0] Following rules are strictly oriented: f_9#(x) = [1] > [0] = c_11(g_9#(x,x)) Following rules are (at-least) weakly oriented: g_10#(s(x),y) = [1] >= [1] = f_9#(y) g_10#(s(x),y) = [1] >= [1] = g_10#(x,y) g_9#(s(x),y) = [0] >= [0] = c_21(g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 7.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_9#(x) -> c_11(g_9#(x,x)) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> c_21(g_9#(x,y)) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/1} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 7.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^8)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) - Weak DPs: f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) Further, following extension rules are added to the lower component. f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) **** Step 7.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_8#(x) -> c_10(g_8#(x,x)) g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) - Weak DPs: f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_8#(x) -> c_10(g_8#(x,x)) -->_1 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):2 2:S:g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)) -->_2 g_8#(s(x),y) -> c_20(f_7#(y),g_8#(x,y)):2 3:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):7 -->_1 g_9#(s(x),y) -> f_8#(y):6 4:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):3 5:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):5 -->_1 g_10#(s(x),y) -> f_9#(y):4 6:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> c_10(g_8#(x,x)):1 7:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):7 -->_1 g_9#(s(x),y) -> f_8#(y):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_8#(s(x),y) -> c_20(g_8#(x,y)) **** Step 7.b:1.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_8#(x) -> c_10(g_8#(x,x)) g_8#(s(x),y) -> c_20(g_8#(x,y)) - Weak DPs: f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [1] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [1] x1 + [0] p(f_8) = [4] p(f_9) = [0] p(g_1) = [1] x2 + [0] p(g_10) = [0] p(g_2) = [8] p(g_3) = [1] x1 + [0] p(g_4) = [2] x2 + [0] p(g_5) = [2] x1 + [1] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [2] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [2] p(f_9#) = [2] x1 + [9] p(g_1#) = [0] p(g_10#) = [3] x2 + [13] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [0] p(g_8#) = [0] p(g_9#) = [1] x1 + [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) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x2 + [2] p(c_19) = [1] x1 + [1] p(c_20) = [1] x1 + [3] p(c_21) = [1] x1 + [8] x2 + [1] Following rules are strictly oriented: f_8#(x) = [2] > [0] = c_10(g_8#(x,x)) Following rules are (at-least) weakly oriented: f_9#(x) = [2] x + [9] >= [1] x + [0] = g_9#(x,x) g_10#(s(x),y) = [3] y + [13] >= [2] y + [9] = f_9#(y) g_10#(s(x),y) = [3] y + [13] >= [3] y + [13] = g_10#(x,y) g_8#(s(x),y) = [0] >= [3] = c_20(g_8#(x,y)) g_9#(s(x),y) = [1] x + [2] >= [2] = f_8#(y) g_9#(s(x),y) = [1] x + [2] >= [1] x + [0] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 7.b:1.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_8#(s(x),y) -> c_20(g_8#(x,y)) - Weak DPs: f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_10) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [1] x1 + [0] p(f_1) = [1] p(f_10) = [0] p(f_2) = [0] p(f_3) = [1] x1 + [0] p(f_4) = [8] x1 + [0] p(f_5) = [0] p(f_6) = [1] x1 + [0] p(f_7) = [1] p(f_8) = [4] x1 + [2] p(f_9) = [8] x1 + [1] p(g_1) = [4] x1 + [1] x2 + [1] p(g_10) = [4] p(g_2) = [2] x1 + [0] p(g_3) = [2] x1 + [1] x2 + [0] p(g_4) = [1] x2 + [1] p(g_5) = [4] x1 + [1] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [2] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [6] x1 + [15] p(f_9#) = [14] x1 + [9] p(g_1#) = [0] p(g_10#) = [2] x1 + [14] x2 + [5] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [0] p(g_8#) = [4] x1 + [2] x2 + [12] p(g_9#) = [8] x1 + [6] x2 + [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) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [1] p(c_11) = [0] p(c_12) = [1] x1 + [1] p(c_13) = [1] x1 + [0] p(c_14) = [2] x1 + [1] x2 + [0] p(c_15) = [1] x1 + [2] p(c_16) = [1] x2 + [2] p(c_17) = [1] x1 + [0] p(c_18) = [4] x1 + [1] p(c_19) = [1] x1 + [1] x2 + [2] p(c_20) = [1] x1 + [0] p(c_21) = [8] x1 + [1] x2 + [1] Following rules are strictly oriented: g_8#(s(x),y) = [4] x + [2] y + [20] > [4] x + [2] y + [12] = c_20(g_8#(x,y)) Following rules are (at-least) weakly oriented: f_8#(x) = [6] x + [15] >= [6] x + [13] = c_10(g_8#(x,x)) f_9#(x) = [14] x + [9] >= [14] x + [0] = g_9#(x,x) g_10#(s(x),y) = [2] x + [14] y + [9] >= [14] y + [9] = f_9#(y) g_10#(s(x),y) = [2] x + [14] y + [9] >= [2] x + [14] y + [5] = g_10#(x,y) g_9#(s(x),y) = [8] x + [6] y + [16] >= [6] y + [15] = f_8#(y) g_9#(s(x),y) = [8] x + [6] y + [16] >= [8] x + [6] y + [0] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. **** Step 7.b:1.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_8#(x) -> c_10(g_8#(x,x)) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> c_20(g_8#(x,y)) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 7.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^7)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) - Weak DPs: f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) Further, following extension rules are added to the lower component. f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ***** Step 7.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_7#(x) -> c_9(g_7#(x,x)) g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) - Weak DPs: f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_7#(x) -> c_9(g_7#(x,x)) -->_1 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):2 2:S:g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)) -->_2 g_7#(s(x),y) -> c_19(f_6#(y),g_7#(x,y)):2 3:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):8 -->_1 g_8#(s(x),y) -> f_7#(y):7 4:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):10 -->_1 g_9#(s(x),y) -> f_8#(y):9 5:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):4 6:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):6 -->_1 g_10#(s(x),y) -> f_9#(y):5 7:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> c_9(g_7#(x,x)):1 8:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):8 -->_1 g_8#(s(x),y) -> f_7#(y):7 9:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):3 10:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):10 -->_1 g_9#(s(x),y) -> f_8#(y):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_7#(s(x),y) -> c_19(g_7#(x,y)) ***** Step 7.b:1.b:1.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_7#(x) -> c_9(g_7#(x,x)) g_7#(s(x),y) -> c_19(g_7#(x,y)) - Weak DPs: f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/1 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_19) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [1] p(f_5) = [0] p(f_6) = [1] x1 + [8] p(f_7) = [4] p(f_8) = [0] p(f_9) = [8] p(g_1) = [1] x1 + [0] p(g_10) = [0] p(g_2) = [1] x1 + [2] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [1] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [1] x1 + [7] p(f_8#) = [1] x1 + [7] p(f_9#) = [1] x1 + [7] p(g_1#) = [0] p(g_10#) = [1] x2 + [7] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [1] x1 + [4] p(g_8#) = [1] x2 + [7] p(g_9#) = [1] x2 + [7] 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) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x2 + [8] p(c_17) = [1] x1 + [0] p(c_18) = [4] x2 + [0] p(c_19) = [1] x1 + [0] p(c_20) = [1] x1 + [0] p(c_21) = [2] x1 + [2] x2 + [1] Following rules are strictly oriented: f_7#(x) = [1] x + [7] > [1] x + [4] = c_9(g_7#(x,x)) g_7#(s(x),y) = [1] x + [5] > [1] x + [4] = c_19(g_7#(x,y)) Following rules are (at-least) weakly oriented: f_8#(x) = [1] x + [7] >= [1] x + [7] = g_8#(x,x) f_9#(x) = [1] x + [7] >= [1] x + [7] = g_9#(x,x) g_10#(s(x),y) = [1] y + [7] >= [1] y + [7] = f_9#(y) g_10#(s(x),y) = [1] y + [7] >= [1] y + [7] = g_10#(x,y) g_8#(s(x),y) = [1] y + [7] >= [1] y + [7] = f_7#(y) g_8#(s(x),y) = [1] y + [7] >= [1] y + [7] = g_8#(x,y) g_9#(s(x),y) = [1] y + [7] >= [1] y + [7] = f_8#(y) g_9#(s(x),y) = [1] y + [7] >= [1] y + [7] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ***** Step 7.b:1.b:1.b:1.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> c_19(g_7#(x,y)) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/1 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ***** Step 7.b:1.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^6)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> c_8(g_6#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) - Weak DPs: f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) Further, following extension rules are added to the lower component. f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ****** Step 7.b:1.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_6#(x) -> c_8(g_6#(x,x)) g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) - Weak DPs: f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_6#(x) -> c_8(g_6#(x,x)) -->_1 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):2 2:S:g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)) -->_2 g_6#(s(x),y) -> c_18(f_5#(y),g_6#(x,y)):2 3:W:f_7#(x) -> g_7#(x,x) -->_1 g_7#(s(x),y) -> g_7#(x,y):9 -->_1 g_7#(s(x),y) -> f_6#(y):8 4:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):11 -->_1 g_8#(s(x),y) -> f_7#(y):10 5:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):13 -->_1 g_9#(s(x),y) -> f_8#(y):12 6:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):5 7:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):7 -->_1 g_10#(s(x),y) -> f_9#(y):6 8:W:g_7#(s(x),y) -> f_6#(y) -->_1 f_6#(x) -> c_8(g_6#(x,x)):1 9:W:g_7#(s(x),y) -> g_7#(x,y) -->_1 g_7#(s(x),y) -> g_7#(x,y):9 -->_1 g_7#(s(x),y) -> f_6#(y):8 10:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> g_7#(x,x):3 11:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):11 -->_1 g_8#(s(x),y) -> f_7#(y):10 12:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):4 13:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):13 -->_1 g_9#(s(x),y) -> f_8#(y):12 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_6#(s(x),y) -> c_18(g_6#(x,y)) ****** Step 7.b:1.b:1.b:1.b:1.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_6#(x) -> c_8(g_6#(x,x)) g_6#(s(x),y) -> c_18(g_6#(x,y)) - Weak DPs: f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/1,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_8) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9#,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8# ,g_9#} TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [0] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [4] p(f_7#) = [5] p(f_8#) = [5] p(f_9#) = [5] p(g_1#) = [0] p(g_10#) = [5] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [4] p(g_8#) = [5] p(g_9#) = [5] 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) = [0] p(c_8) = [8] x1 + [3] p(c_9) = [2] x1 + [0] p(c_10) = [2] x1 + [0] p(c_11) = [8] x1 + [0] p(c_12) = [0] p(c_13) = [1] x2 + [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [8] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: f_6#(x) = [4] > [3] = c_8(g_6#(x,x)) Following rules are (at-least) weakly oriented: f_7#(x) = [5] >= [4] = g_7#(x,x) f_8#(x) = [5] >= [5] = g_8#(x,x) f_9#(x) = [5] >= [5] = g_9#(x,x) g_10#(s(x),y) = [5] >= [5] = f_9#(y) g_10#(s(x),y) = [5] >= [5] = g_10#(x,y) g_6#(s(x),y) = [0] >= [0] = c_18(g_6#(x,y)) g_7#(s(x),y) = [4] >= [4] = f_6#(y) g_7#(s(x),y) = [4] >= [4] = g_7#(x,y) g_8#(s(x),y) = [5] >= [5] = f_7#(y) g_8#(s(x),y) = [5] >= [5] = g_8#(x,y) g_9#(s(x),y) = [5] >= [5] = f_8#(y) g_9#(s(x),y) = [5] >= [5] = g_9#(x,y) ****** Step 7.b:1.b:1.b:1.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_6#(s(x),y) -> c_18(g_6#(x,y)) - Weak DPs: f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/1,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_8) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [1] x1 + [4] p(f_2) = [4] x1 + [0] p(f_3) = [1] x1 + [0] p(f_4) = [1] x1 + [0] p(f_5) = [1] x1 + [1] p(f_6) = [4] x1 + [1] p(f_7) = [4] x1 + [0] p(f_8) = [1] p(f_9) = [1] p(g_1) = [1] x1 + [0] p(g_10) = [4] x1 + [1] x2 + [1] p(g_2) = [1] p(g_3) = [1] x2 + [1] p(g_4) = [1] p(g_5) = [2] x1 + [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [3] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [0] p(f_6#) = [3] x1 + [0] p(f_7#) = [3] x1 + [0] p(f_8#) = [4] x1 + [0] p(f_9#) = [5] x1 + [1] p(g_1#) = [0] p(g_10#) = [7] x2 + [4] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [0] p(g_6#) = [3] x1 + [0] p(g_7#) = [3] x2 + [0] p(g_8#) = [4] x2 + [0] p(g_9#) = [5] x2 + [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) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [2] x2 + [0] p(c_18) = [1] x1 + [5] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: g_6#(s(x),y) = [3] x + [9] > [3] x + [5] = c_18(g_6#(x,y)) Following rules are (at-least) weakly oriented: f_6#(x) = [3] x + [0] >= [3] x + [0] = c_8(g_6#(x,x)) f_7#(x) = [3] x + [0] >= [3] x + [0] = g_7#(x,x) f_8#(x) = [4] x + [0] >= [4] x + [0] = g_8#(x,x) f_9#(x) = [5] x + [1] >= [5] x + [0] = g_9#(x,x) g_10#(s(x),y) = [7] y + [4] >= [5] y + [1] = f_9#(y) g_10#(s(x),y) = [7] y + [4] >= [7] y + [4] = g_10#(x,y) g_7#(s(x),y) = [3] y + [0] >= [3] y + [0] = f_6#(y) g_7#(s(x),y) = [3] y + [0] >= [3] y + [0] = g_7#(x,y) g_8#(s(x),y) = [4] y + [0] >= [3] y + [0] = f_7#(y) g_8#(s(x),y) = [4] y + [0] >= [4] y + [0] = g_8#(x,y) g_9#(s(x),y) = [5] y + [0] >= [4] y + [0] = f_8#(y) g_9#(s(x),y) = [5] y + [0] >= [5] y + [0] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ****** Step 7.b:1.b:1.b:1.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_6#(x) -> c_8(g_6#(x,x)) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> c_18(g_6#(x,y)) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/1,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ****** Step 7.b:1.b:1.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) - Weak DPs: f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) Further, following extension rules are added to the lower component. f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ******* Step 7.b:1.b:1.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_5#(x) -> c_7(g_5#(x,x)) g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) - Weak DPs: f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_5#(x) -> c_7(g_5#(x,x)) -->_1 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):2 2:S:g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)) -->_2 g_5#(s(x),y) -> c_17(f_4#(y),g_5#(x,y)):2 3:W:f_6#(x) -> g_6#(x,x) -->_1 g_6#(s(x),y) -> g_6#(x,y):10 -->_1 g_6#(s(x),y) -> f_5#(y):9 4:W:f_7#(x) -> g_7#(x,x) -->_1 g_7#(s(x),y) -> g_7#(x,y):12 -->_1 g_7#(s(x),y) -> f_6#(y):11 5:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):14 -->_1 g_8#(s(x),y) -> f_7#(y):13 6:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):16 -->_1 g_9#(s(x),y) -> f_8#(y):15 7:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):6 8:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):8 -->_1 g_10#(s(x),y) -> f_9#(y):7 9:W:g_6#(s(x),y) -> f_5#(y) -->_1 f_5#(x) -> c_7(g_5#(x,x)):1 10:W:g_6#(s(x),y) -> g_6#(x,y) -->_1 g_6#(s(x),y) -> g_6#(x,y):10 -->_1 g_6#(s(x),y) -> f_5#(y):9 11:W:g_7#(s(x),y) -> f_6#(y) -->_1 f_6#(x) -> g_6#(x,x):3 12:W:g_7#(s(x),y) -> g_7#(x,y) -->_1 g_7#(s(x),y) -> g_7#(x,y):12 -->_1 g_7#(s(x),y) -> f_6#(y):11 13:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> g_7#(x,x):4 14:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):14 -->_1 g_8#(s(x),y) -> f_7#(y):13 15:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):5 16:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):16 -->_1 g_9#(s(x),y) -> f_8#(y):15 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_5#(s(x),y) -> c_17(g_5#(x,y)) ******* Step 7.b:1.b:1.b:1.b:1.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_5#(x) -> c_7(g_5#(x,x)) g_5#(s(x),y) -> c_17(g_5#(x,y)) - Weak DPs: f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/1,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [1] x1 + [0] p(f_10) = [1] x1 + [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [4] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [3] x1 + [7] p(f_6#) = [3] x1 + [7] p(f_7#) = [3] x1 + [7] p(f_8#) = [3] x1 + [7] p(f_9#) = [6] x1 + [1] p(g_1#) = [0] p(g_10#) = [6] x2 + [1] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [4] x1 + [4] x2 + [0] p(g_5#) = [2] x1 + [1] x2 + [5] p(g_6#) = [3] x2 + [7] p(g_7#) = [3] x2 + [7] p(g_8#) = [3] x2 + [7] p(g_9#) = [2] x1 + [4] x2 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [4] x1 + [1] p(c_9) = [0] p(c_10) = [4] x1 + [0] p(c_11) = [1] x1 + [4] p(c_12) = [4] x1 + [0] p(c_13) = [1] x2 + [2] p(c_14) = [1] x2 + [0] p(c_15) = [1] x1 + [1] p(c_16) = [4] x1 + [2] x2 + [1] p(c_17) = [1] x1 + [3] p(c_18) = [1] x1 + [0] p(c_19) = [1] x1 + [4] x2 + [0] p(c_20) = [0] p(c_21) = [4] x1 + [2] x2 + [0] Following rules are strictly oriented: f_5#(x) = [3] x + [7] > [3] x + [5] = c_7(g_5#(x,x)) g_5#(s(x),y) = [2] x + [1] y + [13] > [2] x + [1] y + [8] = c_17(g_5#(x,y)) Following rules are (at-least) weakly oriented: f_6#(x) = [3] x + [7] >= [3] x + [7] = g_6#(x,x) f_7#(x) = [3] x + [7] >= [3] x + [7] = g_7#(x,x) f_8#(x) = [3] x + [7] >= [3] x + [7] = g_8#(x,x) f_9#(x) = [6] x + [1] >= [6] x + [1] = g_9#(x,x) g_10#(s(x),y) = [6] y + [1] >= [6] y + [1] = f_9#(y) g_10#(s(x),y) = [6] y + [1] >= [6] y + [1] = g_10#(x,y) g_6#(s(x),y) = [3] y + [7] >= [3] y + [7] = f_5#(y) g_6#(s(x),y) = [3] y + [7] >= [3] y + [7] = g_6#(x,y) g_7#(s(x),y) = [3] y + [7] >= [3] y + [7] = f_6#(y) g_7#(s(x),y) = [3] y + [7] >= [3] y + [7] = g_7#(x,y) g_8#(s(x),y) = [3] y + [7] >= [3] y + [7] = f_7#(y) g_8#(s(x),y) = [3] y + [7] >= [3] y + [7] = g_8#(x,y) g_9#(s(x),y) = [2] x + [4] y + [9] >= [3] y + [7] = f_8#(y) g_9#(s(x),y) = [2] x + [4] y + [9] >= [2] x + [4] y + [1] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ******* Step 7.b:1.b:1.b:1.b:1.b:1.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_5#(x) -> c_7(g_5#(x,x)) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> c_17(g_5#(x,y)) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/1,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ******* Step 7.b:1.b:1.b:1.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) - Weak DPs: f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) Further, following extension rules are added to the lower component. f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ******** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_4#(x) -> c_6(g_4#(x,x)) g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) - Weak DPs: f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_4#(x) -> c_6(g_4#(x,x)) -->_1 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):2 2:S:g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)) -->_2 g_4#(s(x),y) -> c_16(f_3#(y),g_4#(x,y)):2 3:W:f_5#(x) -> g_5#(x,x) -->_1 g_5#(s(x),y) -> g_5#(x,y):11 -->_1 g_5#(s(x),y) -> f_4#(y):10 4:W:f_6#(x) -> g_6#(x,x) -->_1 g_6#(s(x),y) -> g_6#(x,y):13 -->_1 g_6#(s(x),y) -> f_5#(y):12 5:W:f_7#(x) -> g_7#(x,x) -->_1 g_7#(s(x),y) -> g_7#(x,y):15 -->_1 g_7#(s(x),y) -> f_6#(y):14 6:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):17 -->_1 g_8#(s(x),y) -> f_7#(y):16 7:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):19 -->_1 g_9#(s(x),y) -> f_8#(y):18 8:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):7 9:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):9 -->_1 g_10#(s(x),y) -> f_9#(y):8 10:W:g_5#(s(x),y) -> f_4#(y) -->_1 f_4#(x) -> c_6(g_4#(x,x)):1 11:W:g_5#(s(x),y) -> g_5#(x,y) -->_1 g_5#(s(x),y) -> g_5#(x,y):11 -->_1 g_5#(s(x),y) -> f_4#(y):10 12:W:g_6#(s(x),y) -> f_5#(y) -->_1 f_5#(x) -> g_5#(x,x):3 13:W:g_6#(s(x),y) -> g_6#(x,y) -->_1 g_6#(s(x),y) -> g_6#(x,y):13 -->_1 g_6#(s(x),y) -> f_5#(y):12 14:W:g_7#(s(x),y) -> f_6#(y) -->_1 f_6#(x) -> g_6#(x,x):4 15:W:g_7#(s(x),y) -> g_7#(x,y) -->_1 g_7#(s(x),y) -> g_7#(x,y):15 -->_1 g_7#(s(x),y) -> f_6#(y):14 16:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> g_7#(x,x):5 17:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):17 -->_1 g_8#(s(x),y) -> f_7#(y):16 18:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):6 19:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):19 -->_1 g_9#(s(x),y) -> f_8#(y):18 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_4#(s(x),y) -> c_16(g_4#(x,y)) ******** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_4#(x) -> c_6(g_4#(x,x)) g_4#(s(x),y) -> c_16(g_4#(x,y)) - Weak DPs: f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/1,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_6) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [2] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [1] x1 + [4] p(f_5#) = [1] x1 + [4] p(f_6#) = [3] x1 + [0] p(f_7#) = [5] x1 + [4] p(f_8#) = [6] x1 + [3] p(f_9#) = [7] x1 + [2] p(g_1#) = [0] p(g_10#) = [7] x2 + [2] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [1] x1 + [5] p(g_5#) = [1] x2 + [4] p(g_6#) = [2] x1 + [1] x2 + [0] p(g_7#) = [2] x1 + [3] x2 + [4] p(g_8#) = [1] x1 + [5] x2 + [3] p(g_9#) = [1] x1 + [6] x2 + [2] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [5] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x1 + [1] p(c_17) = [1] x2 + [0] p(c_18) = [4] x1 + [1] x2 + [0] p(c_19) = [4] x2 + [2] p(c_20) = [1] x2 + [1] p(c_21) = [2] Following rules are strictly oriented: g_4#(s(x),y) = [1] x + [7] > [1] x + [6] = c_16(g_4#(x,y)) Following rules are (at-least) weakly oriented: f_4#(x) = [1] x + [4] >= [1] x + [10] = c_6(g_4#(x,x)) f_5#(x) = [1] x + [4] >= [1] x + [4] = g_5#(x,x) f_6#(x) = [3] x + [0] >= [3] x + [0] = g_6#(x,x) f_7#(x) = [5] x + [4] >= [5] x + [4] = g_7#(x,x) f_8#(x) = [6] x + [3] >= [6] x + [3] = g_8#(x,x) f_9#(x) = [7] x + [2] >= [7] x + [2] = g_9#(x,x) g_10#(s(x),y) = [7] y + [2] >= [7] y + [2] = f_9#(y) g_10#(s(x),y) = [7] y + [2] >= [7] y + [2] = g_10#(x,y) g_5#(s(x),y) = [1] y + [4] >= [1] y + [4] = f_4#(y) g_5#(s(x),y) = [1] y + [4] >= [1] y + [4] = g_5#(x,y) g_6#(s(x),y) = [2] x + [1] y + [4] >= [1] y + [4] = f_5#(y) g_6#(s(x),y) = [2] x + [1] y + [4] >= [2] x + [1] y + [0] = g_6#(x,y) g_7#(s(x),y) = [2] x + [3] y + [8] >= [3] y + [0] = f_6#(y) g_7#(s(x),y) = [2] x + [3] y + [8] >= [2] x + [3] y + [4] = g_7#(x,y) g_8#(s(x),y) = [1] x + [5] y + [5] >= [5] y + [4] = f_7#(y) g_8#(s(x),y) = [1] x + [5] y + [5] >= [1] x + [5] y + [3] = g_8#(x,y) g_9#(s(x),y) = [1] x + [6] y + [4] >= [6] y + [3] = f_8#(y) g_9#(s(x),y) = [1] x + [6] y + [4] >= [1] x + [6] y + [2] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ******** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_4#(x) -> c_6(g_4#(x,x)) - Weak DPs: f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> c_16(g_4#(x,y)) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/1,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_6) = {1}, uargs(c_16) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [1] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [1] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [2] x1 + [5] p(f_5#) = [2] x1 + [5] p(f_6#) = [6] x1 + [1] p(f_7#) = [7] x1 + [5] p(f_8#) = [7] x1 + [5] p(f_9#) = [7] x1 + [5] p(g_1#) = [0] p(g_10#) = [7] x2 + [5] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [2] x2 + [0] p(g_5#) = [2] x2 + [5] p(g_6#) = [4] x1 + [2] x2 + [1] p(g_7#) = [7] x2 + [5] p(g_8#) = [7] x2 + [5] p(g_9#) = [7] x2 + [5] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [2] x2 + [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] x1 + [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: f_4#(x) = [2] x + [5] > [2] x + [0] = c_6(g_4#(x,x)) Following rules are (at-least) weakly oriented: f_5#(x) = [2] x + [5] >= [2] x + [5] = g_5#(x,x) f_6#(x) = [6] x + [1] >= [6] x + [1] = g_6#(x,x) f_7#(x) = [7] x + [5] >= [7] x + [5] = g_7#(x,x) f_8#(x) = [7] x + [5] >= [7] x + [5] = g_8#(x,x) f_9#(x) = [7] x + [5] >= [7] x + [5] = g_9#(x,x) g_10#(s(x),y) = [7] y + [5] >= [7] y + [5] = f_9#(y) g_10#(s(x),y) = [7] y + [5] >= [7] y + [5] = g_10#(x,y) g_4#(s(x),y) = [2] y + [0] >= [2] y + [0] = c_16(g_4#(x,y)) g_5#(s(x),y) = [2] y + [5] >= [2] y + [5] = f_4#(y) g_5#(s(x),y) = [2] y + [5] >= [2] y + [5] = g_5#(x,y) g_6#(s(x),y) = [4] x + [2] y + [5] >= [2] y + [5] = f_5#(y) g_6#(s(x),y) = [4] x + [2] y + [5] >= [4] x + [2] y + [1] = g_6#(x,y) g_7#(s(x),y) = [7] y + [5] >= [6] y + [1] = f_6#(y) g_7#(s(x),y) = [7] y + [5] >= [7] y + [5] = g_7#(x,y) g_8#(s(x),y) = [7] y + [5] >= [7] y + [5] = f_7#(y) g_8#(s(x),y) = [7] y + [5] >= [7] y + [5] = g_8#(x,y) g_9#(s(x),y) = [7] y + [5] >= [7] y + [5] = f_8#(y) g_9#(s(x),y) = [7] y + [5] >= [7] y + [5] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ******** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_4#(x) -> c_6(g_4#(x,x)) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> c_16(g_4#(x,y)) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/1,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ******** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) - Weak DPs: f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) Further, following extension rules are added to the lower component. f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ********* Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_3#(x) -> c_5(g_3#(x,x)) g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) - Weak DPs: f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_3#(x) -> c_5(g_3#(x,x)) -->_1 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):2 2:S:g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)) -->_2 g_3#(s(x),y) -> c_15(f_2#(y),g_3#(x,y)):2 3:W:f_4#(x) -> g_4#(x,x) -->_1 g_4#(s(x),y) -> g_4#(x,y):12 -->_1 g_4#(s(x),y) -> f_3#(y):11 4:W:f_5#(x) -> g_5#(x,x) -->_1 g_5#(s(x),y) -> g_5#(x,y):14 -->_1 g_5#(s(x),y) -> f_4#(y):13 5:W:f_6#(x) -> g_6#(x,x) -->_1 g_6#(s(x),y) -> g_6#(x,y):16 -->_1 g_6#(s(x),y) -> f_5#(y):15 6:W:f_7#(x) -> g_7#(x,x) -->_1 g_7#(s(x),y) -> g_7#(x,y):18 -->_1 g_7#(s(x),y) -> f_6#(y):17 7:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):20 -->_1 g_8#(s(x),y) -> f_7#(y):19 8:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):22 -->_1 g_9#(s(x),y) -> f_8#(y):21 9:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):8 10:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):10 -->_1 g_10#(s(x),y) -> f_9#(y):9 11:W:g_4#(s(x),y) -> f_3#(y) -->_1 f_3#(x) -> c_5(g_3#(x,x)):1 12:W:g_4#(s(x),y) -> g_4#(x,y) -->_1 g_4#(s(x),y) -> g_4#(x,y):12 -->_1 g_4#(s(x),y) -> f_3#(y):11 13:W:g_5#(s(x),y) -> f_4#(y) -->_1 f_4#(x) -> g_4#(x,x):3 14:W:g_5#(s(x),y) -> g_5#(x,y) -->_1 g_5#(s(x),y) -> g_5#(x,y):14 -->_1 g_5#(s(x),y) -> f_4#(y):13 15:W:g_6#(s(x),y) -> f_5#(y) -->_1 f_5#(x) -> g_5#(x,x):4 16:W:g_6#(s(x),y) -> g_6#(x,y) -->_1 g_6#(s(x),y) -> g_6#(x,y):16 -->_1 g_6#(s(x),y) -> f_5#(y):15 17:W:g_7#(s(x),y) -> f_6#(y) -->_1 f_6#(x) -> g_6#(x,x):5 18:W:g_7#(s(x),y) -> g_7#(x,y) -->_1 g_7#(s(x),y) -> g_7#(x,y):18 -->_1 g_7#(s(x),y) -> f_6#(y):17 19:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> g_7#(x,x):6 20:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):20 -->_1 g_8#(s(x),y) -> f_7#(y):19 21:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):7 22:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):22 -->_1 g_9#(s(x),y) -> f_8#(y):21 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_3#(s(x),y) -> c_15(g_3#(x,y)) ********* Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_3#(x) -> c_5(g_3#(x,x)) g_3#(s(x),y) -> c_15(g_3#(x,y)) - Weak DPs: f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/1,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [3] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [3] x1 + [5] p(f_4#) = [3] x1 + [5] p(f_5#) = [6] x1 + [0] p(f_6#) = [6] x1 + [0] p(f_7#) = [6] x1 + [0] p(f_8#) = [6] x1 + [0] p(f_9#) = [7] x1 + [0] p(g_1#) = [0] p(g_10#) = [7] x2 + [0] p(g_2#) = [0] p(g_3#) = [3] x1 + [0] p(g_4#) = [3] x2 + [5] p(g_5#) = [3] x1 + [3] x2 + [0] p(g_6#) = [6] x2 + [0] p(g_7#) = [6] x2 + [0] p(g_8#) = [6] x2 + [0] p(g_9#) = [1] x1 + [6] x2 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [4] x1 + [1] x2 + [0] p(c_18) = [2] x1 + [1] x2 + [4] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [4] x1 + [0] p(c_21) = [2] x1 + [0] Following rules are strictly oriented: f_3#(x) = [3] x + [5] > [3] x + [0] = c_5(g_3#(x,x)) g_3#(s(x),y) = [3] x + [9] > [3] x + [0] = c_15(g_3#(x,y)) Following rules are (at-least) weakly oriented: f_4#(x) = [3] x + [5] >= [3] x + [5] = g_4#(x,x) f_5#(x) = [6] x + [0] >= [6] x + [0] = g_5#(x,x) f_6#(x) = [6] x + [0] >= [6] x + [0] = g_6#(x,x) f_7#(x) = [6] x + [0] >= [6] x + [0] = g_7#(x,x) f_8#(x) = [6] x + [0] >= [6] x + [0] = g_8#(x,x) f_9#(x) = [7] x + [0] >= [7] x + [0] = g_9#(x,x) g_10#(s(x),y) = [7] y + [0] >= [7] y + [0] = f_9#(y) g_10#(s(x),y) = [7] y + [0] >= [7] y + [0] = g_10#(x,y) g_4#(s(x),y) = [3] y + [5] >= [3] y + [5] = f_3#(y) g_4#(s(x),y) = [3] y + [5] >= [3] y + [5] = g_4#(x,y) g_5#(s(x),y) = [3] x + [3] y + [9] >= [3] y + [5] = f_4#(y) g_5#(s(x),y) = [3] x + [3] y + [9] >= [3] x + [3] y + [0] = g_5#(x,y) g_6#(s(x),y) = [6] y + [0] >= [6] y + [0] = f_5#(y) g_6#(s(x),y) = [6] y + [0] >= [6] y + [0] = g_6#(x,y) g_7#(s(x),y) = [6] y + [0] >= [6] y + [0] = f_6#(y) g_7#(s(x),y) = [6] y + [0] >= [6] y + [0] = g_7#(x,y) g_8#(s(x),y) = [6] y + [0] >= [6] y + [0] = f_7#(y) g_8#(s(x),y) = [6] y + [0] >= [6] y + [0] = g_8#(x,y) g_9#(s(x),y) = [1] x + [6] y + [3] >= [6] y + [0] = f_8#(y) g_9#(s(x),y) = [1] x + [6] y + [3] >= [1] x + [6] y + [0] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ********* Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> c_15(g_3#(x,y)) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/1,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ********* Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) - Weak DPs: f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) and a lower component f_1#(x) -> c_2(g_1#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) Further, following extension rules are added to the lower component. f_2#(x) -> g_2#(x,x) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> f_1#(y) g_2#(s(x),y) -> g_2#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_2#(x) -> c_4(g_2#(x,x)) g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) - Weak DPs: f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f_2#(x) -> c_4(g_2#(x,x)) -->_1 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):2 2:S:g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)) -->_2 g_2#(s(x),y) -> c_14(f_1#(y),g_2#(x,y)):2 3:W:f_3#(x) -> g_3#(x,x) -->_1 g_3#(s(x),y) -> g_3#(x,y):13 -->_1 g_3#(s(x),y) -> f_2#(y):12 4:W:f_4#(x) -> g_4#(x,x) -->_1 g_4#(s(x),y) -> g_4#(x,y):15 -->_1 g_4#(s(x),y) -> f_3#(y):14 5:W:f_5#(x) -> g_5#(x,x) -->_1 g_5#(s(x),y) -> g_5#(x,y):17 -->_1 g_5#(s(x),y) -> f_4#(y):16 6:W:f_6#(x) -> g_6#(x,x) -->_1 g_6#(s(x),y) -> g_6#(x,y):19 -->_1 g_6#(s(x),y) -> f_5#(y):18 7:W:f_7#(x) -> g_7#(x,x) -->_1 g_7#(s(x),y) -> g_7#(x,y):21 -->_1 g_7#(s(x),y) -> f_6#(y):20 8:W:f_8#(x) -> g_8#(x,x) -->_1 g_8#(s(x),y) -> g_8#(x,y):23 -->_1 g_8#(s(x),y) -> f_7#(y):22 9:W:f_9#(x) -> g_9#(x,x) -->_1 g_9#(s(x),y) -> g_9#(x,y):25 -->_1 g_9#(s(x),y) -> f_8#(y):24 10:W:g_10#(s(x),y) -> f_9#(y) -->_1 f_9#(x) -> g_9#(x,x):9 11:W:g_10#(s(x),y) -> g_10#(x,y) -->_1 g_10#(s(x),y) -> g_10#(x,y):11 -->_1 g_10#(s(x),y) -> f_9#(y):10 12:W:g_3#(s(x),y) -> f_2#(y) -->_1 f_2#(x) -> c_4(g_2#(x,x)):1 13:W:g_3#(s(x),y) -> g_3#(x,y) -->_1 g_3#(s(x),y) -> g_3#(x,y):13 -->_1 g_3#(s(x),y) -> f_2#(y):12 14:W:g_4#(s(x),y) -> f_3#(y) -->_1 f_3#(x) -> g_3#(x,x):3 15:W:g_4#(s(x),y) -> g_4#(x,y) -->_1 g_4#(s(x),y) -> g_4#(x,y):15 -->_1 g_4#(s(x),y) -> f_3#(y):14 16:W:g_5#(s(x),y) -> f_4#(y) -->_1 f_4#(x) -> g_4#(x,x):4 17:W:g_5#(s(x),y) -> g_5#(x,y) -->_1 g_5#(s(x),y) -> g_5#(x,y):17 -->_1 g_5#(s(x),y) -> f_4#(y):16 18:W:g_6#(s(x),y) -> f_5#(y) -->_1 f_5#(x) -> g_5#(x,x):5 19:W:g_6#(s(x),y) -> g_6#(x,y) -->_1 g_6#(s(x),y) -> g_6#(x,y):19 -->_1 g_6#(s(x),y) -> f_5#(y):18 20:W:g_7#(s(x),y) -> f_6#(y) -->_1 f_6#(x) -> g_6#(x,x):6 21:W:g_7#(s(x),y) -> g_7#(x,y) -->_1 g_7#(s(x),y) -> g_7#(x,y):21 -->_1 g_7#(s(x),y) -> f_6#(y):20 22:W:g_8#(s(x),y) -> f_7#(y) -->_1 f_7#(x) -> g_7#(x,x):7 23:W:g_8#(s(x),y) -> g_8#(x,y) -->_1 g_8#(s(x),y) -> g_8#(x,y):23 -->_1 g_8#(s(x),y) -> f_7#(y):22 24:W:g_9#(s(x),y) -> f_8#(y) -->_1 f_8#(x) -> g_8#(x,x):8 25:W:g_9#(s(x),y) -> g_9#(x,y) -->_1 g_9#(s(x),y) -> g_9#(x,y):25 -->_1 g_9#(s(x),y) -> f_8#(y):24 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g_2#(s(x),y) -> c_14(g_2#(x,y)) ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_2#(x) -> c_4(g_2#(x,x)) g_2#(s(x),y) -> c_14(g_2#(x,y)) - Weak DPs: f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/1,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_14) = {1} Following symbols are considered usable: {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9#,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8# ,g_9#} TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [0] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [8] p(f_3#) = [8] p(f_4#) = [8] p(f_5#) = [8] p(f_6#) = [8] p(f_7#) = [8] p(f_8#) = [8] p(f_9#) = [8] p(g_1#) = [0] p(g_10#) = [8] p(g_2#) = [0] p(g_3#) = [8] p(g_4#) = [8] p(g_5#) = [8] p(g_6#) = [8] p(g_7#) = [8] p(g_8#) = [8] p(g_9#) = [8] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [4] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [2] x1 + [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: f_2#(x) = [8] > [0] = c_4(g_2#(x,x)) Following rules are (at-least) weakly oriented: f_3#(x) = [8] >= [8] = g_3#(x,x) f_4#(x) = [8] >= [8] = g_4#(x,x) f_5#(x) = [8] >= [8] = g_5#(x,x) f_6#(x) = [8] >= [8] = g_6#(x,x) f_7#(x) = [8] >= [8] = g_7#(x,x) f_8#(x) = [8] >= [8] = g_8#(x,x) f_9#(x) = [8] >= [8] = g_9#(x,x) g_10#(s(x),y) = [8] >= [8] = f_9#(y) g_10#(s(x),y) = [8] >= [8] = g_10#(x,y) g_2#(s(x),y) = [0] >= [0] = c_14(g_2#(x,y)) g_3#(s(x),y) = [8] >= [8] = f_2#(y) g_3#(s(x),y) = [8] >= [8] = g_3#(x,y) g_4#(s(x),y) = [8] >= [8] = f_3#(y) g_4#(s(x),y) = [8] >= [8] = g_4#(x,y) g_5#(s(x),y) = [8] >= [8] = f_4#(y) g_5#(s(x),y) = [8] >= [8] = g_5#(x,y) g_6#(s(x),y) = [8] >= [8] = f_5#(y) g_6#(s(x),y) = [8] >= [8] = g_6#(x,y) g_7#(s(x),y) = [8] >= [8] = f_6#(y) g_7#(s(x),y) = [8] >= [8] = g_7#(x,y) g_8#(s(x),y) = [8] >= [8] = f_7#(y) g_8#(s(x),y) = [8] >= [8] = g_8#(x,y) g_9#(s(x),y) = [8] >= [8] = f_8#(y) g_9#(s(x),y) = [8] >= [8] = g_9#(x,y) ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_2#(s(x),y) -> c_14(g_2#(x,y)) - Weak DPs: f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/1,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_14) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [4] p(b) = [1] x2 + [4] p(f_0) = [1] x1 + [0] p(f_1) = [1] x1 + [1] p(f_10) = [1] x1 + [4] p(f_2) = [0] p(f_3) = [1] x1 + [1] p(f_4) = [1] p(f_5) = [0] p(f_6) = [4] p(f_7) = [1] x1 + [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [1] p(f_0#) = [0] p(f_1#) = [0] p(f_10#) = [0] p(f_2#) = [1] x1 + [0] p(f_3#) = [1] x1 + [0] p(f_4#) = [1] x1 + [0] p(f_5#) = [3] x1 + [0] p(f_6#) = [3] x1 + [2] p(f_7#) = [6] x1 + [1] p(f_8#) = [7] x1 + [3] p(f_9#) = [7] x1 + [4] p(g_1#) = [1] x2 + [0] p(g_10#) = [5] x1 + [7] x2 + [4] p(g_2#) = [1] x1 + [0] p(g_3#) = [1] x2 + [0] p(g_4#) = [1] x2 + [0] p(g_5#) = [2] x2 + [0] p(g_6#) = [3] x2 + [0] p(g_7#) = [2] x1 + [4] x2 + [0] p(g_8#) = [7] x2 + [2] p(g_9#) = [7] x2 + [4] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [4] x1 + [1] p(c_7) = [1] x1 + [4] p(c_8) = [2] x1 + [1] p(c_9) = [1] x1 + [2] p(c_10) = [1] x1 + [1] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x2 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [4] x1 + [2] x2 + [0] p(c_16) = [2] x1 + [4] p(c_17) = [1] x2 + [4] p(c_18) = [1] x1 + [1] p(c_19) = [1] x2 + [0] p(c_20) = [4] x1 + [1] p(c_21) = [2] x2 + [1] Following rules are strictly oriented: g_2#(s(x),y) = [1] x + [1] > [1] x + [0] = c_14(g_2#(x,y)) Following rules are (at-least) weakly oriented: f_2#(x) = [1] x + [0] >= [1] x + [0] = c_4(g_2#(x,x)) f_3#(x) = [1] x + [0] >= [1] x + [0] = g_3#(x,x) f_4#(x) = [1] x + [0] >= [1] x + [0] = g_4#(x,x) f_5#(x) = [3] x + [0] >= [2] x + [0] = g_5#(x,x) f_6#(x) = [3] x + [2] >= [3] x + [0] = g_6#(x,x) f_7#(x) = [6] x + [1] >= [6] x + [0] = g_7#(x,x) f_8#(x) = [7] x + [3] >= [7] x + [2] = g_8#(x,x) f_9#(x) = [7] x + [4] >= [7] x + [4] = g_9#(x,x) g_10#(s(x),y) = [5] x + [7] y + [9] >= [7] y + [4] = f_9#(y) g_10#(s(x),y) = [5] x + [7] y + [9] >= [5] x + [7] y + [4] = g_10#(x,y) g_3#(s(x),y) = [1] y + [0] >= [1] y + [0] = f_2#(y) g_3#(s(x),y) = [1] y + [0] >= [1] y + [0] = g_3#(x,y) g_4#(s(x),y) = [1] y + [0] >= [1] y + [0] = f_3#(y) g_4#(s(x),y) = [1] y + [0] >= [1] y + [0] = g_4#(x,y) g_5#(s(x),y) = [2] y + [0] >= [1] y + [0] = f_4#(y) g_5#(s(x),y) = [2] y + [0] >= [2] y + [0] = g_5#(x,y) g_6#(s(x),y) = [3] y + [0] >= [3] y + [0] = f_5#(y) g_6#(s(x),y) = [3] y + [0] >= [3] y + [0] = g_6#(x,y) g_7#(s(x),y) = [2] x + [4] y + [2] >= [3] y + [2] = f_6#(y) g_7#(s(x),y) = [2] x + [4] y + [2] >= [2] x + [4] y + [0] = g_7#(x,y) g_8#(s(x),y) = [7] y + [2] >= [6] y + [1] = f_7#(y) g_8#(s(x),y) = [7] y + [2] >= [7] y + [2] = g_8#(x,y) g_9#(s(x),y) = [7] y + [4] >= [7] y + [3] = f_8#(y) g_9#(s(x),y) = [7] y + [4] >= [7] y + [4] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_2#(x) -> c_4(g_2#(x,x)) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> c_14(g_2#(x,y)) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/1,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) g_1#(s(x),y) -> c_12(g_1#(x,y)) - Weak DPs: f_2#(x) -> g_2#(x,x) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> f_1#(y) g_2#(s(x),y) -> g_2#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_12) = {1} Following symbols are considered usable: {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9#,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8# ,g_9#} TcT has computed the following interpretation: p(a) = [0] p(b) = [1] x1 + [1] x2 + [0] p(f_0) = [0] p(f_1) = [0] p(f_10) = [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [0] p(f_5) = [0] p(f_6) = [0] p(f_7) = [0] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [0] p(f_0#) = [0] p(f_1#) = [4] p(f_10#) = [0] p(f_2#) = [4] p(f_3#) = [4] p(f_4#) = [4] p(f_5#) = [4] p(f_6#) = [4] p(f_7#) = [4] p(f_8#) = [4] p(f_9#) = [4] p(g_1#) = [0] p(g_10#) = [4] p(g_2#) = [4] p(g_3#) = [4] p(g_4#) = [4] p(g_5#) = [4] p(g_6#) = [4] p(g_7#) = [4] p(g_8#) = [4] p(g_9#) = [4] p(c_1) = [0] p(c_2) = [2] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: f_1#(x) = [4] > [0] = c_2(g_1#(x,x)) Following rules are (at-least) weakly oriented: f_2#(x) = [4] >= [4] = g_2#(x,x) f_3#(x) = [4] >= [4] = g_3#(x,x) f_4#(x) = [4] >= [4] = g_4#(x,x) f_5#(x) = [4] >= [4] = g_5#(x,x) f_6#(x) = [4] >= [4] = g_6#(x,x) f_7#(x) = [4] >= [4] = g_7#(x,x) f_8#(x) = [4] >= [4] = g_8#(x,x) f_9#(x) = [4] >= [4] = g_9#(x,x) g_1#(s(x),y) = [0] >= [0] = c_12(g_1#(x,y)) g_10#(s(x),y) = [4] >= [4] = f_9#(y) g_10#(s(x),y) = [4] >= [4] = g_10#(x,y) g_2#(s(x),y) = [4] >= [4] = f_1#(y) g_2#(s(x),y) = [4] >= [4] = g_2#(x,y) g_3#(s(x),y) = [4] >= [4] = f_2#(y) g_3#(s(x),y) = [4] >= [4] = g_3#(x,y) g_4#(s(x),y) = [4] >= [4] = f_3#(y) g_4#(s(x),y) = [4] >= [4] = g_4#(x,y) g_5#(s(x),y) = [4] >= [4] = f_4#(y) g_5#(s(x),y) = [4] >= [4] = g_5#(x,y) g_6#(s(x),y) = [4] >= [4] = f_5#(y) g_6#(s(x),y) = [4] >= [4] = g_6#(x,y) g_7#(s(x),y) = [4] >= [4] = f_6#(y) g_7#(s(x),y) = [4] >= [4] = g_7#(x,y) g_8#(s(x),y) = [4] >= [4] = f_7#(y) g_8#(s(x),y) = [4] >= [4] = g_8#(x,y) g_9#(s(x),y) = [4] >= [4] = f_8#(y) g_9#(s(x),y) = [4] >= [4] = g_9#(x,y) ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: g_1#(s(x),y) -> c_12(g_1#(x,y)) - Weak DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> g_2#(x,x) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> f_1#(y) g_2#(s(x),y) -> g_2#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_12) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [4] p(f_0) = [1] p(f_1) = [2] x1 + [1] p(f_10) = [1] x1 + [4] p(f_2) = [4] x1 + [0] p(f_3) = [4] x1 + [4] p(f_4) = [1] x1 + [1] p(f_5) = [0] p(f_6) = [4] x1 + [0] p(f_7) = [1] x1 + [2] p(f_8) = [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [0] p(g_7) = [0] p(g_8) = [0] p(g_9) = [0] p(s) = [1] x1 + [1] p(f_0#) = [0] p(f_1#) = [2] x1 + [0] p(f_10#) = [0] p(f_2#) = [2] x1 + [0] p(f_3#) = [2] x1 + [0] p(f_4#) = [2] x1 + [0] p(f_5#) = [2] x1 + [0] p(f_6#) = [6] x1 + [1] p(f_7#) = [6] x1 + [2] p(f_8#) = [6] x1 + [2] p(f_9#) = [7] x1 + [4] p(g_1#) = [1] x1 + [1] x2 + [0] p(g_10#) = [2] x1 + [7] x2 + [6] p(g_2#) = [2] x2 + [0] p(g_3#) = [2] x2 + [0] p(g_4#) = [2] x2 + [0] p(g_5#) = [2] x2 + [0] p(g_6#) = [2] x1 + [4] x2 + [0] p(g_7#) = [6] x2 + [1] p(g_8#) = [6] x2 + [2] p(g_9#) = [7] x2 + [2] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [4] x2 + [2] Following rules are strictly oriented: g_1#(s(x),y) = [1] x + [1] y + [1] > [1] x + [1] y + [0] = c_12(g_1#(x,y)) Following rules are (at-least) weakly oriented: f_1#(x) = [2] x + [0] >= [2] x + [0] = c_2(g_1#(x,x)) f_2#(x) = [2] x + [0] >= [2] x + [0] = g_2#(x,x) f_3#(x) = [2] x + [0] >= [2] x + [0] = g_3#(x,x) f_4#(x) = [2] x + [0] >= [2] x + [0] = g_4#(x,x) f_5#(x) = [2] x + [0] >= [2] x + [0] = g_5#(x,x) f_6#(x) = [6] x + [1] >= [6] x + [0] = g_6#(x,x) f_7#(x) = [6] x + [2] >= [6] x + [1] = g_7#(x,x) f_8#(x) = [6] x + [2] >= [6] x + [2] = g_8#(x,x) f_9#(x) = [7] x + [4] >= [7] x + [2] = g_9#(x,x) g_10#(s(x),y) = [2] x + [7] y + [8] >= [7] y + [4] = f_9#(y) g_10#(s(x),y) = [2] x + [7] y + [8] >= [2] x + [7] y + [6] = g_10#(x,y) g_2#(s(x),y) = [2] y + [0] >= [2] y + [0] = f_1#(y) g_2#(s(x),y) = [2] y + [0] >= [2] y + [0] = g_2#(x,y) g_3#(s(x),y) = [2] y + [0] >= [2] y + [0] = f_2#(y) g_3#(s(x),y) = [2] y + [0] >= [2] y + [0] = g_3#(x,y) g_4#(s(x),y) = [2] y + [0] >= [2] y + [0] = f_3#(y) g_4#(s(x),y) = [2] y + [0] >= [2] y + [0] = g_4#(x,y) g_5#(s(x),y) = [2] y + [0] >= [2] y + [0] = f_4#(y) g_5#(s(x),y) = [2] y + [0] >= [2] y + [0] = g_5#(x,y) g_6#(s(x),y) = [2] x + [4] y + [2] >= [2] y + [0] = f_5#(y) g_6#(s(x),y) = [2] x + [4] y + [2] >= [2] x + [4] y + [0] = g_6#(x,y) g_7#(s(x),y) = [6] y + [1] >= [6] y + [1] = f_6#(y) g_7#(s(x),y) = [6] y + [1] >= [6] y + [1] = g_7#(x,y) g_8#(s(x),y) = [6] y + [2] >= [6] y + [2] = f_7#(y) g_8#(s(x),y) = [6] y + [2] >= [6] y + [2] = g_8#(x,y) g_9#(s(x),y) = [7] y + [2] >= [6] y + [2] = f_8#(y) g_9#(s(x),y) = [7] y + [2] >= [7] y + [2] = g_9#(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ********** Step 7.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> g_2#(x,x) f_3#(x) -> g_3#(x,x) f_4#(x) -> g_4#(x,x) f_5#(x) -> g_5#(x,x) f_6#(x) -> g_6#(x,x) f_7#(x) -> g_7#(x,x) f_8#(x) -> g_8#(x,x) f_9#(x) -> g_9#(x,x) g_1#(s(x),y) -> c_12(g_1#(x,y)) g_10#(s(x),y) -> f_9#(y) g_10#(s(x),y) -> g_10#(x,y) g_2#(s(x),y) -> f_1#(y) g_2#(s(x),y) -> g_2#(x,y) g_3#(s(x),y) -> f_2#(y) g_3#(s(x),y) -> g_3#(x,y) g_4#(s(x),y) -> f_3#(y) g_4#(s(x),y) -> g_4#(x,y) g_5#(s(x),y) -> f_4#(y) g_5#(s(x),y) -> g_5#(x,y) g_6#(s(x),y) -> f_5#(y) g_6#(s(x),y) -> g_6#(x,y) g_7#(s(x),y) -> f_6#(y) g_7#(s(x),y) -> g_7#(x,y) g_8#(s(x),y) -> f_7#(y) g_8#(s(x),y) -> g_8#(x,y) g_9#(s(x),y) -> f_8#(y) g_9#(s(x),y) -> g_9#(x,y) - Signature: {f_0/1,f_1/1,f_10/1,f_2/1,f_3/1,f_4/1,f_5/1,f_6/1,f_7/1,f_8/1,f_9/1,g_1/2,g_10/2,g_2/2,g_3/2,g_4/2,g_5/2 ,g_6/2,g_7/2,g_8/2,g_9/2,f_0#/1,f_1#/1,f_10#/1,f_2#/1,f_3#/1,f_4#/1,f_5#/1,f_6#/1,f_7#/1,f_8#/1,f_9#/1 ,g_1#/2,g_10#/2,g_2#/2,g_3#/2,g_4#/2,g_5#/2,g_6#/2,g_7#/2,g_8#/2,g_9#/2} / {a/0,b/2,s/1,c_1/0,c_2/1,c_3/1 ,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2,c_14/2,c_15/2,c_16/2,c_17/2,c_18/2,c_19/2 ,c_20/2,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {f_0#,f_1#,f_10#,f_2#,f_3#,f_4#,f_5#,f_6#,f_7#,f_8#,f_9# ,g_1#,g_10#,g_2#,g_3#,g_4#,g_5#,g_6#,g_7#,g_8#,g_9#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^10))