We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) , p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add the following dependency tuples: Strict DPs: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , p^#(s(s(x))) -> c_2(p^#(s(x))) , p^#(s(0())) -> c_3() } 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: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , p^#(s(s(x))) -> c_2(p^#(s(x))) , p^#(s(0())) -> c_3() } Weak Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) , p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {3} by applications of Pre({3}) = {1,2}. Here rules are labeled as follows: DPs: { 1: fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , 2: p^#(s(s(x))) -> c_2(p^#(s(x))) , 3: p^#(s(0())) -> c_3() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , p^#(s(s(x))) -> c_2(p^#(s(x))) } Weak DPs: { p^#(s(0())) -> c_3() } Weak Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) , p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } 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. { p^#(s(0())) -> c_3() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , p^#(s(s(x))) -> c_2(p^#(s(x))) } Weak Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) , p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) , p^#(s(s(x))) -> c_2(p^#(s(x))) } Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) } and lower component { p^#(s(s(x))) -> c_2(p^#(s(x))) } Further, following extension rules are added to the lower component. { fac^#(s(x)) -> fac^#(p(s(x))) , fac^#(s(x)) -> p^#(s(x)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) } Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 1: fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) } Trs: { p(s(0())) -> 0() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [s](x1) = [1 0] x1 + [2] [1 0] [1] [p](x1) = [0 1] x1 + [0] [0 1] [0] [0] = [0] [0] [fac^#](x1) = [1 3] x1 + [4] [0 0] [0] [c_1](x1, x2) = [1 1] x1 + [0 1] x2 + [0] [0 0] [0 0] [0] [p^#](x1) = [1 0] x1 + [0] [0 0] [0] The order satisfies the following ordering constraints: [p(s(s(x)))] = [1 0] x + [3] [1 0] [3] >= [1 0] x + [3] [1 0] [2] = [s(p(s(x)))] [p(s(0()))] = [1] [1] > [0] [0] = [0()] [fac^#(s(x))] = [4 0] x + [9] [0 0] [0] > [4 0] x + [8] [0 0] [0] = [c_1(fac^#(p(s(x))), p^#(s(x)))] 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: { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) } Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } 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. { fac^#(s(x)) -> c_1(fac^#(p(s(x))), p^#(s(x))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) 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(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { p^#(s(s(x))) -> c_2(p^#(s(x))) } Weak DPs: { fac^#(s(x)) -> fac^#(p(s(x))) , fac^#(s(x)) -> p^#(s(x)) } Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } 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: p^#(s(s(x))) -> c_2(p^#(s(x))) } Trs: { p(s(0())) -> 0() } Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(s) = {1}, safe(p) = {}, safe(0) = {}, safe(fac^#) = {}, safe(p^#) = {}, safe(c_2) = {} and precedence fac^# ~ p^# . Following symbols are considered recursive: {p^#} The recursion depth is 1. Further, following argument filtering is employed: pi(s) = [1], pi(p) = 1, pi(0) = [], pi(fac^#) = [1], pi(p^#) = [1], pi(c_2) = [1] Usable defined function symbols are a subset of: {p, fac^#, p^#} For your convenience, here are the satisfied ordering constraints: pi(fac^#(s(x))) = fac^#(s(; x);) >= fac^#(s(; x);) = pi(fac^#(p(s(x)))) pi(fac^#(s(x))) = fac^#(s(; x);) >= p^#(s(; x);) = pi(p^#(s(x))) pi(p^#(s(s(x)))) = p^#(s(; s(; x));) > c_2(p^#(s(; x););) = pi(c_2(p^#(s(x)))) pi(p(s(s(x)))) = s(; s(; x)) >= s(; s(; x)) = pi(s(p(s(x)))) pi(p(s(0()))) = s(; 0()) > 0() = pi(0()) 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: { fac^#(s(x)) -> fac^#(p(s(x))) , fac^#(s(x)) -> p^#(s(x)) , p^#(s(s(x))) -> c_2(p^#(s(x))) } Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } 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. { fac^#(s(x)) -> fac^#(p(s(x))) , fac^#(s(x)) -> p^#(s(x)) , p^#(s(s(x))) -> c_2(p^#(s(x))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { p(s(s(x))) -> s(p(s(x))) , p(s(0())) -> 0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) 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(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))