YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { f(0()) -> true() , f(1()) -> false() , f(s(x)) -> f(x) , if(true(), s(x), s(y)) -> s(x) , if(false(), s(x), s(y)) -> s(y) , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) , g(x, c(y)) -> c(g(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add the following dependency tuples: Strict DPs: { f^#(0()) -> c_1() , f^#(1()) -> c_2() , f^#(s(x)) -> c_3(f^#(x)) , if^#(true(), s(x), s(y)) -> c_4() , if^#(false(), s(x), s(y)) -> c_5() , g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) , g^#(x, c(y)) -> c_7(g^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { f^#(0()) -> c_1() , f^#(1()) -> c_2() , f^#(s(x)) -> c_3(f^#(x)) , if^#(true(), s(x), s(y)) -> c_4() , if^#(false(), s(x), s(y)) -> c_5() , g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) , g^#(x, c(y)) -> c_7(g^#(x, y)) } Weak Trs: { f(0()) -> true() , f(1()) -> false() , f(s(x)) -> f(x) , if(true(), s(x), s(y)) -> s(x) , if(false(), s(x), s(y)) -> s(y) , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) , g(x, c(y)) -> c(g(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,2,4,5} by applications of Pre({1,2,4,5}) = {3,6}. Here rules are labeled as follows: DPs: { 1: f^#(0()) -> c_1() , 2: f^#(1()) -> c_2() , 3: f^#(s(x)) -> c_3(f^#(x)) , 4: if^#(true(), s(x), s(y)) -> c_4() , 5: if^#(false(), s(x), s(y)) -> c_5() , 6: g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) , 7: g^#(x, c(y)) -> c_7(g^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { f^#(s(x)) -> c_3(f^#(x)) , g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) , g^#(x, c(y)) -> c_7(g^#(x, y)) } Weak DPs: { f^#(0()) -> c_1() , f^#(1()) -> c_2() , if^#(true(), s(x), s(y)) -> c_4() , if^#(false(), s(x), s(y)) -> c_5() } Weak Trs: { f(0()) -> true() , f(1()) -> false() , f(s(x)) -> f(x) , if(true(), s(x), s(y)) -> s(x) , if(false(), s(x), s(y)) -> s(y) , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) , g(x, c(y)) -> c(g(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(0()) -> c_1() , f^#(1()) -> c_2() , if^#(true(), s(x), s(y)) -> c_4() , if^#(false(), s(x), s(y)) -> c_5() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { f^#(s(x)) -> c_3(f^#(x)) , g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) , g^#(x, c(y)) -> c_7(g^#(x, y)) } Weak Trs: { f(0()) -> true() , f(1()) -> false() , f(s(x)) -> f(x) , if(true(), s(x), s(y)) -> s(x) , if(false(), s(x), s(y)) -> s(y) , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) , g(x, c(y)) -> c(g(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { g^#(x, c(y)) -> c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))), if^#(f(x), c(g(s(x), y)), c(y)), f^#(x), g^#(s(x), y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { f^#(s(x)) -> c_1(f^#(x)) , g^#(x, c(y)) -> c_2(g^#(x, y)) , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } Weak Trs: { f(0()) -> true() , f(1()) -> false() , f(s(x)) -> f(x) , if(true(), s(x), s(y)) -> s(x) , if(false(), s(x), s(y)) -> s(y) , g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y))) , g(x, c(y)) -> c(g(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { f^#(s(x)) -> c_1(f^#(x)) , g^#(x, c(y)) -> c_2(g^#(x, y)) , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. DPs: { 1: f^#(s(x)) -> c_1(f^#(x)) } Sub-proof: ---------- The following argument positions are considered usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} TcT has computed the following constructor-restricted polynomial interpretation. [f](x1) = 3*x1 + 3*x1^2 [0]() = 0 [true]() = 0 [1]() = 0 [false]() = 0 [s](x1) = 1 + x1 [if](x1, x2, x3) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2^2 + 3*x3 + 3*x3^2 [g](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2 [c](x1) = 1 + x1 [f^#](x1) = x1 [c_1]() = 0 [c_2]() = 0 [c_3](x1) = 3*x1 + 3*x1^2 [if^#](x1, x2, x3) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2^2 + 3*x3 + 3*x3^2 [c_4]() = 0 [c_5]() = 0 [g^#](x1, x2) = x1*x2 + x2^2 [c_6](x1, x2, x3, x4) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1*x4 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2*x4 + 3*x2^2 + 3*x3 + 3*x3*x4 + 3*x3^2 + 3*x4 + 3*x4^2 [c_7](x1) = 3*x1 + 3*x1^2 [c]() = 0 [c_1](x1) = x1 [c_2](x1) = 1 + x1 [c_3](x1, x2) = 1 + x1 + x2 The following symbols are considered usable {f^#, if^#, g^#} This order satisfies the following ordering constraints. [f^#(s(x))] = 1 + x > x = [c_1(f^#(x))] [g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2 >= 1 + x*y + y^2 = [c_2(g^#(x, y))] [g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2 >= 1 + x + y + x*y + y^2 = [c_3(f^#(x), g^#(s(x), y))] The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { g^#(x, c(y)) -> c_2(g^#(x, y)) , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } Weak DPs: { f^#(s(x)) -> c_1(f^#(x)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { f^#(s(x)) -> c_1(f^#(x)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { g^#(x, c(y)) -> c_2(g^#(x, y)) , g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { g^#(x, c(y)) -> c_1(g^#(x, y)) , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. DPs: { 1: g^#(x, c(y)) -> c_1(g^#(x, y)) , 2: g^#(x, c(y)) -> c_2(g^#(s(x), y)) } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(f) = {}, safe(0) = {}, safe(true) = {}, safe(1) = {}, safe(false) = {}, safe(s) = {1}, safe(if) = {}, safe(g) = {}, safe(c) = {1}, safe(f^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(if^#) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(g^#) = {1}, safe(c_6) = {}, safe(c_7) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {} and precedence empty . Following symbols are considered recursive: {g^#} The recursion depth is 1. Further, following argument filtering is employed: pi(f) = [], pi(0) = [], pi(true) = [], pi(1) = [], pi(false) = [], pi(s) = 1, pi(if) = [], pi(g) = [], pi(c) = [1], pi(f^#) = [], pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(if^#) = [], pi(c_4) = [], pi(c_5) = [], pi(g^#) = [1, 2], pi(c_6) = [], pi(c_7) = [], pi(c) = [], pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(c) = [], pi(c_1) = [1], pi(c_2) = [1] Usable defined function symbols are a subset of: {f^#, if^#, g^#} For your convenience, here are the satisfied ordering constraints: pi(g^#(x, c(y))) = g^#(c(; y); x) > c_1(g^#(y; x);) = pi(c_1(g^#(x, y))) pi(g^#(x, c(y))) = g^#(c(; y); x) > c_2(g^#(y; x);) = pi(c_2(g^#(s(x), y))) The strictly oriented rules are moved into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { g^#(x, c(y)) -> c_1(g^#(x, y)) , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { g^#(x, c(y)) -> c_1(g^#(x, y)) , g^#(x, c(y)) -> c_2(g^#(s(x), y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))