MAYBE * Step 1: DependencyPairs MAYBE + 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: UsableRules MAYBE + 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: UsableRules + Details: We replace rewrite rules by usable rules: 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)) * Step 3: PredecessorEstimation MAYBE + 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)) - 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 4: RemoveWeakSuffixes MAYBE + 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() - 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 5: SimplifyRHS MAYBE + 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)) - 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 6: RemoveHeads MAYBE + 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: WeightGap MAYBE + 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: WeightGap {wgDimension = 1, wgDegree = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2}, uargs(c_21) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [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) = [2] x1 + [0] p(f_8) = [2] x1 + [0] p(f_9) = [0] p(g_1) = [0] p(g_10) = [0] p(g_2) = [0] p(g_3) = [1] x2 + [0] p(g_4) = [0] p(g_5) = [0] p(g_6) = [1] x2 + [0] p(g_7) = [1] x2 + [0] p(g_8) = [2] x1 + [4] p(g_9) = [1] x1 + [4] x2 + [0] p(s) = [1] p(f_0#) = [2] x1 + [0] p(f_1#) = [5] p(f_10#) = [2] p(f_2#) = [2] p(f_3#) = [4] p(f_4#) = [0] p(f_5#) = [4] p(f_6#) = [1] p(f_7#) = [2] p(f_8#) = [4] p(f_9#) = [0] p(g_1#) = [6] p(g_10#) = [0] p(g_2#) = [0] p(g_3#) = [6] p(g_4#) = [7] p(g_5#) = [0] p(g_6#) = [7] p(g_7#) = [0] p(g_8#) = [3] p(g_9#) = [4] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [7] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [1] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [1] x1 + [1] x2 + [2] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] x1 + [1] x2 + [0] p(c_21) = [1] x1 + [1] x2 + [4] Following rules are strictly oriented: f_2#(x) = [2] > [0] = c_4(g_2#(x,x)) f_5#(x) = [4] > [0] = c_7(g_5#(x,x)) f_7#(x) = [2] > [1] = c_9(g_7#(x,x)) f_8#(x) = [4] > [3] = c_10(g_8#(x,x)) Following rules are (at-least) weakly oriented: f_1#(x) = [5] >= [6] = c_2(g_1#(x,x)) f_3#(x) = [4] >= [13] = c_5(g_3#(x,x)) f_4#(x) = [0] >= [7] = c_6(g_4#(x,x)) f_6#(x) = [1] >= [7] = c_8(g_6#(x,x)) f_9#(x) = [0] >= [4] = c_11(g_9#(x,x)) g_1#(s(x),y) = [6] >= [7] = c_12(g_1#(x,y)) g_10#(s(x),y) = [0] >= [0] = c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) = [0] >= [5] = c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) = [6] >= [10] = c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) = [7] >= [11] = c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) = [0] >= [0] = c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) = [7] >= [11] = c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) = [0] >= [1] = c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) = [3] >= [5] = c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) = [4] >= [12] = c_21(f_8#(y),g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: f_1#(x) -> c_2(g_1#(x,x)) f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_6#(x) -> c_8(g_6#(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 DPs: f_2#(x) -> c_4(g_2#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) - 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 = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2}, uargs(c_21) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [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] x1 + [0] p(g_1) = [1] 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#) = [3] p(f_10#) = [0] p(f_2#) = [0] p(f_3#) = [0] p(f_4#) = [0] p(f_5#) = [7] p(f_6#) = [0] p(f_7#) = [0] p(f_8#) = [1] p(f_9#) = [0] p(g_1#) = [2] p(g_10#) = [4] x2 + [0] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [7] p(g_6#) = [5] p(g_7#) = [0] p(g_8#) = [1] p(g_9#) = [3] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [3] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] x1 + [1] x2 + [0] p(c_21) = [1] x1 + [1] x2 + [3] Following rules are strictly oriented: f_1#(x) = [3] > [2] = c_2(g_1#(x,x)) Following rules are (at-least) weakly oriented: f_2#(x) = [0] >= [0] = c_4(g_2#(x,x)) f_3#(x) = [0] >= [0] = c_5(g_3#(x,x)) f_4#(x) = [0] >= [0] = c_6(g_4#(x,x)) f_5#(x) = [7] >= [7] = c_7(g_5#(x,x)) f_6#(x) = [0] >= [8] = c_8(g_6#(x,x)) f_7#(x) = [0] >= [0] = c_9(g_7#(x,x)) f_8#(x) = [1] >= [1] = c_10(g_8#(x,x)) f_9#(x) = [0] >= [3] = c_11(g_9#(x,x)) g_1#(s(x),y) = [2] >= [2] = c_12(g_1#(x,y)) g_10#(s(x),y) = [4] y + [0] >= [4] y + [0] = c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) = [0] >= [3] = c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) = [0] >= [0] = c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) = [0] >= [0] = c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) = [7] >= [7] = c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) = [5] >= [12] = c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) = [0] >= [0] = c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) = [1] >= [1] = c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) = [3] >= [7] = c_21(f_8#(y),g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: WeightGap MAYBE + Considered Problem: - Strict DPs: f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_6#(x) -> c_8(g_6#(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 DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_5#(x) -> c_7(g_5#(x,x)) f_7#(x) -> c_9(g_7#(x,x)) f_8#(x) -> c_10(g_8#(x,x)) - 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 = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2}, uargs(c_21) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [0] p(f_0) = [0] p(f_1) = [4] x1 + [0] p(f_10) = [1] x1 + [0] p(f_2) = [0] p(f_3) = [0] p(f_4) = [1] x1 + [2] p(f_5) = [2] p(f_6) = [4] x1 + [0] p(f_7) = [4] p(f_8) = [1] p(f_9) = [1] x1 + [0] p(g_1) = [0] p(g_10) = [2] x1 + [4] p(g_2) = [0] p(g_3) = [0] p(g_4) = [1] x1 + [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#) = [7] p(f_10#) = [0] p(f_2#) = [3] p(f_3#) = [2] p(f_4#) = [1] p(f_5#) = [0] p(f_6#) = [0] p(f_7#) = [7] p(f_8#) = [0] p(f_9#) = [7] p(g_1#) = [0] p(g_10#) = [0] p(g_2#) = [0] p(g_3#) = [2] p(g_4#) = [1] p(g_5#) = [0] p(g_6#) = [0] p(g_7#) = [4] p(g_8#) = [0] p(g_9#) = [4] p(c_1) = [0] p(c_2) = [1] x1 + [7] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [3] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [3] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [1] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [1] x2 + [4] p(c_15) = [1] x1 + [1] x2 + [4] p(c_16) = [1] x1 + [1] x2 + [7] p(c_17) = [1] x1 + [1] x2 + [7] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] x1 + [1] x2 + [1] p(c_21) = [1] x1 + [1] x2 + [4] Following rules are strictly oriented: f_9#(x) = [7] > [5] = c_11(g_9#(x,x)) Following rules are (at-least) weakly oriented: f_1#(x) = [7] >= [7] = c_2(g_1#(x,x)) f_2#(x) = [3] >= [0] = c_4(g_2#(x,x)) f_3#(x) = [2] >= [5] = c_5(g_3#(x,x)) f_4#(x) = [1] >= [1] = c_6(g_4#(x,x)) f_5#(x) = [0] >= [0] = c_7(g_5#(x,x)) f_6#(x) = [0] >= [0] = c_8(g_6#(x,x)) f_7#(x) = [7] >= [7] = c_9(g_7#(x,x)) f_8#(x) = [0] >= [0] = c_10(g_8#(x,x)) g_1#(s(x),y) = [0] >= [0] = c_12(g_1#(x,y)) g_10#(s(x),y) = [0] >= [7] = c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) = [0] >= [11] = c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) = [2] >= [9] = c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) = [1] >= [10] = c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) = [0] >= [8] = c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) = [0] >= [0] = c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) = [4] >= [4] = c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) = [0] >= [8] = c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) = [4] >= [8] = c_21(f_8#(y),g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 10: WeightGap MAYBE + Considered Problem: - Strict DPs: f_3#(x) -> c_5(g_3#(x,x)) f_4#(x) -> c_6(g_4#(x,x)) f_6#(x) -> c_8(g_6#(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 DPs: f_1#(x) -> c_2(g_1#(x,x)) f_2#(x) -> c_4(g_2#(x,x)) f_5#(x) -> c_7(g_5#(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)) - 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 = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2}, uargs(c_21) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] p(f_0) = [0] p(f_1) = [1] x1 + [0] p(f_10) = [4] x1 + [0] p(f_2) = [1] x1 + [4] p(f_3) = [1] p(f_4) = [0] p(f_5) = [0] p(f_6) = [1] x1 + [2] p(f_7) = [4] x1 + [4] p(f_8) = [2] p(f_9) = [1] p(g_1) = [1] x2 + [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#) = [0] p(f_3#) = [4] p(f_4#) = [2] p(f_5#) = [6] p(f_6#) = [0] p(f_7#) = [3] p(f_8#) = [7] p(f_9#) = [0] p(g_1#) = [4] p(g_10#) = [4] x2 + [0] p(g_2#) = [0] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [5] p(g_6#) = [0] p(g_7#) = [2] p(g_8#) = [7] p(g_9#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [2] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [1] x2 + [4] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [1] x1 + [1] x2 + [1] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] x1 + [1] x2 + [0] p(c_21) = [1] x1 + [1] x2 + [0] Following rules are strictly oriented: f_3#(x) = [4] > [0] = c_5(g_3#(x,x)) f_4#(x) = [2] > [0] = c_6(g_4#(x,x)) Following rules are (at-least) weakly oriented: f_1#(x) = [4] >= [4] = c_2(g_1#(x,x)) f_2#(x) = [0] >= [0] = c_4(g_2#(x,x)) f_5#(x) = [6] >= [5] = c_7(g_5#(x,x)) f_6#(x) = [0] >= [0] = c_8(g_6#(x,x)) f_7#(x) = [3] >= [2] = c_9(g_7#(x,x)) f_8#(x) = [7] >= [7] = c_10(g_8#(x,x)) f_9#(x) = [0] >= [0] = c_11(g_9#(x,x)) g_1#(s(x),y) = [4] >= [4] = c_12(g_1#(x,y)) g_10#(s(x),y) = [4] y + [0] >= [4] y + [0] = c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) = [0] >= [8] = c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) = [0] >= [0] = c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) = [0] >= [4] = c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) = [5] >= [7] = c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) = [0] >= [7] = c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) = [2] >= [2] = c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) = [7] >= [10] = c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) = [0] >= [7] = c_21(f_8#(y),g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 11: WeightGap MAYBE + Considered Problem: - Strict DPs: f_6#(x) -> c_8(g_6#(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 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_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)) - 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 = 0, 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 (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2}, uargs(c_21) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [1] p(f_0) = [1] p(f_1) = [2] p(f_10) = [1] x1 + [4] p(f_2) = [1] x1 + [4] p(f_3) = [0] p(f_4) = [4] x1 + [0] p(f_5) = [1] x1 + [1] p(f_6) = [1] x1 + [4] p(f_7) = [1] x1 + [4] p(f_8) = [1] p(f_9) = [1] x1 + [0] p(g_1) = [1] x2 + [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) = [2] x2 + [0] p(g_8) = [2] x2 + [0] p(g_9) = [0] p(s) = [0] p(f_0#) = [0] p(f_1#) = [3] p(f_10#) = [0] p(f_2#) = [2] p(f_3#) = [5] p(f_4#) = [7] p(f_5#) = [4] p(f_6#) = [4] p(f_7#) = [6] p(f_8#) = [3] p(f_9#) = [3] p(g_1#) = [3] p(g_10#) = [2] p(g_2#) = [1] p(g_3#) = [0] p(g_4#) = [0] p(g_5#) = [4] p(g_6#) = [0] p(g_7#) = [3] p(g_8#) = [0] p(g_9#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [3] p(c_11) = [1] x1 + [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [3] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [1] x1 + [1] x2 + [4] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [1] x2 + [1] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] x1 + [1] x2 + [6] p(c_21) = [1] x1 + [1] x2 + [4] Following rules are strictly oriented: f_6#(x) = [4] > [0] = c_8(g_6#(x,x)) Following rules are (at-least) weakly oriented: f_1#(x) = [3] >= [3] = c_2(g_1#(x,x)) f_2#(x) = [2] >= [1] = c_4(g_2#(x,x)) f_3#(x) = [5] >= [0] = c_5(g_3#(x,x)) f_4#(x) = [7] >= [0] = c_6(g_4#(x,x)) f_5#(x) = [4] >= [4] = c_7(g_5#(x,x)) f_7#(x) = [6] >= [3] = c_9(g_7#(x,x)) f_8#(x) = [3] >= [3] = c_10(g_8#(x,x)) f_9#(x) = [3] >= [0] = c_11(g_9#(x,x)) g_1#(s(x),y) = [3] >= [3] = c_12(g_1#(x,y)) g_10#(s(x),y) = [2] >= [8] = c_13(f_9#(y),g_10#(x,y)) g_2#(s(x),y) = [1] >= [4] = c_14(f_1#(y),g_2#(x,y)) g_3#(s(x),y) = [0] >= [6] = c_15(f_2#(y),g_3#(x,y)) g_4#(s(x),y) = [0] >= [5] = c_16(f_3#(y),g_4#(x,y)) g_5#(s(x),y) = [4] >= [12] = c_17(f_4#(y),g_5#(x,y)) g_6#(s(x),y) = [0] >= [4] = c_18(f_5#(y),g_6#(x,y)) g_7#(s(x),y) = [3] >= [7] = c_19(f_6#(y),g_7#(x,y)) g_8#(s(x),y) = [0] >= [12] = c_20(f_7#(y),g_8#(x,y)) g_9#(s(x),y) = [0] >= [7] = c_21(f_8#(y),g_9#(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 12: Failure MAYBE + Considered Problem: - Strict DPs: 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 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)) - 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 still open. MAYBE