MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { cond(true(), x, y) -> cond(and(gr(x, 0()), gr(y, 0())), p(x), p(y)) , and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE We add following weak dependency pairs: Strict DPs: { cond^#(true(), x, y) -> c_1(cond^#(and(gr(x, 0()), gr(y, 0())), p(x), p(y))) , and^#(x, false()) -> c_2() , and^#(true(), true()) -> c_3() , and^#(false(), x) -> c_4() , gr^#(0(), x) -> c_5() , gr^#(0(), 0()) -> c_6() , gr^#(s(x), 0()) -> c_7() , gr^#(s(x), s(y)) -> c_8(gr^#(x, y)) , p^#(0()) -> c_9() , p^#(s(x)) -> c_10() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cond^#(true(), x, y) -> c_1(cond^#(and(gr(x, 0()), gr(y, 0())), p(x), p(y))) , and^#(x, false()) -> c_2() , and^#(true(), true()) -> c_3() , and^#(false(), x) -> c_4() , gr^#(0(), x) -> c_5() , gr^#(0(), 0()) -> c_6() , gr^#(s(x), 0()) -> c_7() , gr^#(s(x), s(y)) -> c_8(gr^#(x, y)) , p^#(0()) -> c_9() , p^#(s(x)) -> c_10() } Strict Trs: { cond(true(), x, y) -> cond(and(gr(x, 0()), gr(y, 0())), p(x), p(y)) , and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Strict Usable Rules: { and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cond^#(true(), x, y) -> c_1(cond^#(and(gr(x, 0()), gr(y, 0())), p(x), p(y))) , and^#(x, false()) -> c_2() , and^#(true(), true()) -> c_3() , and^#(false(), x) -> c_4() , gr^#(0(), x) -> c_5() , gr^#(0(), 0()) -> c_6() , gr^#(s(x), 0()) -> c_7() , gr^#(s(x), s(y)) -> c_8(gr^#(x, y)) , p^#(0()) -> c_9() , p^#(s(x)) -> c_10() } Strict Trs: { and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(and) = {1, 2}, Uargs(cond^#) = {1, 2, 3}, Uargs(c_1) = {1}, Uargs(c_8) = {1} TcT has computed following constructor-restricted matrix interpretation. [true] = [0] [and](x1, x2) = [1] x1 + [1] x2 + [1] [gr](x1, x2) = [1] x2 + [1] [0] = [0] [p](x1) = [1] x1 + [1] [false] = [0] [s](x1) = [1] x1 + [1] [cond^#](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [1] [c_1](x1) = [1] x1 + [0] [and^#](x1, x2) = [2] x1 + [1] x2 + [2] [c_2] = [1] [c_3] = [1] [c_4] = [1] [gr^#](x1, x2) = [2] x1 + [2] x2 + [1] [c_5] = [1] [c_6] = [0] [c_7] = [2] [c_8](x1) = [1] x1 + [1] [p^#](x1) = [2] x1 + [2] [c_9] = [1] [c_10] = [1] This order satisfies following ordering constraints: [and(x, false())] = [1] x + [1] > [0] = [false()] [and(true(), true())] = [1] > [0] = [true()] [and(false(), x)] = [1] x + [1] > [0] = [false()] [gr(0(), x)] = [1] x + [1] > [0] = [false()] [gr(0(), 0())] = [1] > [0] = [false()] [gr(s(x), 0())] = [1] > [0] = [true()] [gr(s(x), s(y))] = [1] y + [2] > [1] y + [1] = [gr(x, y)] [p(0())] = [1] > [0] = [0()] [p(s(x))] = [1] x + [2] > [1] x + [0] = [x] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cond^#(true(), x, y) -> c_1(cond^#(and(gr(x, 0()), gr(y, 0())), p(x), p(y))) , gr^#(0(), x) -> c_5() } Weak DPs: { and^#(x, false()) -> c_2() , and^#(true(), true()) -> c_3() , and^#(false(), x) -> c_4() , gr^#(0(), 0()) -> c_6() , gr^#(s(x), 0()) -> c_7() , gr^#(s(x), s(y)) -> c_8(gr^#(x, y)) , p^#(0()) -> c_9() , p^#(s(x)) -> c_10() } Weak Trs: { and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } 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. { and^#(x, false()) -> c_2() , and^#(true(), true()) -> c_3() , and^#(false(), x) -> c_4() , gr^#(0(), 0()) -> c_6() , gr^#(s(x), 0()) -> c_7() , p^#(0()) -> c_9() , p^#(s(x)) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cond^#(true(), x, y) -> c_1(cond^#(and(gr(x, 0()), gr(y, 0())), p(x), p(y))) , gr^#(0(), x) -> c_5() } Weak DPs: { gr^#(s(x), s(y)) -> c_8(gr^#(x, y)) } Weak Trs: { and(x, false()) -> false() , and(true(), true()) -> true() , and(false(), x) -> false() , gr(0(), x) -> false() , gr(0(), 0()) -> false() , gr(s(x), 0()) -> true() , gr(s(x), s(y)) -> gr(x, y) , p(0()) -> 0() , p(s(x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..