MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), 0()) -> c_6() , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), 0()) -> c_10() , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , ify^#(false(), x, y) -> c_15() , if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) , if^#(false(), x, y) -> c_17() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), 0()) -> c_6() , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), 0()) -> c_10() , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , ify^#(false(), x, y) -> c_15() , if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) , if^#(false(), x, y) -> c_17() } Weak Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,6,10,15,17} by applications of Pre({1,2,6,10,15,17}) = {3,4,5,7,8,9,11,12,13,14,16}. Here rules are labeled as follows: DPs: { 1: ge^#(0(), 0()) -> c_1() , 2: ge^#(0(), s(0())) -> c_2() , 3: ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , 4: ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , 5: ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , 6: minus^#(0(), 0()) -> c_6() , 7: minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , 8: minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , 9: minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , 10: plus^#(0(), 0()) -> c_10() , 11: plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , 12: plus^#(s(x), y) -> c_12(plus^#(x, y)) , 13: div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , 14: ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , 15: ify^#(false(), x, y) -> c_15() , 16: if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) , 17: if^#(false(), x, y) -> c_17() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) } Weak DPs: { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , minus^#(0(), 0()) -> c_6() , plus^#(0(), 0()) -> c_10() , ify^#(false(), x, y) -> c_15() , if^#(false(), x, y) -> c_17() } Weak Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } 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. { ge^#(0(), 0()) -> c_1() , ge^#(0(), s(0())) -> c_2() , minus^#(0(), 0()) -> c_6() , plus^#(0(), 0()) -> c_10() , ify^#(false(), x, y) -> c_15() , if^#(false(), x, y) -> c_17() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) } Weak Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) , plus(0(), 0()) -> 0() , plus(0(), s(x)) -> s(plus(0(), x)) , plus(s(x), y) -> s(plus(x, y)) , div(x, y) -> ify(ge(y, s(0())), x, y) , ify(true(), x, y) -> if(ge(x, y), x, y) , ify(false(), x, y) -> divByZeroError() , if(true(), x, y) -> s(div(minus(x, y), y)) , if(false(), x, y) -> 0() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(0(), s(s(x))) -> c_3(ge^#(0(), s(x))) , ge^#(s(x), 0()) -> c_4(ge^#(x, 0())) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , minus^#(0(), s(x)) -> c_7(minus^#(0(), x)) , minus^#(s(x), 0()) -> c_8(minus^#(x, 0())) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , plus^#(0(), s(x)) -> c_11(plus^#(0(), x)) , plus^#(s(x), y) -> c_12(plus^#(x, y)) , div^#(x, y) -> c_13(ify^#(ge(y, s(0())), x, y), ge^#(y, s(0()))) , ify^#(true(), x, y) -> c_14(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_16(div^#(minus(x, y), y), minus^#(x, y)) } Weak Trs: { ge(0(), 0()) -> true() , ge(0(), s(0())) -> false() , ge(0(), s(s(x))) -> ge(0(), s(x)) , ge(s(x), 0()) -> ge(x, 0()) , ge(s(x), s(y)) -> ge(x, y) , minus(0(), 0()) -> 0() , minus(0(), s(x)) -> minus(0(), x) , minus(s(x), 0()) -> s(minus(x, 0())) , minus(s(x), s(y)) -> minus(x, y) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..