MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) f(s(x)) -> f(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) - Signature: {*/2,+/2,-/2,f/1,max/2,min/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,-,f,max,min} and constructors {0,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(x,0()) -> c_1() *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(0(),y) -> c_3() +#(s(x),y) -> c_4(+#(x,y)) -#(x,0()) -> c_5() -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(x,0()) -> c_8() max#(0(),y) -> c_9() max#(s(x),s(y)) -> c_10(max#(x,y)) min#(x,0()) -> c_11() min#(0(),y) -> c_12() min#(s(x),s(y)) -> c_13(min#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(0(),y) -> c_3() +#(s(x),y) -> c_4(+#(x,y)) -#(x,0()) -> c_5() -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(x,0()) -> c_8() max#(0(),y) -> c_9() max#(s(x),s(y)) -> c_10(max#(x,y)) min#(x,0()) -> c_11() min#(0(),y) -> c_12() min#(s(x),s(y)) -> c_13(min#(x,y)) - Weak TRS: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) f(s(x)) -> f(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) - Signature: {*/2,+/2,-/2,f/1,max/2,min/2,*#/2,+#/2,-#/2,f#/1,max#/2,min#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0 ,c_6/1,c_7/8,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#} and constructors {0,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) *#(x,0()) -> c_1() *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(0(),y) -> c_3() +#(s(x),y) -> c_4(+#(x,y)) -#(x,0()) -> c_5() -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(x,0()) -> c_8() max#(0(),y) -> c_9() max#(s(x),s(y)) -> c_10(max#(x,y)) min#(x,0()) -> c_11() min#(0(),y) -> c_12() min#(s(x),s(y)) -> c_13(min#(x,y)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(x,0()) -> c_1() *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(0(),y) -> c_3() +#(s(x),y) -> c_4(+#(x,y)) -#(x,0()) -> c_5() -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(x,0()) -> c_8() max#(0(),y) -> c_9() max#(s(x),s(y)) -> c_10(max#(x,y)) min#(x,0()) -> c_11() min#(0(),y) -> c_12() min#(s(x),s(y)) -> c_13(min#(x,y)) - Weak TRS: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) - Signature: {*/2,+/2,-/2,f/1,max/2,min/2,*#/2,+#/2,-#/2,f#/1,max#/2,min#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0 ,c_6/1,c_7/8,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#} and constructors {0,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,8,9,11,12} by application of Pre({1,3,5,8,9,11,12}) = {2,4,6,7,10,13}. Here rules are labelled as follows: 1: *#(x,0()) -> c_1() 2: *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) 3: +#(0(),y) -> c_3() 4: +#(s(x),y) -> c_4(+#(x,y)) 5: -#(x,0()) -> c_5() 6: -#(s(x),s(y)) -> c_6(-#(x,y)) 7: f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) 8: max#(x,0()) -> c_8() 9: max#(0(),y) -> c_9() 10: max#(s(x),s(y)) -> c_10(max#(x,y)) 11: min#(x,0()) -> c_11() 12: min#(0(),y) -> c_12() 13: min#(s(x),s(y)) -> c_13(min#(x,y)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(s(x),y) -> c_4(+#(x,y)) -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(s(x),s(y)) -> c_10(max#(x,y)) min#(s(x),s(y)) -> c_13(min#(x,y)) - Weak DPs: *#(x,0()) -> c_1() +#(0(),y) -> c_3() -#(x,0()) -> c_5() max#(x,0()) -> c_8() max#(0(),y) -> c_9() min#(x,0()) -> c_11() min#(0(),y) -> c_12() - Weak TRS: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) - Signature: {*/2,+/2,-/2,f/1,max/2,min/2,*#/2,+#/2,-#/2,f#/1,max#/2,min#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0 ,c_6/1,c_7/8,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) -->_1 +#(s(x),y) -> c_4(+#(x,y)):2 -->_1 +#(0(),y) -> c_3():8 -->_2 *#(x,0()) -> c_1():7 -->_2 *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)):1 2:S:+#(s(x),y) -> c_4(+#(x,y)) -->_1 +#(0(),y) -> c_3():8 -->_1 +#(s(x),y) -> c_4(+#(x,y)):2 3:S:-#(s(x),s(y)) -> c_6(-#(x,y)) -->_1 -#(x,0()) -> c_5():9 -->_1 -#(s(x),s(y)) -> c_6(-#(x,y)):3 4:S:f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) -->_6 max#(s(x),s(y)) -> c_10(max#(x,y)):5 -->_3 max#(s(x),s(y)) -> c_10(max#(x,y)):5 -->_3 max#(0(),y) -> c_9():11 -->_6 max#(x,0()) -> c_8():10 -->_3 max#(x,0()) -> c_8():10 -->_2 -#(x,0()) -> c_5():9 -->_1 f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))):4 -->_2 -#(s(x),s(y)) -> c_6(-#(x,y)):3 -->_8 +#(s(x),y) -> c_4(+#(x,y)):2 -->_5 +#(s(x),y) -> c_4(+#(x,y)):2 -->_7 *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)):1 -->_4 *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)):1 5:S:max#(s(x),s(y)) -> c_10(max#(x,y)) -->_1 max#(0(),y) -> c_9():11 -->_1 max#(x,0()) -> c_8():10 -->_1 max#(s(x),s(y)) -> c_10(max#(x,y)):5 6:S:min#(s(x),s(y)) -> c_13(min#(x,y)) -->_1 min#(0(),y) -> c_12():13 -->_1 min#(x,0()) -> c_11():12 -->_1 min#(s(x),s(y)) -> c_13(min#(x,y)):6 7:W:*#(x,0()) -> c_1() 8:W:+#(0(),y) -> c_3() 9:W:-#(x,0()) -> c_5() 10:W:max#(x,0()) -> c_8() 11:W:max#(0(),y) -> c_9() 12:W:min#(x,0()) -> c_11() 13:W:min#(0(),y) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: min#(x,0()) -> c_11() 13: min#(0(),y) -> c_12() 10: max#(x,0()) -> c_8() 11: max#(0(),y) -> c_9() 9: -#(x,0()) -> c_5() 7: *#(x,0()) -> c_1() 8: +#(0(),y) -> c_3() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: *#(x,s(y)) -> c_2(+#(x,*(x,y)),*#(x,y)) +#(s(x),y) -> c_4(+#(x,y)) -#(s(x),s(y)) -> c_6(-#(x,y)) f#(s(x)) -> c_7(f#(-(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))))) ,-#(max(*(s(x),s(x)),+(s(x),s(s(s(0()))))),max(s(*(s(x),s(x))),+(s(x),s(s(s(s(0()))))))) ,max#(*(s(x),s(x)),+(s(x),s(s(s(0()))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(0())))) ,max#(s(*(s(x),s(x))),+(s(x),s(s(s(s(0())))))) ,*#(s(x),s(x)) ,+#(s(x),s(s(s(s(0())))))) max#(s(x),s(y)) -> c_10(max#(x,y)) min#(s(x),s(y)) -> c_13(min#(x,y)) - Weak TRS: *(x,0()) -> 0() *(x,s(y)) -> +(x,*(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) -(x,0()) -> x -(s(x),s(y)) -> -(x,y) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) - Signature: {*/2,+/2,-/2,f/1,max/2,min/2,*#/2,+#/2,-#/2,f#/1,max#/2,min#/2} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1,c_5/0 ,c_6/1,c_7/8,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE