MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs))))) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2() , max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, nil()) -> c_10() , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , if2^#(true(), x, y, xs) -> c_12() , if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(nil()) -> c_18() , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , h^#(nil()) -> c_20() , h^#(cons(x, xs)) -> c_21(h^#(xs)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2() , max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, nil()) -> c_10() , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , if2^#(true(), x, y, xs) -> c_12() , if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(nil()) -> c_18() , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , h^#(nil()) -> c_20() , h^#(cons(x, xs)) -> c_21(h^#(xs)) } Weak Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs))))) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,6,7,8,10,12,14,15,16,18,20} by applications of Pre({1,2,6,7,8,10,12,14,15,16,18,20}) = {3,4,5,9,11,13,17,19,21}. Here rules are labeled as follows: DPs: { 1: max^#(nil()) -> c_1() , 2: max^#(cons(x, nil())) -> c_2() , 3: max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , 4: if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , 5: if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , 6: ge^#(0(), 0()) -> c_6() , 7: ge^#(0(), s(x)) -> c_7() , 8: ge^#(s(x), 0()) -> c_8() , 9: ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , 10: del^#(x, nil()) -> c_10() , 11: del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , 12: if2^#(true(), x, y, xs) -> c_12() , 13: if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , 14: eq^#(0(), 0()) -> c_14() , 15: eq^#(0(), s(y)) -> c_15() , 16: eq^#(s(x), 0()) -> c_16() , 17: eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , 18: sort^#(nil()) -> c_18() , 19: sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , 20: h^#(nil()) -> c_20() , 21: h^#(cons(x, xs)) -> c_21(h^#(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , h^#(cons(x, xs)) -> c_21(h^#(xs)) } Weak DPs: { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2() , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , del^#(x, nil()) -> c_10() , if2^#(true(), x, y, xs) -> c_12() , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , sort^#(nil()) -> c_18() , h^#(nil()) -> c_20() } Weak Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs))))) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { max^#(nil()) -> c_1() , max^#(cons(x, nil())) -> c_2() , ge^#(0(), 0()) -> c_6() , ge^#(0(), s(x)) -> c_7() , ge^#(s(x), 0()) -> c_8() , del^#(x, nil()) -> c_10() , if2^#(true(), x, y, xs) -> c_12() , eq^#(0(), 0()) -> c_14() , eq^#(0(), s(y)) -> c_15() , eq^#(s(x), 0()) -> c_16() , sort^#(nil()) -> c_18() , h^#(nil()) -> c_20() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , h^#(cons(x, xs)) -> c_21(h^#(xs)) } Weak Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , sort(nil()) -> nil() , sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs))))) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { max^#(cons(x, cons(y, xs))) -> c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y)) , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs))) , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , del^#(x, cons(y, xs)) -> c_11(if2^#(eq(x, y), x, y, xs), eq^#(x, y)) , if2^#(false(), x, y, xs) -> c_13(del^#(x, xs)) , eq^#(s(x), s(y)) -> c_17(eq^#(x, y)) , sort^#(cons(x, xs)) -> c_19(max^#(cons(x, xs)), sort^#(h(del(max(cons(x, xs)), cons(x, xs)))), h^#(del(max(cons(x, xs)), cons(x, xs))), del^#(max(cons(x, xs)), cons(x, xs)), max^#(cons(x, xs))) , h^#(cons(x, xs)) -> c_21(h^#(xs)) } Weak Trs: { max(nil()) -> 0() , max(cons(x, nil())) -> x , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) , if1(true(), x, y, xs) -> max(cons(x, xs)) , if1(false(), x, y, xs) -> max(cons(y, xs)) , ge(0(), 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , del(x, nil()) -> nil() , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) , if2(true(), x, y, xs) -> xs , if2(false(), x, y, xs) -> cons(y, del(x, xs)) , eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , h(nil()) -> nil() , h(cons(x, xs)) -> cons(x, h(xs)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..