YES(O(1),O(n^2)) 36.90/9.42 YES(O(1),O(n^2)) 36.90/9.42 36.90/9.42 We are left with following problem, upon which TcT provides the 36.90/9.42 certificate YES(O(1),O(n^2)). 36.90/9.42 36.90/9.42 Strict Trs: 36.90/9.42 { f(x, c(y)) -> f(x, s(f(y, y))) 36.90/9.42 , f(s(x), y) -> f(x, s(c(y))) } 36.90/9.42 Obligation: 36.90/9.42 runtime complexity 36.90/9.42 Answer: 36.90/9.42 YES(O(1),O(n^2)) 36.90/9.42 36.90/9.42 We add the following weak dependency pairs: 36.90/9.42 36.90/9.42 Strict DPs: 36.90/9.42 { f^#(x, c(y)) -> c_1(f^#(x, s(f(y, y)))) 36.90/9.42 , f^#(s(x), y) -> c_2(f^#(x, s(c(y)))) } 36.90/9.42 36.90/9.42 and mark the set of starting terms. 36.90/9.42 36.90/9.42 We are left with following problem, upon which TcT provides the 36.90/9.42 certificate YES(O(1),O(n^2)). 36.90/9.42 36.90/9.42 Strict DPs: 36.90/9.42 { f^#(x, c(y)) -> c_1(f^#(x, s(f(y, y)))) 36.90/9.42 , f^#(s(x), y) -> c_2(f^#(x, s(c(y)))) } 36.90/9.42 Strict Trs: 36.90/9.42 { f(x, c(y)) -> f(x, s(f(y, y))) 36.90/9.42 , f(s(x), y) -> f(x, s(c(y))) } 36.90/9.42 Obligation: 36.90/9.42 runtime complexity 36.90/9.42 Answer: 36.90/9.42 YES(O(1),O(n^2)) 36.90/9.42 36.90/9.42 We use the processor 'matrix interpretation of dimension 2' to 36.90/9.42 orient following rules strictly. 36.90/9.42 36.90/9.42 DPs: 36.90/9.42 { f^#(x, c(y)) -> c_1(f^#(x, s(f(y, y)))) 36.90/9.42 , f^#(s(x), y) -> c_2(f^#(x, s(c(y)))) } 36.90/9.42 Trs: { f(x, c(y)) -> f(x, s(f(y, y))) } 36.90/9.42 36.90/9.42 The induced complexity on above rules (modulo remaining rules) is 36.90/9.42 YES(?,O(n^2)) . These rules are moved into the corresponding weak 36.90/9.42 component(s). 36.90/9.42 36.90/9.42 Sub-proof: 36.90/9.42 ---------- 36.90/9.42 The following argument positions are usable: 36.90/9.42 Uargs(f) = {1, 2}, Uargs(c) = {1}, Uargs(s) = {1}, 36.90/9.42 Uargs(f^#) = {2}, Uargs(c_1) = {1}, Uargs(c_2) = {1} 36.90/9.42 36.90/9.42 TcT has computed the following constructor-based matrix 36.90/9.42 interpretation satisfying not(EDA). 36.90/9.42 36.90/9.42 [f](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 36.90/9.42 [c](x1) = [1 0] x1 + [0] 36.90/9.42 [1 1] [2] 36.90/9.42 36.90/9.42 [s](x1) = [1 0] x1 + [1] 36.90/9.42 [0 0] [0] 36.90/9.42 36.90/9.42 [f^#](x1, x2) = [6 0] x1 + [4 4] x2 + [2] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 36.90/9.42 [c_1](x1) = [1 0] x1 + [1] 36.90/9.42 [0 0] [0] 36.90/9.42 36.90/9.42 [c_2](x1) = [1 0] x1 + [1] 36.90/9.42 [0 0] [0] 36.90/9.42 36.90/9.42 The order satisfies the following ordering constraints: 36.90/9.42 36.90/9.42 [f(x, c(y))] = [1 0] x + [2 1] y + [2] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 > [1 0] x + [2 1] y + [1] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [f(x, s(f(y, y)))] 36.90/9.42 36.90/9.42 [f(s(x), y)] = [1 0] x + [1 1] y + [1] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 >= [1 0] x + [1 0] y + [1] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [f(x, s(c(y)))] 36.90/9.42 36.90/9.42 [f^#(x, c(y))] = [6 0] x + [8 4] y + [10] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 > [6 0] x + [8 4] y + [7] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [c_1(f^#(x, s(f(y, y))))] 36.90/9.42 36.90/9.42 [f^#(s(x), y)] = [6 0] x + [4 4] y + [8] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 > [6 0] x + [4 0] y + [7] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [c_2(f^#(x, s(c(y))))] 36.90/9.42 36.90/9.42 36.90/9.42 We return to the main proof. 36.90/9.42 36.90/9.42 We are left with following problem, upon which TcT provides the 36.90/9.42 certificate YES(O(1),O(n^2)). 36.90/9.42 36.90/9.42 Strict Trs: { f(s(x), y) -> f(x, s(c(y))) } 36.90/9.42 Weak DPs: 36.90/9.42 { f^#(x, c(y)) -> c_1(f^#(x, s(f(y, y)))) 36.90/9.42 , f^#(s(x), y) -> c_2(f^#(x, s(c(y)))) } 36.90/9.42 Weak Trs: { f(x, c(y)) -> f(x, s(f(y, y))) } 36.90/9.42 Obligation: 36.90/9.42 runtime complexity 36.90/9.42 Answer: 36.90/9.42 YES(O(1),O(n^2)) 36.90/9.42 36.90/9.42 We use the processor 'matrix interpretation of dimension 2' to 36.90/9.42 orient following rules strictly. 36.90/9.42 36.90/9.42 Trs: { f(s(x), y) -> f(x, s(c(y))) } 36.90/9.42 36.90/9.42 The induced complexity on above rules (modulo remaining rules) is 36.90/9.42 YES(?,O(n^2)) . These rules are moved into the corresponding weak 36.90/9.42 component(s). 36.90/9.42 36.90/9.42 Sub-proof: 36.90/9.42 ---------- 36.90/9.42 The following argument positions are usable: 36.90/9.42 Uargs(f) = {1, 2}, Uargs(c) = {1}, Uargs(s) = {1}, 36.90/9.42 Uargs(f^#) = {2}, Uargs(c_1) = {1}, Uargs(c_2) = {1} 36.90/9.42 36.90/9.42 TcT has computed the following constructor-based matrix 36.90/9.42 interpretation satisfying not(EDA). 36.90/9.42 36.90/9.42 [f](x1, x2) = [2 0] x1 + [1 3] x2 + [0] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 36.90/9.42 [c](x1) = [1 0] x1 + [0] 36.90/9.42 [1 1] [3] 36.90/9.42 36.90/9.42 [s](x1) = [1 0] x1 + [4] 36.90/9.42 [0 0] [0] 36.90/9.42 36.90/9.42 [f^#](x1, x2) = [2 0] x1 + [1 3] x2 + [0] 36.90/9.42 [0 0] [0 0] [1] 36.90/9.42 36.90/9.42 [c_1](x1) = [1 0] x1 + [3] 36.90/9.42 [0 0] [1] 36.90/9.42 36.90/9.42 [c_2](x1) = [1 4] x1 + [0] 36.90/9.42 [0 0] [1] 36.90/9.42 36.90/9.42 The order satisfies the following ordering constraints: 36.90/9.42 36.90/9.42 [f(x, c(y))] = [2 0] x + [4 3] y + [9] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 > [2 0] x + [3 3] y + [4] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [f(x, s(f(y, y)))] 36.90/9.42 36.90/9.42 [f(s(x), y)] = [2 0] x + [1 3] y + [8] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 > [2 0] x + [1 0] y + [4] 36.90/9.42 [0 0] [0 0] [0] 36.90/9.42 = [f(x, s(c(y)))] 36.90/9.42 36.90/9.42 [f^#(x, c(y))] = [2 0] x + [4 3] y + [9] 36.90/9.42 [0 0] [0 0] [1] 36.90/9.42 > [2 0] x + [3 3] y + [7] 36.90/9.42 [0 0] [0 0] [1] 36.90/9.42 = [c_1(f^#(x, s(f(y, y))))] 36.90/9.42 36.90/9.42 [f^#(s(x), y)] = [2 0] x + [1 3] y + [8] 36.90/9.42 [0 0] [0 0] [1] 36.90/9.42 >= [2 0] x + [1 0] y + [8] 36.90/9.42 [0 0] [0 0] [1] 36.90/9.42 = [c_2(f^#(x, s(c(y))))] 36.90/9.42 36.90/9.42 36.90/9.42 We return to the main proof. 36.90/9.42 36.90/9.42 We are left with following problem, upon which TcT provides the 36.90/9.42 certificate YES(O(1),O(1)). 36.90/9.42 36.90/9.42 Weak DPs: 36.90/9.42 { f^#(x, c(y)) -> c_1(f^#(x, s(f(y, y)))) 36.90/9.42 , f^#(s(x), y) -> c_2(f^#(x, s(c(y)))) } 36.90/9.42 Weak Trs: 36.90/9.42 { f(x, c(y)) -> f(x, s(f(y, y))) 36.90/9.42 , f(s(x), y) -> f(x, s(c(y))) } 36.90/9.42 Obligation: 36.90/9.42 runtime complexity 36.90/9.42 Answer: 36.90/9.42 YES(O(1),O(1)) 36.90/9.42 36.90/9.42 Empty rules are trivially bounded 36.90/9.42 36.90/9.42 Hurray, we answered YES(O(1),O(n^2)) 36.90/9.45 EOF