YES(O(1),O(n^1)) 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict Trs: 141.32/63.01 { -(x, 0()) -> x 141.32/63.01 , -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()) 141.32/63.01 , -(0(), y) -> 0() 141.32/63.01 , p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 We add the following weak dependency pairs: 141.32/63.01 141.32/63.01 Strict DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , -^#(0(), y) -> c_3() 141.32/63.01 , p^#(0()) -> c_4() 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 141.32/63.01 and mark the set of starting terms. 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , -^#(0(), y) -> c_3() 141.32/63.01 , p^#(0()) -> c_4() 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 Strict Trs: 141.32/63.01 { -(x, 0()) -> x 141.32/63.01 , -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()) 141.32/63.01 , -(0(), y) -> 0() 141.32/63.01 , p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 We replace rewrite rules by usable rules: 141.32/63.01 141.32/63.01 Strict Usable Rules: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , -^#(0(), y) -> c_3() 141.32/63.01 , p^#(0()) -> c_4() 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 Strict Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 The weightgap principle applies (using the following constant 141.32/63.01 growth matrix-interpretation) 141.32/63.01 141.32/63.01 The following argument positions are usable: 141.32/63.01 Uargs(-^#) = {2}, Uargs(c_2) = {3} 141.32/63.01 141.32/63.01 TcT has computed the following constructor-restricted matrix 141.32/63.01 interpretation. 141.32/63.01 141.32/63.01 [0] = [0] 141.32/63.01 [2] 141.32/63.01 141.32/63.01 [s](x1) = [1 2] x1 + [1] 141.32/63.01 [0 0] [0] 141.32/63.01 141.32/63.01 [p](x1) = [1 2] x1 + [0] 141.32/63.01 [2 2] [0] 141.32/63.01 141.32/63.01 [-^#](x1, x2) = [1 1] x1 + [2 0] x2 + [0] 141.32/63.01 [2 1] [0 0] [0] 141.32/63.01 141.32/63.01 [c_1](x1) = [1 1] x1 + [1] 141.32/63.01 [1 1] [0] 141.32/63.01 141.32/63.01 [c_2](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [2] 141.32/63.01 [1 1] [2 2] [0 1] [2] 141.32/63.01 141.32/63.01 [c_3] = [1] 141.32/63.01 [1] 141.32/63.01 141.32/63.01 [p^#](x1) = [1 1] x1 + [1] 141.32/63.01 [2 1] [2] 141.32/63.01 141.32/63.01 [c_4] = [2] 141.32/63.01 [0] 141.32/63.01 141.32/63.01 [c_5](x1) = [1 1] x1 + [1] 141.32/63.01 [1 0] [0] 141.32/63.01 141.32/63.01 The order satisfies the following ordering constraints: 141.32/63.01 141.32/63.01 [p(0())] = [4] 141.32/63.01 [4] 141.32/63.01 > [0] 141.32/63.01 [2] 141.32/63.01 = [0()] 141.32/63.01 141.32/63.01 [p(s(x))] = [1 2] x + [1] 141.32/63.01 [2 4] [2] 141.32/63.01 > [1 0] x + [0] 141.32/63.01 [0 1] [0] 141.32/63.01 = [x] 141.32/63.01 141.32/63.01 [-^#(x, 0())] = [1 1] x + [0] 141.32/63.01 [2 1] [0] 141.32/63.01 ? [1 1] x + [1] 141.32/63.01 [1 1] [0] 141.32/63.01 = [c_1(x)] 141.32/63.01 141.32/63.01 [-^#(x, s(y))] = [2 4] y + [1 1] x + [2] 141.32/63.01 [0 0] [2 1] [0] 141.32/63.01 ? [2 4] y + [1 1] x + [4] 141.32/63.01 [2 2] [3 2] [2] 141.32/63.01 = [c_2(x, y, -^#(x, p(s(y))))] 141.32/63.01 141.32/63.01 [-^#(0(), y)] = [2 0] y + [2] 141.32/63.01 [0 0] [2] 141.32/63.01 > [1] 141.32/63.01 [1] 141.32/63.01 = [c_3()] 141.32/63.01 141.32/63.01 [p^#(0())] = [3] 141.32/63.01 [4] 141.32/63.01 > [2] 141.32/63.01 [0] 141.32/63.01 = [c_4()] 141.32/63.01 141.32/63.01 [p^#(s(x))] = [1 2] x + [2] 141.32/63.01 [2 4] [4] 141.32/63.01 > [1 1] x + [1] 141.32/63.01 [1 0] [0] 141.32/63.01 = [c_5(x)] 141.32/63.01 141.32/63.01 141.32/63.01 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) } 141.32/63.01 Weak DPs: 141.32/63.01 { -^#(0(), y) -> c_3() 141.32/63.01 , p^#(0()) -> c_4() 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 Weak Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 The following weak DPs constitute a sub-graph of the DG that is 141.32/63.01 closed under successors. The DPs are removed. 141.32/63.01 141.32/63.01 { -^#(0(), y) -> c_3() 141.32/63.01 , p^#(0()) -> c_4() } 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) } 141.32/63.01 Weak DPs: { p^#(s(x)) -> c_5(x) } 141.32/63.01 Weak Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 We use the processor 'matrix interpretation of dimension 1' to 141.32/63.01 orient following rules strictly. 141.32/63.01 141.32/63.01 DPs: 141.32/63.01 { 1: -^#(x, 0()) -> c_1(x) 141.32/63.01 , 3: p^#(s(x)) -> c_5(x) } 141.32/63.01 141.32/63.01 Sub-proof: 141.32/63.01 ---------- 141.32/63.01 The following argument positions are usable: 141.32/63.01 Uargs(c_2) = {3} 141.32/63.01 141.32/63.01 TcT has computed the following constructor-based matrix 141.32/63.01 interpretation satisfying not(EDA). 141.32/63.01 141.32/63.01 [0] = [0] 141.32/63.01 141.32/63.01 [s](x1) = [1] x1 + [0] 141.32/63.01 141.32/63.01 [p](x1) = [0] 141.32/63.01 141.32/63.01 [-^#](x1, x2) = [7] x1 + [1] 141.32/63.01 141.32/63.01 [c_1](x1) = [7] x1 + [0] 141.32/63.01 141.32/63.01 [c_2](x1, x2, x3) = [1] x3 + [0] 141.32/63.01 141.32/63.01 [p^#](x1) = [7] x1 + [7] 141.32/63.01 141.32/63.01 [c_5](x1) = [7] x1 + [6] 141.32/63.01 141.32/63.01 The order satisfies the following ordering constraints: 141.32/63.01 141.32/63.01 [p(0())] = [0] 141.32/63.01 >= [0] 141.32/63.01 = [0()] 141.32/63.01 141.32/63.01 [p(s(x))] = [0] 141.32/63.01 ? [1] x + [0] 141.32/63.01 = [x] 141.32/63.01 141.32/63.01 [-^#(x, 0())] = [7] x + [1] 141.32/63.01 > [7] x + [0] 141.32/63.01 = [c_1(x)] 141.32/63.01 141.32/63.01 [-^#(x, s(y))] = [7] x + [1] 141.32/63.01 >= [7] x + [1] 141.32/63.01 = [c_2(x, y, -^#(x, p(s(y))))] 141.32/63.01 141.32/63.01 [p^#(s(x))] = [7] x + [7] 141.32/63.01 > [7] x + [6] 141.32/63.01 = [c_5(x)] 141.32/63.01 141.32/63.01 141.32/63.01 The strictly oriented rules are moved into the weak component. 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(n^1)). 141.32/63.01 141.32/63.01 Strict DPs: { -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) } 141.32/63.01 Weak DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 Weak Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(n^1)) 141.32/63.01 141.32/63.01 We use the processor 'matrix interpretation of dimension 3' to 141.32/63.01 orient following rules strictly. 141.32/63.01 141.32/63.01 DPs: 141.32/63.01 { 1: -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , 3: p^#(s(x)) -> c_5(x) } 141.32/63.01 141.32/63.01 Sub-proof: 141.32/63.01 ---------- 141.32/63.01 The following argument positions are usable: 141.32/63.01 Uargs(c_2) = {3} 141.32/63.01 141.32/63.01 TcT has computed the following constructor-based matrix 141.32/63.01 interpretation satisfying not(EDA) and not(IDA(1)). 141.32/63.01 141.32/63.01 [0] 141.32/63.01 [0] = [0] 141.32/63.01 [0] 141.32/63.01 141.32/63.01 [1 0 0] [2] 141.32/63.01 [s](x1) = [1 0 0] x1 + [0] 141.32/63.01 [0 1 1] [0] 141.32/63.01 141.32/63.01 [0 1 0] [0] 141.32/63.01 [p](x1) = [0 0 1] x1 + [0] 141.32/63.01 [0 0 2] [0] 141.32/63.01 141.32/63.01 [1 0 0] [0] 141.32/63.01 [-^#](x1, x2) = [0 0 0] x2 + [0] 141.32/63.01 [0 0 0] [0] 141.32/63.01 141.32/63.01 [0] 141.32/63.01 [c_1](x1) = [0] 141.32/63.01 [0] 141.32/63.01 141.32/63.01 [1 0 0] [1] 141.32/63.01 [c_2](x1, x2, x3) = [0 0 0] x3 + [0] 141.32/63.01 [0 0 0] [0] 141.32/63.01 141.32/63.01 [7] 141.32/63.01 [p^#](x1) = [7] 141.32/63.01 [7] 141.32/63.01 141.32/63.01 [6] 141.32/63.01 [c_5](x1) = [7] 141.32/63.01 [7] 141.32/63.01 141.32/63.01 The order satisfies the following ordering constraints: 141.32/63.01 141.32/63.01 [p(0())] = [0] 141.32/63.01 [0] 141.32/63.01 [0] 141.32/63.01 >= [0] 141.32/63.01 [0] 141.32/63.01 [0] 141.32/63.01 = [0()] 141.32/63.01 141.32/63.01 [p(s(x))] = [1 0 0] [0] 141.32/63.01 [0 1 1] x + [0] 141.32/63.01 [0 2 2] [0] 141.32/63.01 >= [1 0 0] [0] 141.32/63.01 [0 1 0] x + [0] 141.32/63.01 [0 0 1] [0] 141.32/63.01 = [x] 141.32/63.01 141.32/63.01 [-^#(x, 0())] = [0] 141.32/63.01 [0] 141.32/63.01 [0] 141.32/63.01 >= [0] 141.32/63.01 [0] 141.32/63.01 [0] 141.32/63.01 = [c_1(x)] 141.32/63.01 141.32/63.01 [-^#(x, s(y))] = [1 0 0] [2] 141.32/63.01 [0 0 0] y + [0] 141.32/63.01 [0 0 0] [0] 141.32/63.01 > [1 0 0] [1] 141.32/63.01 [0 0 0] y + [0] 141.32/63.01 [0 0 0] [0] 141.32/63.01 = [c_2(x, y, -^#(x, p(s(y))))] 141.32/63.01 141.32/63.01 [p^#(s(x))] = [7] 141.32/63.01 [7] 141.32/63.01 [7] 141.32/63.01 > [6] 141.32/63.01 [7] 141.32/63.01 [7] 141.32/63.01 = [c_5(x)] 141.32/63.01 141.32/63.01 141.32/63.01 The strictly oriented rules are moved into the weak component. 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(1)). 141.32/63.01 141.32/63.01 Weak DPs: 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 Weak Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(1)) 141.32/63.01 141.32/63.01 The following weak DPs constitute a sub-graph of the DG that is 141.32/63.01 closed under successors. The DPs are removed. 141.32/63.01 141.32/63.01 { -^#(x, 0()) -> c_1(x) 141.32/63.01 , -^#(x, s(y)) -> c_2(x, y, -^#(x, p(s(y)))) 141.32/63.01 , p^#(s(x)) -> c_5(x) } 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(1)). 141.32/63.01 141.32/63.01 Weak Trs: 141.32/63.01 { p(0()) -> 0() 141.32/63.01 , p(s(x)) -> x } 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(1)) 141.32/63.01 141.32/63.01 No rule is usable, rules are removed from the input problem. 141.32/63.01 141.32/63.01 We are left with following problem, upon which TcT provides the 141.32/63.01 certificate YES(O(1),O(1)). 141.32/63.01 141.32/63.01 Rules: Empty 141.32/63.01 Obligation: 141.32/63.01 runtime complexity 141.32/63.01 Answer: 141.32/63.01 YES(O(1),O(1)) 141.32/63.01 141.32/63.01 Empty rules are trivially bounded 141.32/63.01 141.32/63.01 Hurray, we answered YES(O(1),O(n^1)) 141.32/63.04 EOF