MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() , average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y) , if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y) , if(false(), b1, b2, b3, x, y) -> average(p(x), s(y)) , if2(true(), b2, b3, x, y) -> 0() , if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y) , if3(true(), b3, x, y) -> 0() , if3(false(), b3, x, y) -> if4(b3, x, y) , if4(true(), x, y) -> s(0()) , if4(false(), x, y) -> average(s(x), p(p(y))) } Obligation: innermost runtime complexity Answer: MAYBE We add following weak dependency pairs: Strict DPs: { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), s(y)) -> c_3(le^#(x, y)) , le^#(s(x), 0()) -> c_4() , le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(true(), b2, b3, x, y) -> c_9() , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(true(), b3, x, y) -> c_11() , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(true(), x, y) -> c_13() , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), s(y)) -> c_3(le^#(x, y)) , le^#(s(x), 0()) -> c_4() , le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(true(), b2, b3, x, y) -> c_9() , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(true(), b3, x, y) -> c_11() , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(true(), x, y) -> c_13() , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } Strict Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() , average(x, y) -> if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y) , if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y) , if(false(), b1, b2, b3, x, y) -> average(p(x), s(y)) , if2(true(), b2, b3, x, y) -> 0() , if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y) , if3(true(), b3, x, y) -> 0() , if3(false(), b3, x, y) -> if4(b3, x, y) , if4(true(), x, y) -> s(0()) , if4(false(), x, y) -> average(s(x), p(p(y))) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Strict Usable Rules: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), s(y)) -> c_3(le^#(x, y)) , le^#(s(x), 0()) -> c_4() , le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(true(), b2, b3, x, y) -> c_9() , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(true(), b3, x, y) -> c_11() , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(true(), x, y) -> c_13() , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } Strict Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(p) = {1}, Uargs(c_3) = {1}, Uargs(average^#) = {1, 2}, Uargs(c_6) = {1}, Uargs(if^#) = {1, 2, 3, 4}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_10) = {1}, Uargs(c_12) = {1}, Uargs(c_14) = {1} TcT has computed following constructor-restricted matrix interpretation. [p](x1) = [1] x1 + [1] [s](x1) = [1] x1 + [1] [0] = [0] [le](x1, x2) = [1] x2 + [1] [true] = [0] [false] = [0] [p^#](x1) = [2] x1 + [2] [c_1] = [1] [c_2] = [1] [le^#](x1, x2) = [1] x1 + [2] x2 + [1] [c_3](x1) = [1] x1 + [1] [c_4] = [1] [c_5] = [2] [average^#](x1, x2) = [1] x1 + [1] x2 + [1] [c_6](x1) = [1] x1 + [0] [if^#](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [1] x6 + [0] [c_7](x1) = [1] x1 + [1] [if2^#](x1, x2, x3, x4, x5) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1] x5 + [2] [c_8](x1) = [1] x1 + [1] [c_9] = [1] [c_10](x1) = [1] x1 + [1] [if3^#](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [2] [c_11] = [2] [c_12](x1) = [1] x1 + [1] [if4^#](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [c_13] = [1] [c_14](x1) = [1] x1 + [2] This order satisfies following ordering constraints: [p(s(x))] = [1] x + [2] > [1] x + [0] = [x] [p(0())] = [1] > [0] = [0()] [le(s(x), s(y))] = [1] y + [2] > [1] y + [1] = [le(x, y)] [le(s(x), 0())] = [1] > [0] = [false()] [le(0(), y)] = [1] y + [1] > [0] = [true()] 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: { le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(true(), b3, x, y) -> c_11() , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } Weak DPs: { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), s(y)) -> c_3(le^#(x, y)) , le^#(s(x), 0()) -> c_4() , if2^#(true(), b2, b3, x, y) -> c_9() , if4^#(true(), x, y) -> c_13() } Weak Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {6} by applications of Pre({6}) = {5}. Here rules are labeled as follows: DPs: { 1: le^#(0(), y) -> c_5() , 2: average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , 3: if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , 4: if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , 5: if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , 6: if3^#(true(), b3, x, y) -> c_11() , 7: if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , 8: if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) , 9: p^#(s(x)) -> c_1() , 10: p^#(0()) -> c_2() , 11: le^#(s(x), s(y)) -> c_3(le^#(x, y)) , 12: le^#(s(x), 0()) -> c_4() , 13: if2^#(true(), b2, b3, x, y) -> c_9() , 14: if4^#(true(), x, y) -> c_13() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } Weak DPs: { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), s(y)) -> c_3(le^#(x, y)) , le^#(s(x), 0()) -> c_4() , if2^#(true(), b2, b3, x, y) -> c_9() , if3^#(true(), b3, x, y) -> c_11() , if4^#(true(), x, y) -> c_13() } Weak Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() } 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. { p^#(s(x)) -> c_1() , p^#(0()) -> c_2() , le^#(s(x), 0()) -> c_4() , if2^#(true(), b2, b3, x, y) -> c_9() , if3^#(true(), b3, x, y) -> c_11() , if4^#(true(), x, y) -> c_13() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { le^#(0(), y) -> c_5() , average^#(x, y) -> c_6(if^#(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)) , if^#(true(), b1, b2, b3, x, y) -> c_7(if2^#(b1, b2, b3, x, y)) , if^#(false(), b1, b2, b3, x, y) -> c_8(average^#(p(x), s(y))) , if2^#(false(), b2, b3, x, y) -> c_10(if3^#(b2, b3, x, y)) , if3^#(false(), b3, x, y) -> c_12(if4^#(b3, x, y)) , if4^#(false(), x, y) -> c_14(average^#(s(x), p(p(y)))) } Weak DPs: { le^#(s(x), s(y)) -> c_3(le^#(x, y)) } Weak Trs: { p(s(x)) -> x , p(0()) -> 0() , le(s(x), s(y)) -> le(x, y) , le(s(x), 0()) -> false() , le(0(), y) -> true() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..