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