MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { sort(l) -> st(0(), l) , st(n, l) -> cond1(member(n, l), n, l) , cond1(true(), n, l) -> cons(n, st(s(n), l)) , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , cond2(true(), n, l) -> nil() , cond2(false(), n, l) -> st(s(n), l) , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , member^#(n, nil()) -> c_6() , cond2^#(true(), n, l) -> c_7() , cond2^#(false(), n, l) -> c_8(st^#(s(n), l)) , gt^#(0(), v) -> c_9() , gt^#(s(u), 0()) -> c_10() , gt^#(s(u), s(v)) -> c_11(gt^#(u, v)) , max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) , max^#(nil()) -> c_13() , or^#(x, true()) -> c_14() , or^#(x, false()) -> c_15() , equal^#(0(), 0()) -> c_16() , equal^#(0(), s(y)) -> c_17() , equal^#(s(x), 0()) -> c_18() , equal^#(s(x), s(y)) -> c_19(equal^#(x, y)) , if^#(true(), u, v) -> c_20() , if^#(false(), u, v) -> c_21() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , member^#(n, nil()) -> c_6() , cond2^#(true(), n, l) -> c_7() , cond2^#(false(), n, l) -> c_8(st^#(s(n), l)) , gt^#(0(), v) -> c_9() , gt^#(s(u), 0()) -> c_10() , gt^#(s(u), s(v)) -> c_11(gt^#(u, v)) , max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) , max^#(nil()) -> c_13() , or^#(x, true()) -> c_14() , or^#(x, false()) -> c_15() , equal^#(0(), 0()) -> c_16() , equal^#(0(), s(y)) -> c_17() , equal^#(s(x), 0()) -> c_18() , equal^#(s(x), s(y)) -> c_19(equal^#(x, y)) , if^#(true(), u, v) -> c_20() , if^#(false(), u, v) -> c_21() } Weak Trs: { sort(l) -> st(0(), l) , st(n, l) -> cond1(member(n, l), n, l) , cond1(true(), n, l) -> cons(n, st(s(n), l)) , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , cond2(true(), n, l) -> nil() , cond2(false(), n, l) -> st(s(n), l) , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {6,7,9,10,13,14,15,16,17,18,20,21} by applications of Pre({6,7,9,10,13,14,15,16,17,18,20,21}) = {2,4,5,11,12,19}. Here rules are labeled as follows: DPs: { 1: sort^#(l) -> c_1(st^#(0(), l)) , 2: st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , 3: cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , 4: cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , 5: member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , 6: member^#(n, nil()) -> c_6() , 7: cond2^#(true(), n, l) -> c_7() , 8: cond2^#(false(), n, l) -> c_8(st^#(s(n), l)) , 9: gt^#(0(), v) -> c_9() , 10: gt^#(s(u), 0()) -> c_10() , 11: gt^#(s(u), s(v)) -> c_11(gt^#(u, v)) , 12: max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) , 13: max^#(nil()) -> c_13() , 14: or^#(x, true()) -> c_14() , 15: or^#(x, false()) -> c_15() , 16: equal^#(0(), 0()) -> c_16() , 17: equal^#(0(), s(y)) -> c_17() , 18: equal^#(s(x), 0()) -> c_18() , 19: equal^#(s(x), s(y)) -> c_19(equal^#(x, y)) , 20: if^#(true(), u, v) -> c_20() , 21: if^#(false(), u, v) -> c_21() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , cond2^#(false(), n, l) -> c_8(st^#(s(n), l)) , gt^#(s(u), s(v)) -> c_11(gt^#(u, v)) , max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) , equal^#(s(x), s(y)) -> c_19(equal^#(x, y)) } Weak DPs: { member^#(n, nil()) -> c_6() , cond2^#(true(), n, l) -> c_7() , gt^#(0(), v) -> c_9() , gt^#(s(u), 0()) -> c_10() , max^#(nil()) -> c_13() , or^#(x, true()) -> c_14() , or^#(x, false()) -> c_15() , equal^#(0(), 0()) -> c_16() , equal^#(0(), s(y)) -> c_17() , equal^#(s(x), 0()) -> c_18() , if^#(true(), u, v) -> c_20() , if^#(false(), u, v) -> c_21() } Weak Trs: { sort(l) -> st(0(), l) , st(n, l) -> cond1(member(n, l), n, l) , cond1(true(), n, l) -> cons(n, st(s(n), l)) , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , cond2(true(), n, l) -> nil() , cond2(false(), n, l) -> st(s(n), l) , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } 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. { member^#(n, nil()) -> c_6() , cond2^#(true(), n, l) -> c_7() , gt^#(0(), v) -> c_9() , gt^#(s(u), 0()) -> c_10() , max^#(nil()) -> c_13() , or^#(x, true()) -> c_14() , or^#(x, false()) -> c_15() , equal^#(0(), 0()) -> c_16() , equal^#(0(), s(y)) -> c_17() , equal^#(s(x), 0()) -> c_18() , if^#(true(), u, v) -> c_20() , if^#(false(), u, v) -> c_21() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , cond2^#(false(), n, l) -> c_8(st^#(s(n), l)) , gt^#(s(u), s(v)) -> c_11(gt^#(u, v)) , max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) , equal^#(s(x), s(y)) -> c_19(equal^#(x, y)) } Weak Trs: { sort(l) -> st(0(), l) , st(n, l) -> cond1(member(n, l), n, l) , cond1(true(), n, l) -> cons(n, st(s(n), l)) , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , cond2(true(), n, l) -> nil() , cond2(false(), n, l) -> st(s(n), l) , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { member^#(n, cons(m, l)) -> c_5(or^#(equal(n, m), member(n, l)), equal^#(n, m), member^#(n, l)) , max^#(cons(u, l)) -> c_12(if^#(gt(u, max(l)), u, max(l)), gt^#(u, max(l)), max^#(l), max^#(l)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) , cond2^#(false(), n, l) -> c_6(st^#(s(n), l)) , gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) , max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) , equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) } Weak Trs: { sort(l) -> st(0(), l) , st(n, l) -> cond1(member(n, l), n, l) , cond1(true(), n, l) -> cons(n, st(s(n), l)) , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , cond2(true(), n, l) -> nil() , cond2(false(), n, l) -> st(s(n), l) , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sort^#(l) -> c_1(st^#(0(), l)) , st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) , cond2^#(false(), n, l) -> c_6(st^#(s(n), l)) , gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) , max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) , equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) } Weak Trs: { member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: sort^#(l) -> c_1(st^#(0(), l)) -->_1 st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) :2 2: st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) -->_2 member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) :5 -->_1 cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) :4 -->_1 cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) :3 3: cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) -->_1 st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) :2 4: cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) -->_3 max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) :8 -->_2 gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) :7 -->_1 cond2^#(false(), n, l) -> c_6(st^#(s(n), l)) :6 5: member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) -->_1 equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) :9 -->_2 member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) :5 6: cond2^#(false(), n, l) -> c_6(st^#(s(n), l)) -->_1 st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) :2 7: gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) -->_1 gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) :7 8: max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) -->_3 max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) :8 -->_2 max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) :8 -->_1 gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) :7 9: equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) -->_1 equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) :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). { sort^#(l) -> c_1(st^#(0(), l)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { st^#(n, l) -> c_2(cond1^#(member(n, l), n, l), member^#(n, l)) , cond1^#(true(), n, l) -> c_3(st^#(s(n), l)) , cond1^#(false(), n, l) -> c_4(cond2^#(gt(n, max(l)), n, l), gt^#(n, max(l)), max^#(l)) , member^#(n, cons(m, l)) -> c_5(equal^#(n, m), member^#(n, l)) , cond2^#(false(), n, l) -> c_6(st^#(s(n), l)) , gt^#(s(u), s(v)) -> c_7(gt^#(u, v)) , max^#(cons(u, l)) -> c_8(gt^#(u, max(l)), max^#(l), max^#(l)) , equal^#(s(x), s(y)) -> c_9(equal^#(x, y)) } Weak Trs: { member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) , member(n, nil()) -> false() , gt(0(), v) -> false() , gt(s(u), 0()) -> true() , gt(s(u), s(v)) -> gt(u, v) , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) , max(nil()) -> 0() , or(x, true()) -> true() , or(x, false()) -> x , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , if(true(), u, v) -> u , if(false(), u, v) -> v } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..