MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { minus(x, x) -> 0() , minus(x, y) -> cond(equal(min(x, y), y), x, y) , cond(true(), x, y) -> s(minus(x, s(y))) , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, v)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { minus^#(x, x) -> c_1() , minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , equal^#(0(), 0()) -> c_4() , equal^#(0(), s(y)) -> c_5() , equal^#(s(x), 0()) -> c_6() , equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , min^#(u, 0()) -> c_8() , min^#(0(), v) -> c_9() , min^#(s(u), s(v)) -> c_10(min^#(u, v)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, x) -> c_1() , minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , equal^#(0(), 0()) -> c_4() , equal^#(0(), s(y)) -> c_5() , equal^#(s(x), 0()) -> c_6() , equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , min^#(u, 0()) -> c_8() , min^#(0(), v) -> c_9() , min^#(s(u), s(v)) -> c_10(min^#(u, v)) } Weak Trs: { minus(x, x) -> 0() , minus(x, y) -> cond(equal(min(x, y), y), x, y) , cond(true(), x, y) -> s(minus(x, s(y))) , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, v)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,4,5,6,8,9} by applications of Pre({1,4,5,6,8,9}) = {2,3,7,10}. Here rules are labeled as follows: DPs: { 1: minus^#(x, x) -> c_1() , 2: minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , 3: cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , 4: equal^#(0(), 0()) -> c_4() , 5: equal^#(0(), s(y)) -> c_5() , 6: equal^#(s(x), 0()) -> c_6() , 7: equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , 8: min^#(u, 0()) -> c_8() , 9: min^#(0(), v) -> c_9() , 10: min^#(s(u), s(v)) -> c_10(min^#(u, v)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , min^#(s(u), s(v)) -> c_10(min^#(u, v)) } Weak DPs: { minus^#(x, x) -> c_1() , equal^#(0(), 0()) -> c_4() , equal^#(0(), s(y)) -> c_5() , equal^#(s(x), 0()) -> c_6() , min^#(u, 0()) -> c_8() , min^#(0(), v) -> c_9() } Weak Trs: { minus(x, x) -> 0() , minus(x, y) -> cond(equal(min(x, y), y), x, y) , cond(true(), x, y) -> s(minus(x, s(y))) , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, 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. { minus^#(x, x) -> c_1() , equal^#(0(), 0()) -> c_4() , equal^#(0(), s(y)) -> c_5() , equal^#(s(x), 0()) -> c_6() , min^#(u, 0()) -> c_8() , min^#(0(), v) -> c_9() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , min^#(s(u), s(v)) -> c_10(min^#(u, v)) } Weak Trs: { minus(x, x) -> 0() , minus(x, y) -> cond(equal(min(x, y), y), x, y) , cond(true(), x, y) -> s(minus(x, s(y))) , equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, v)) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, v)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { minus^#(x, y) -> c_2(cond^#(equal(min(x, y), y), x, y), equal^#(min(x, y), y), min^#(x, y)) , cond^#(true(), x, y) -> c_3(minus^#(x, s(y))) , equal^#(s(x), s(y)) -> c_7(equal^#(x, y)) , min^#(s(u), s(v)) -> c_10(min^#(u, v)) } Weak Trs: { equal(0(), 0()) -> true() , equal(0(), s(y)) -> false() , equal(s(x), 0()) -> false() , equal(s(x), s(y)) -> equal(x, y) , min(u, 0()) -> 0() , min(0(), v) -> 0() , min(s(u), s(v)) -> s(min(u, v)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..