YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { p(X) -> n__p(X) , p(0()) -> 0() , p(s(X)) -> X , 0() -> n__0() , s(X) -> n__s(X) , leq(0(), Y) -> true() , leq(s(X), 0()) -> false() , leq(s(X), s(Y)) -> leq(X, Y) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Arguments of following rules are not normal-forms: { p(0()) -> 0() , p(s(X)) -> X , leq(0(), Y) -> true() , leq(s(X), 0()) -> false() , leq(s(X), s(Y)) -> leq(X, Y) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following dependency tuples: Strict DPs: { p^#(X) -> c_1() , 0^#() -> c_2() , s^#(X) -> c_3() , if^#(true(), X, Y) -> c_4(activate^#(X)) , if^#(false(), X, Y) -> c_5(activate^#(Y)) , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) , diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , diff^#(X1, X2) -> c_12() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { p^#(X) -> c_1() , 0^#() -> c_2() , s^#(X) -> c_3() , if^#(true(), X, Y) -> c_4(activate^#(X)) , if^#(false(), X, Y) -> c_5(activate^#(Y)) , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) , diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , diff^#(X1, X2) -> c_12() } Weak Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1,2,3,6,11,12} by applications of Pre({1,2,3,6,11,12}) = {4,5,7,8,9,10}. Here rules are labeled as follows: DPs: { 1: p^#(X) -> c_1() , 2: 0^#() -> c_2() , 3: s^#(X) -> c_3() , 4: if^#(true(), X, Y) -> c_4(activate^#(X)) , 5: if^#(false(), X, Y) -> c_5(activate^#(Y)) , 6: activate^#(X) -> c_6() , 7: activate^#(n__0()) -> c_7(0^#()) , 8: activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , 9: activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 10: activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) , 11: diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , 12: diff^#(X1, X2) -> c_12() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { if^#(true(), X, Y) -> c_4(activate^#(X)) , if^#(false(), X, Y) -> c_5(activate^#(Y)) , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) } Weak DPs: { p^#(X) -> c_1() , 0^#() -> c_2() , s^#(X) -> c_3() , activate^#(X) -> c_6() , diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , diff^#(X1, X2) -> c_12() } Weak Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {1,2,4,5,6}. Here rules are labeled as follows: DPs: { 1: if^#(true(), X, Y) -> c_4(activate^#(X)) , 2: if^#(false(), X, Y) -> c_5(activate^#(Y)) , 3: activate^#(n__0()) -> c_7(0^#()) , 4: activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , 5: activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 6: activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) , 7: p^#(X) -> c_1() , 8: 0^#() -> c_2() , 9: s^#(X) -> c_3() , 10: activate^#(X) -> c_6() , 11: diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , 12: diff^#(X1, X2) -> c_12() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { if^#(true(), X, Y) -> c_4(activate^#(X)) , if^#(false(), X, Y) -> c_5(activate^#(Y)) , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) } Weak DPs: { p^#(X) -> c_1() , 0^#() -> c_2() , s^#(X) -> c_3() , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , diff^#(X1, X2) -> c_12() } Weak Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } 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. { p^#(X) -> c_1() , 0^#() -> c_2() , s^#(X) -> c_3() , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , diff^#(X, Y) -> c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))) , diff^#(X1, X2) -> c_12() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { if^#(true(), X, Y) -> c_4(activate^#(X)) , if^#(false(), X, Y) -> c_5(activate^#(Y)) , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) } Weak Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } 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: { activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_9(diff^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { if^#(true(), X, Y) -> c_1(activate^#(X)) , if^#(false(), X, Y) -> c_2(activate^#(Y)) , activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } Weak Trs: { p(X) -> n__p(X) , 0() -> n__0() , s(X) -> n__s(X) , if(true(), X, Y) -> activate(X) , if(false(), X, Y) -> activate(Y) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__s(X)) -> s(activate(X)) , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)) , activate(n__p(X)) -> p(activate(X)) , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))) , diff(X1, X2) -> n__diff(X1, X2) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^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(n^1)). Strict DPs: { if^#(true(), X, Y) -> c_1(activate^#(X)) , if^#(false(), X, Y) -> c_2(activate^#(Y)) , activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Consider the dependency graph 1: if^#(true(), X, Y) -> c_1(activate^#(X)) -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_1 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 2: if^#(false(), X, Y) -> c_2(activate^#(Y)) -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_1 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 3: activate^#(n__s(X)) -> c_3(activate^#(X)) -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_1 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 4: activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) -->_2 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_2 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_1 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_2 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 5: activate^#(n__p(X)) -> c_5(activate^#(X)) -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5 -->_1 activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) :4 -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3 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). { if^#(true(), X, Y) -> c_1(activate^#(X)) , if^#(false(), X, Y) -> c_2(activate^#(Y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: activate^#(n__s(X)) -> c_3(activate^#(X)) , 3: activate^#(n__p(X)) -> c_5(activate^#(X)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [p](x1) = [7] x1 + [0] [0] = [0] [s](x1) = [7] x1 + [0] [leq](x1, x2) = [7] x1 + [7] x2 + [0] [true] = [0] [false] = [0] [if](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [activate](x1) = [7] x1 + [0] [diff](x1, x2) = [7] x1 + [7] x2 + [0] [n__0] = [0] [n__s](x1) = [1] x1 + [4] [n__diff](x1, x2) = [1] x1 + [1] x2 + [0] [n__p](x1) = [1] x1 + [4] [p^#](x1) = [7] x1 + [0] [c_1] = [0] [0^#] = [0] [c_2] = [0] [s^#](x1) = [7] x1 + [0] [c_3] = [0] [if^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_4](x1) = [7] x1 + [0] [activate^#](x1) = [2] x1 + [0] [c_5](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [diff^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1) = [7] x1 + [0] [c_12] = [0] [leq^#](x1, x2) = [7] x1 + [7] x2 + [0] [c] = [0] [c_1](x1) = [7] x1 + [0] [c_2](x1) = [7] x1 + [0] [c_3](x1) = [1] x1 + [1] [c_4](x1, x2) = [1] x1 + [1] x2 + [0] [c_5](x1) = [1] x1 + [7] The following symbols are considered usable {activate^#} The order satisfies the following ordering constraints: [activate^#(n__s(X))] = [2] X + [8] > [2] X + [1] = [c_3(activate^#(X))] [activate^#(n__diff(X1, X2))] = [2] X1 + [2] X2 + [0] >= [2] X1 + [2] X2 + [0] = [c_4(activate^#(X1), activate^#(X2))] [activate^#(n__p(X))] = [2] X + [8] > [2] X + [7] = [c_5(activate^#(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(n^1)). Strict DPs: { activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) } Weak DPs: { activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , 2: activate^#(n__s(X)) -> c_3(activate^#(X)) , 3: activate^#(n__p(X)) -> c_5(activate^#(X)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [p](x1) = [7] x1 + [0] [0] = [0] [s](x1) = [7] x1 + [0] [leq](x1, x2) = [7] x1 + [7] x2 + [0] [true] = [0] [false] = [0] [if](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [activate](x1) = [7] x1 + [0] [diff](x1, x2) = [7] x1 + [7] x2 + [0] [n__0] = [0] [n__s](x1) = [1] x1 + [4] [n__diff](x1, x2) = [1] x1 + [1] x2 + [4] [n__p](x1) = [1] x1 + [4] [p^#](x1) = [7] x1 + [0] [c_1] = [0] [0^#] = [0] [c_2] = [0] [s^#](x1) = [7] x1 + [0] [c_3] = [0] [if^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_4](x1) = [7] x1 + [0] [activate^#](x1) = [2] x1 + [0] [c_5](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [diff^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1) = [7] x1 + [0] [c_12] = [0] [leq^#](x1, x2) = [7] x1 + [7] x2 + [0] [c] = [0] [c_1](x1) = [7] x1 + [0] [c_2](x1) = [7] x1 + [0] [c_3](x1) = [1] x1 + [1] [c_4](x1, x2) = [1] x1 + [1] x2 + [5] [c_5](x1) = [1] x1 + [1] The following symbols are considered usable {activate^#} The order satisfies the following ordering constraints: [activate^#(n__s(X))] = [2] X + [8] > [2] X + [1] = [c_3(activate^#(X))] [activate^#(n__diff(X1, X2))] = [2] X1 + [2] X2 + [8] > [2] X1 + [2] X2 + [5] = [c_4(activate^#(X1), activate^#(X2))] [activate^#(n__p(X))] = [2] X + [8] > [2] X + [1] = [c_5(activate^#(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: { activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } 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. { activate^#(n__s(X)) -> c_3(activate^#(X)) , activate^#(n__diff(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , activate^#(n__p(X)) -> c_5(activate^#(X)) } 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^1))