YES(O(1),O(n^2)) 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 We are left with following problem, upon which TcT provides the 428.70/148.03 certificate YES(O(1),O(n^2)). 428.70/148.03 428.70/148.03 Strict Trs: 428.70/148.03 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.03 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.03 , activate(X) -> X 428.70/148.03 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.03 , plus(N, 0()) -> N 428.70/148.03 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.03 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.03 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.03 , x(N, 0()) -> 0() } 428.70/148.03 Obligation: 428.70/148.03 innermost runtime complexity 428.70/148.03 Answer: 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 We add the following dependency tuples: 428.70/148.03 428.70/148.03 Strict DPs: 428.70/148.03 { U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , activate^#(X) -> c_3() 428.70/148.03 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 428.70/148.03 , plus^#(N, 0()) -> c_5() 428.70/148.03 , U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 428.70/148.03 , x^#(N, 0()) -> c_9() } 428.70/148.03 428.70/148.03 and mark the set of starting terms. 428.70/148.03 428.70/148.03 We are left with following problem, upon which TcT provides the 428.70/148.03 certificate YES(O(1),O(n^2)). 428.70/148.03 428.70/148.03 Strict DPs: 428.70/148.03 { U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , activate^#(X) -> c_3() 428.70/148.03 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 428.70/148.03 , plus^#(N, 0()) -> c_5() 428.70/148.03 , U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 428.70/148.03 , x^#(N, 0()) -> c_9() } 428.70/148.03 Weak Trs: 428.70/148.03 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.03 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.03 , activate(X) -> X 428.70/148.03 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.03 , plus(N, 0()) -> N 428.70/148.03 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.03 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.03 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.03 , x(N, 0()) -> 0() } 428.70/148.03 Obligation: 428.70/148.03 innermost runtime complexity 428.70/148.03 Answer: 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 We estimate the number of application of {3,5,9} by applications of 428.70/148.03 Pre({3,5,9}) = {1,2,6,7}. Here rules are labeled as follows: 428.70/148.03 428.70/148.03 DPs: 428.70/148.03 { 1: U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , 2: U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , 3: activate^#(X) -> c_3() 428.70/148.03 , 4: plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 428.70/148.03 , 5: plus^#(N, 0()) -> c_5() 428.70/148.03 , 6: U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , 7: U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , 8: x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 428.70/148.03 , 9: x^#(N, 0()) -> c_9() } 428.70/148.03 428.70/148.03 We are left with following problem, upon which TcT provides the 428.70/148.03 certificate YES(O(1),O(n^2)). 428.70/148.03 428.70/148.03 Strict DPs: 428.70/148.03 { U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 428.70/148.03 , U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) } 428.70/148.03 Weak DPs: 428.70/148.03 { activate^#(X) -> c_3() 428.70/148.03 , plus^#(N, 0()) -> c_5() 428.70/148.03 , x^#(N, 0()) -> c_9() } 428.70/148.03 Weak Trs: 428.70/148.03 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.03 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.03 , activate(X) -> X 428.70/148.03 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.03 , plus(N, 0()) -> N 428.70/148.03 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.03 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.03 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.03 , x(N, 0()) -> 0() } 428.70/148.03 Obligation: 428.70/148.03 innermost runtime complexity 428.70/148.03 Answer: 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 The following weak DPs constitute a sub-graph of the DG that is 428.70/148.03 closed under successors. The DPs are removed. 428.70/148.03 428.70/148.03 { activate^#(X) -> c_3() 428.70/148.03 , plus^#(N, 0()) -> c_5() 428.70/148.03 , x^#(N, 0()) -> c_9() } 428.70/148.03 428.70/148.03 We are left with following problem, upon which TcT provides the 428.70/148.03 certificate YES(O(1),O(n^2)). 428.70/148.03 428.70/148.03 Strict DPs: 428.70/148.03 { U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 428.70/148.03 , U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) } 428.70/148.03 Weak Trs: 428.70/148.03 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.03 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.03 , activate(X) -> X 428.70/148.03 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.03 , plus(N, 0()) -> N 428.70/148.03 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.03 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.03 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.03 , x(N, 0()) -> 0() } 428.70/148.03 Obligation: 428.70/148.03 innermost runtime complexity 428.70/148.03 Answer: 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 Due to missing edges in the dependency-graph, the right-hand sides 428.70/148.03 of following rules could be simplified: 428.70/148.03 428.70/148.03 { U11^#(tt(), M, N) -> 428.70/148.03 c_1(U12^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U12^#(tt(), M, N) -> 428.70/148.03 c_2(plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) 428.70/148.03 , U21^#(tt(), M, N) -> 428.70/148.03 c_6(U22^#(tt(), activate(M), activate(N)), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_7(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M)), 428.70/148.03 activate^#(N), 428.70/148.03 activate^#(M), 428.70/148.03 activate^#(N)) } 428.70/148.03 428.70/148.03 We are left with following problem, upon which TcT provides the 428.70/148.03 certificate YES(O(1),O(n^2)). 428.70/148.03 428.70/148.03 Strict DPs: 428.70/148.03 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.03 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.03 , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) 428.70/148.03 , U21^#(tt(), M, N) -> c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M))) 428.70/148.03 , x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.03 Weak Trs: 428.70/148.03 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.03 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.03 , activate(X) -> X 428.70/148.03 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.03 , plus(N, 0()) -> N 428.70/148.03 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.03 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.03 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.03 , x(N, 0()) -> 0() } 428.70/148.03 Obligation: 428.70/148.03 innermost runtime complexity 428.70/148.03 Answer: 428.70/148.03 YES(O(1),O(n^2)) 428.70/148.03 428.70/148.03 We decompose the input problem according to the dependency graph 428.70/148.03 into the upper component 428.70/148.03 428.70/148.03 { U21^#(tt(), M, N) -> c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.03 , U22^#(tt(), M, N) -> 428.70/148.03 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.03 x^#(activate(N), activate(M))) 428.70/148.04 , x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.04 428.70/148.04 and lower component 428.70/148.04 428.70/148.04 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.04 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.04 , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) } 428.70/148.04 428.70/148.04 Further, following extension rules are added to the lower 428.70/148.04 component. 428.70/148.04 428.70/148.04 { U21^#(tt(), M, N) -> U22^#(tt(), activate(M), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 plus^#(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> x^#(activate(N), activate(M)) 428.70/148.04 , x^#(N, s(M)) -> U21^#(tt(), M, N) } 428.70/148.04 428.70/148.04 TcT solves the upper component with certificate YES(O(1),O(n^1)). 428.70/148.04 428.70/148.04 Sub-proof: 428.70/148.04 ---------- 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(n^1)). 428.70/148.04 428.70/148.04 Strict DPs: 428.70/148.04 { U21^#(tt(), M, N) -> c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.04 x^#(activate(N), activate(M))) 428.70/148.04 , x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(n^1)) 428.70/148.04 428.70/148.04 We use the processor 'matrix interpretation of dimension 1' to 428.70/148.04 orient following rules strictly. 428.70/148.04 428.70/148.04 DPs: 428.70/148.04 { 1: U21^#(tt(), M, N) -> 428.70/148.04 c_4(U22^#(tt(), activate(M), activate(N))) } 428.70/148.04 428.70/148.04 Sub-proof: 428.70/148.04 ---------- 428.70/148.04 The following argument positions are usable: 428.70/148.04 Uargs(c_4) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1} 428.70/148.04 428.70/148.04 TcT has computed the following constructor-based matrix 428.70/148.04 interpretation satisfying not(EDA). 428.70/148.04 428.70/148.04 [U11](x1, x2, x3) = [7] x2 + [7] x3 + [0] 428.70/148.04 428.70/148.04 [tt] = [1] 428.70/148.04 428.70/148.04 [U12](x1, x2, x3) = [0] 428.70/148.04 428.70/148.04 [activate](x1) = [1] x1 + [0] 428.70/148.04 428.70/148.04 [s](x1) = [1] x1 + [1] 428.70/148.04 428.70/148.04 [plus](x1, x2) = [0] 428.70/148.04 428.70/148.04 [U21](x1, x2, x3) = [7] x2 + [7] x3 + [0] 428.70/148.04 428.70/148.04 [U22](x1, x2, x3) = [0] 428.70/148.04 428.70/148.04 [x](x1, x2) = [0] 428.70/148.04 428.70/148.04 [0] = [0] 428.70/148.04 428.70/148.04 [plus^#](x1, x2) = [0] 428.70/148.04 428.70/148.04 [U21^#](x1, x2, x3) = [2] x1 + [4] x2 + [2] 428.70/148.04 428.70/148.04 [U22^#](x1, x2, x3) = [4] x2 + [0] 428.70/148.04 428.70/148.04 [x^#](x1, x2) = [4] x2 + [0] 428.70/148.04 428.70/148.04 [c_4](x1) = [1] x1 + [1] 428.70/148.04 428.70/148.04 [c_5](x1, x2) = [4] x1 + [1] x2 + [0] 428.70/148.04 428.70/148.04 [c_6](x1) = [1] x1 + [0] 428.70/148.04 428.70/148.04 The order satisfies the following ordering constraints: 428.70/148.04 428.70/148.04 [U11(tt(), M, N)] = [7] M + [7] N + [0] 428.70/148.04 >= [0] 428.70/148.04 = [U12(tt(), activate(M), activate(N))] 428.70/148.04 428.70/148.04 [U12(tt(), M, N)] = [0] 428.70/148.04 ? [1] 428.70/148.04 = [s(plus(activate(N), activate(M)))] 428.70/148.04 428.70/148.04 [activate(X)] = [1] X + [0] 428.70/148.04 >= [1] X + [0] 428.70/148.04 = [X] 428.70/148.04 428.70/148.04 [plus(N, s(M))] = [0] 428.70/148.04 ? [7] M + [7] N + [0] 428.70/148.04 = [U11(tt(), M, N)] 428.70/148.04 428.70/148.04 [plus(N, 0())] = [0] 428.70/148.04 ? [1] N + [0] 428.70/148.04 = [N] 428.70/148.04 428.70/148.04 [U21(tt(), M, N)] = [7] M + [7] N + [0] 428.70/148.04 >= [0] 428.70/148.04 = [U22(tt(), activate(M), activate(N))] 428.70/148.04 428.70/148.04 [U22(tt(), M, N)] = [0] 428.70/148.04 >= [0] 428.70/148.04 = [plus(x(activate(N), activate(M)), activate(N))] 428.70/148.04 428.70/148.04 [x(N, s(M))] = [0] 428.70/148.04 ? [7] M + [7] N + [0] 428.70/148.04 = [U21(tt(), M, N)] 428.70/148.04 428.70/148.04 [x(N, 0())] = [0] 428.70/148.04 >= [0] 428.70/148.04 = [0()] 428.70/148.04 428.70/148.04 [U21^#(tt(), M, N)] = [4] M + [4] 428.70/148.04 > [4] M + [1] 428.70/148.04 = [c_4(U22^#(tt(), activate(M), activate(N)))] 428.70/148.04 428.70/148.04 [U22^#(tt(), M, N)] = [4] M + [0] 428.70/148.04 >= [4] M + [0] 428.70/148.04 = [c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.04 x^#(activate(N), activate(M)))] 428.70/148.04 428.70/148.04 [x^#(N, s(M))] = [4] M + [4] 428.70/148.04 >= [4] M + [4] 428.70/148.04 = [c_6(U21^#(tt(), M, N))] 428.70/148.04 428.70/148.04 428.70/148.04 We return to the main proof. Consider the set of all dependency 428.70/148.04 pairs 428.70/148.04 428.70/148.04 : 428.70/148.04 { 1: U21^#(tt(), M, N) -> 428.70/148.04 c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.04 , 2: U22^#(tt(), M, N) -> 428.70/148.04 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.04 x^#(activate(N), activate(M))) 428.70/148.04 , 3: x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.04 428.70/148.04 Processor 'matrix interpretation of dimension 1' induces the 428.70/148.04 complexity certificate YES(?,O(n^1)) on application of dependency 428.70/148.04 pairs {1}. These cover all (indirect) predecessors of dependency 428.70/148.04 pairs {1,2,3}, their number of application is equally bounded. The 428.70/148.04 dependency pairs are shifted into the weak component. 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Weak DPs: 428.70/148.04 { U21^#(tt(), M, N) -> c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.04 x^#(activate(N), activate(M))) 428.70/148.04 , x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 The following weak DPs constitute a sub-graph of the DG that is 428.70/148.04 closed under successors. The DPs are removed. 428.70/148.04 428.70/148.04 { U21^#(tt(), M, N) -> c_4(U22^#(tt(), activate(M), activate(N))) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 c_5(plus^#(x(activate(N), activate(M)), activate(N)), 428.70/148.04 x^#(activate(N), activate(M))) 428.70/148.04 , x^#(N, s(M)) -> c_6(U21^#(tt(), M, N)) } 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 No rule is usable, rules are removed from the input problem. 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Rules: Empty 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 Empty rules are trivially bounded 428.70/148.04 428.70/148.04 We return to the main proof. 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(n^1)). 428.70/148.04 428.70/148.04 Strict DPs: 428.70/148.04 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.04 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.04 , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) } 428.70/148.04 Weak DPs: 428.70/148.04 { U21^#(tt(), M, N) -> U22^#(tt(), activate(M), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 plus^#(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> x^#(activate(N), activate(M)) 428.70/148.04 , x^#(N, s(M)) -> U21^#(tt(), M, N) } 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(n^1)) 428.70/148.04 428.70/148.04 We use the processor 'matrix interpretation of dimension 1' to 428.70/148.04 orient following rules strictly. 428.70/148.04 428.70/148.04 DPs: 428.70/148.04 { 3: plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) } 428.70/148.04 428.70/148.04 Sub-proof: 428.70/148.04 ---------- 428.70/148.04 The following argument positions are usable: 428.70/148.04 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1} 428.70/148.04 428.70/148.04 TcT has computed the following constructor-based matrix 428.70/148.04 interpretation satisfying not(EDA). 428.70/148.04 428.70/148.04 [U11](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 428.70/148.04 428.70/148.04 [tt] = [0] 428.70/148.04 428.70/148.04 [U12](x1, x2, x3) = [7] x1 + [0] 428.70/148.04 428.70/148.04 [activate](x1) = [1] x1 + [0] 428.70/148.04 428.70/148.04 [s](x1) = [1] x1 + [1] 428.70/148.04 428.70/148.04 [plus](x1, x2) = [0] 428.70/148.04 428.70/148.04 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 428.70/148.04 428.70/148.04 [U22](x1, x2, x3) = [7] x1 + [0] 428.70/148.04 428.70/148.04 [x](x1, x2) = [0] 428.70/148.04 428.70/148.04 [0] = [0] 428.70/148.04 428.70/148.04 [U11^#](x1, x2, x3) = [2] x2 + [0] 428.70/148.04 428.70/148.04 [U12^#](x1, x2, x3) = [2] x2 + [0] 428.70/148.04 428.70/148.04 [plus^#](x1, x2) = [2] x2 + [0] 428.70/148.04 428.70/148.04 [U21^#](x1, x2, x3) = [7] x1 + [2] x3 + [0] 428.70/148.04 428.70/148.04 [U22^#](x1, x2, x3) = [7] x1 + [2] x3 + [0] 428.70/148.04 428.70/148.04 [x^#](x1, x2) = [2] x1 + [0] 428.70/148.04 428.70/148.04 [c_1](x1) = [1] x1 + [0] 428.70/148.04 428.70/148.04 [c_2](x1) = [1] x1 + [0] 428.70/148.04 428.70/148.04 [c_3](x1) = [1] x1 + [1] 428.70/148.04 428.70/148.04 The order satisfies the following ordering constraints: 428.70/148.04 428.70/148.04 [U11(tt(), M, N)] = [7] M + [7] N + [0] 428.70/148.04 >= [0] 428.70/148.04 = [U12(tt(), activate(M), activate(N))] 428.70/148.04 428.70/148.04 [U12(tt(), M, N)] = [0] 428.70/148.04 ? [1] 428.70/148.04 = [s(plus(activate(N), activate(M)))] 428.70/148.04 428.70/148.04 [activate(X)] = [1] X + [0] 428.70/148.04 >= [1] X + [0] 428.70/148.04 = [X] 428.70/148.04 428.70/148.04 [plus(N, s(M))] = [0] 428.70/148.04 ? [7] M + [7] N + [0] 428.70/148.04 = [U11(tt(), M, N)] 428.70/148.04 428.70/148.04 [plus(N, 0())] = [0] 428.70/148.04 ? [1] N + [0] 428.70/148.04 = [N] 428.70/148.04 428.70/148.04 [U21(tt(), M, N)] = [7] M + [7] N + [0] 428.70/148.04 >= [0] 428.70/148.04 = [U22(tt(), activate(M), activate(N))] 428.70/148.04 428.70/148.04 [U22(tt(), M, N)] = [0] 428.70/148.04 >= [0] 428.70/148.04 = [plus(x(activate(N), activate(M)), activate(N))] 428.70/148.04 428.70/148.04 [x(N, s(M))] = [0] 428.70/148.04 ? [7] M + [7] N + [0] 428.70/148.04 = [U21(tt(), M, N)] 428.70/148.04 428.70/148.04 [x(N, 0())] = [0] 428.70/148.04 >= [0] 428.70/148.04 = [0()] 428.70/148.04 428.70/148.04 [U11^#(tt(), M, N)] = [2] M + [0] 428.70/148.04 >= [2] M + [0] 428.70/148.04 = [c_1(U12^#(tt(), activate(M), activate(N)))] 428.70/148.04 428.70/148.04 [U12^#(tt(), M, N)] = [2] M + [0] 428.70/148.04 >= [2] M + [0] 428.70/148.04 = [c_2(plus^#(activate(N), activate(M)))] 428.70/148.04 428.70/148.04 [plus^#(N, s(M))] = [2] M + [2] 428.70/148.04 > [2] M + [1] 428.70/148.04 = [c_3(U11^#(tt(), M, N))] 428.70/148.04 428.70/148.04 [U21^#(tt(), M, N)] = [2] N + [0] 428.70/148.04 >= [2] N + [0] 428.70/148.04 = [U22^#(tt(), activate(M), activate(N))] 428.70/148.04 428.70/148.04 [U22^#(tt(), M, N)] = [2] N + [0] 428.70/148.04 >= [2] N + [0] 428.70/148.04 = [plus^#(x(activate(N), activate(M)), activate(N))] 428.70/148.04 428.70/148.04 [U22^#(tt(), M, N)] = [2] N + [0] 428.70/148.04 >= [2] N + [0] 428.70/148.04 = [x^#(activate(N), activate(M))] 428.70/148.04 428.70/148.04 [x^#(N, s(M))] = [2] N + [0] 428.70/148.04 >= [2] N + [0] 428.70/148.04 = [U21^#(tt(), M, N)] 428.70/148.04 428.70/148.04 428.70/148.04 We return to the main proof. Consider the set of all dependency 428.70/148.04 pairs 428.70/148.04 428.70/148.04 : 428.70/148.04 { 1: U11^#(tt(), M, N) -> 428.70/148.04 c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.04 , 2: U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.04 , 3: plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) 428.70/148.04 , 4: U21^#(tt(), M, N) -> U22^#(tt(), activate(M), activate(N)) 428.70/148.04 , 5: U22^#(tt(), M, N) -> 428.70/148.04 plus^#(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , 6: U22^#(tt(), M, N) -> x^#(activate(N), activate(M)) 428.70/148.04 , 7: x^#(N, s(M)) -> U21^#(tt(), M, N) } 428.70/148.04 428.70/148.04 Processor 'matrix interpretation of dimension 1' induces the 428.70/148.04 complexity certificate YES(?,O(n^1)) on application of dependency 428.70/148.04 pairs {3}. These cover all (indirect) predecessors of dependency 428.70/148.04 pairs {1,2,3}, their number of application is equally bounded. The 428.70/148.04 dependency pairs are shifted into the weak component. 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Weak DPs: 428.70/148.04 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.04 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.04 , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) 428.70/148.04 , U21^#(tt(), M, N) -> U22^#(tt(), activate(M), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 plus^#(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> x^#(activate(N), activate(M)) 428.70/148.04 , x^#(N, s(M)) -> U21^#(tt(), M, N) } 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 The following weak DPs constitute a sub-graph of the DG that is 428.70/148.04 closed under successors. The DPs are removed. 428.70/148.04 428.70/148.04 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 428.70/148.04 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 428.70/148.04 , plus^#(N, s(M)) -> c_3(U11^#(tt(), M, N)) 428.70/148.04 , U21^#(tt(), M, N) -> U22^#(tt(), activate(M), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> 428.70/148.04 plus^#(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , U22^#(tt(), M, N) -> x^#(activate(N), activate(M)) 428.70/148.04 , x^#(N, s(M)) -> U21^#(tt(), M, N) } 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Weak Trs: 428.70/148.04 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 428.70/148.04 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 428.70/148.04 , activate(X) -> X 428.70/148.04 , plus(N, s(M)) -> U11(tt(), M, N) 428.70/148.04 , plus(N, 0()) -> N 428.70/148.04 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 428.70/148.04 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 428.70/148.04 , x(N, s(M)) -> U21(tt(), M, N) 428.70/148.04 , x(N, 0()) -> 0() } 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 No rule is usable, rules are removed from the input problem. 428.70/148.04 428.70/148.04 We are left with following problem, upon which TcT provides the 428.70/148.04 certificate YES(O(1),O(1)). 428.70/148.04 428.70/148.04 Rules: Empty 428.70/148.04 Obligation: 428.70/148.04 innermost runtime complexity 428.70/148.04 Answer: 428.70/148.04 YES(O(1),O(1)) 428.70/148.04 428.70/148.04 Empty rules are trivially bounded 428.70/148.04 428.70/148.04 Hurray, we answered YES(O(1),O(n^2)) 428.96/148.21 EOF