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),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) 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)) p(s(x)) -> x - Signature: {*/2,+/2,-/2,f/2,max/2,min/2,p/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,-,f,max,min,p} 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) p#(s(x)) -> c_14() 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) p#(s(x)) -> c_14() - 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),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) 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)) p(s(x)) -> x - Signature: {*/2,+/2,-/2,f/2,max/2,min/2,p/1,*#/2,+#/2,-#/2,f#/2,max#/2,min#/2,p#/1} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1 ,c_5/0,c_6/1,c_7/5,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#,p#} 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)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) p#(s(x)) -> c_14() * 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) p#(s(x)) -> c_14() - 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)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) - Signature: {*/2,+/2,-/2,f/2,max/2,min/2,p/1,*#/2,+#/2,-#/2,f#/2,max#/2,min#/2,p#/1} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1 ,c_5/0,c_6/1,c_7/5,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#,p#} 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,14} by application of Pre({1,3,5,8,9,11,12,14}) = {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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) 14: p#(s(x)) -> c_14() * 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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() p#(s(x)) -> c_14() - 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)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) - Signature: {*/2,+/2,-/2,f/2,max/2,min/2,p/1,*#/2,+#/2,-#/2,f#/2,max#/2,min#/2,p#/1} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1 ,c_5/0,c_6/1,c_7/5,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#,p#} 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) -->_3 min#(s(x),s(y)) -> c_13(min#(x,y)):6 -->_4 max#(s(x),s(y)) -> c_10(max#(x,y)):5 -->_2 -#(x,0()) -> c_5():9 -->_1 f#(s(x),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))):4 -->_2 -#(s(x),s(y)) -> c_6(-#(x,y)):3 -->_5 *#(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() 14:W:p#(s(x)) -> c_14() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: p#(s(x)) -> c_14() 10: max#(x,0()) -> c_8() 11: max#(0(),y) -> c_9() 12: min#(x,0()) -> c_11() 13: min#(0(),y) -> c_12() 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),s(y)) -> c_7(f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ,-#(min(s(x),s(y)),max(s(x),s(y))) ,min#(s(x),s(y)) ,max#(s(x),s(y)) ,*#(s(x),s(y))) 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)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) - Signature: {*/2,+/2,-/2,f/2,max/2,min/2,p/1,*#/2,+#/2,-#/2,f#/2,max#/2,min#/2,p#/1} / {0/0,s/1,c_1/0,c_2/2,c_3/0,c_4/1 ,c_5/0,c_6/1,c_7/5,c_8/0,c_9/0,c_10/1,c_11/0,c_12/0,c_13/1,c_14/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,-#,f#,max#,min#,p#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE