YES(O(1),O(n^2)) 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y 26.82/7.71 , div(x, y) -> quot(x, y, y) 26.82/7.71 , div(0(), y) -> 0() 26.82/7.71 , div(div(x, y), z) -> div(x, times(y, z)) 26.82/7.71 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 26.82/7.71 , quot(0(), s(y), z) -> 0() 26.82/7.71 , quot(s(x), s(y), z) -> quot(x, y, z) } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 Arguments of following rules are not normal-forms: 26.82/7.71 26.82/7.71 { div(div(x, y), z) -> div(x, times(y, z)) } 26.82/7.71 26.82/7.71 All above mentioned rules can be savely removed. 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y 26.82/7.71 , div(x, y) -> quot(x, y, y) 26.82/7.71 , div(0(), y) -> 0() 26.82/7.71 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 26.82/7.71 , quot(0(), s(y), z) -> 0() 26.82/7.71 , quot(s(x), s(y), z) -> quot(x, y, z) } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We add the following dependency tuples: 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(x, 0()) -> c_1() 26.82/7.71 , plus^#(0(), y) -> c_2() 26.82/7.71 , plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(0(), y) -> c_4() 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , times^#(s(0()), y) -> c_6() 26.82/7.71 , div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , div^#(0(), y) -> c_8() 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(0(), s(y), z) -> c_10() 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 26.82/7.71 and mark the set of starting terms. 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(x, 0()) -> c_1() 26.82/7.71 , plus^#(0(), y) -> c_2() 26.82/7.71 , plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(0(), y) -> c_4() 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , times^#(s(0()), y) -> c_6() 26.82/7.71 , div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , div^#(0(), y) -> c_8() 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(0(), s(y), z) -> c_10() 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y 26.82/7.71 , div(x, y) -> quot(x, y, y) 26.82/7.71 , div(0(), y) -> 0() 26.82/7.71 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 26.82/7.71 , quot(0(), s(y), z) -> 0() 26.82/7.71 , quot(s(x), s(y), z) -> quot(x, y, z) } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We estimate the number of application of {1,2,4,6,8,10} by 26.82/7.71 applications of Pre({1,2,4,6,8,10}) = {3,5,7,9,11}. Here rules are 26.82/7.71 labeled as follows: 26.82/7.71 26.82/7.71 DPs: 26.82/7.71 { 1: plus^#(x, 0()) -> c_1() 26.82/7.71 , 2: plus^#(0(), y) -> c_2() 26.82/7.71 , 3: plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , 4: times^#(0(), y) -> c_4() 26.82/7.71 , 5: times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , 6: times^#(s(0()), y) -> c_6() 26.82/7.71 , 7: div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , 8: div^#(0(), y) -> c_8() 26.82/7.71 , 9: quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , 10: quot^#(0(), s(y), z) -> c_10() 26.82/7.71 , 11: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 Weak DPs: 26.82/7.71 { plus^#(x, 0()) -> c_1() 26.82/7.71 , plus^#(0(), y) -> c_2() 26.82/7.71 , times^#(0(), y) -> c_4() 26.82/7.71 , times^#(s(0()), y) -> c_6() 26.82/7.71 , div^#(0(), y) -> c_8() 26.82/7.71 , quot^#(0(), s(y), z) -> c_10() } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y 26.82/7.71 , div(x, y) -> quot(x, y, y) 26.82/7.71 , div(0(), y) -> 0() 26.82/7.71 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 26.82/7.71 , quot(0(), s(y), z) -> 0() 26.82/7.71 , quot(s(x), s(y), z) -> quot(x, y, z) } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 The following weak DPs constitute a sub-graph of the DG that is 26.82/7.71 closed under successors. The DPs are removed. 26.82/7.71 26.82/7.71 { plus^#(x, 0()) -> c_1() 26.82/7.71 , plus^#(0(), y) -> c_2() 26.82/7.71 , times^#(0(), y) -> c_4() 26.82/7.71 , times^#(s(0()), y) -> c_6() 26.82/7.71 , div^#(0(), y) -> c_8() 26.82/7.71 , quot^#(0(), s(y), z) -> c_10() } 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y 26.82/7.71 , div(x, y) -> quot(x, y, y) 26.82/7.71 , div(0(), y) -> 0() 26.82/7.71 , quot(x, 0(), s(z)) -> s(div(x, s(z))) 26.82/7.71 , quot(0(), s(y), z) -> 0() 26.82/7.71 , quot(s(x), s(y), z) -> quot(x, y, z) } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We replace rewrite rules by usable rules: 26.82/7.71 26.82/7.71 Weak Usable Rules: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We use the processor 'matrix interpretation of dimension 1' to 26.82/7.71 orient following rules strictly. 26.82/7.71 26.82/7.71 DPs: 26.82/7.71 { 5: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 26.82/7.71 Sub-proof: 26.82/7.71 ---------- 26.82/7.71 The following argument positions are usable: 26.82/7.71 Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_7) = {1}, 26.82/7.71 Uargs(c_9) = {1}, Uargs(c_11) = {1} 26.82/7.71 26.82/7.71 TcT has computed the following constructor-based matrix 26.82/7.71 interpretation satisfying not(EDA). 26.82/7.71 26.82/7.71 [plus](x1, x2) = [0] 26.82/7.71 26.82/7.71 [0] = [0] 26.82/7.71 26.82/7.71 [s](x1) = [1] x1 + [4] 26.82/7.71 26.82/7.71 [times](x1, x2) = [0] 26.82/7.71 26.82/7.71 [plus^#](x1, x2) = [0] 26.82/7.71 26.82/7.71 [c_3](x1) = [2] x1 + [0] 26.82/7.71 26.82/7.71 [times^#](x1, x2) = [0] 26.82/7.71 26.82/7.71 [c_5](x1, x2) = [2] x1 + [2] x2 + [0] 26.82/7.71 26.82/7.71 [div^#](x1, x2) = [2] x1 + [0] 26.82/7.71 26.82/7.71 [c_7](x1) = [1] x1 + [0] 26.82/7.71 26.82/7.71 [quot^#](x1, x2, x3) = [2] x1 + [0] 26.82/7.71 26.82/7.71 [c_9](x1) = [1] x1 + [0] 26.82/7.71 26.82/7.71 [c_11](x1) = [1] x1 + [5] 26.82/7.71 26.82/7.71 The order satisfies the following ordering constraints: 26.82/7.71 26.82/7.71 [plus(x, 0())] = [0] 26.82/7.71 ? [1] x + [0] 26.82/7.71 = [x] 26.82/7.71 26.82/7.71 [plus(0(), y)] = [0] 26.82/7.71 ? [1] y + [0] 26.82/7.71 = [y] 26.82/7.71 26.82/7.71 [plus(s(x), y)] = [0] 26.82/7.71 ? [4] 26.82/7.71 = [s(plus(x, y))] 26.82/7.71 26.82/7.71 [times(0(), y)] = [0] 26.82/7.71 >= [0] 26.82/7.71 = [0()] 26.82/7.71 26.82/7.71 [times(s(x), y)] = [0] 26.82/7.71 >= [0] 26.82/7.71 = [plus(y, times(x, y))] 26.82/7.71 26.82/7.71 [times(s(0()), y)] = [0] 26.82/7.71 ? [1] y + [0] 26.82/7.71 = [y] 26.82/7.71 26.82/7.71 [plus^#(s(x), y)] = [0] 26.82/7.71 >= [0] 26.82/7.71 = [c_3(plus^#(x, y))] 26.82/7.71 26.82/7.71 [times^#(s(x), y)] = [0] 26.82/7.71 >= [0] 26.82/7.71 = [c_5(plus^#(y, times(x, y)), times^#(x, y))] 26.82/7.71 26.82/7.71 [div^#(x, y)] = [2] x + [0] 26.82/7.71 >= [2] x + [0] 26.82/7.71 = [c_7(quot^#(x, y, y))] 26.82/7.71 26.82/7.71 [quot^#(x, 0(), s(z))] = [2] x + [0] 26.82/7.71 >= [2] x + [0] 26.82/7.71 = [c_9(div^#(x, s(z)))] 26.82/7.71 26.82/7.71 [quot^#(s(x), s(y), z)] = [2] x + [8] 26.82/7.71 > [2] x + [5] 26.82/7.71 = [c_11(quot^#(x, y, z))] 26.82/7.71 26.82/7.71 26.82/7.71 We return to the main proof. Consider the set of all dependency 26.82/7.71 pairs 26.82/7.71 26.82/7.71 : 26.82/7.71 { 1: plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , 2: times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) 26.82/7.71 , 3: div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , 4: quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , 5: quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 26.82/7.71 Processor 'matrix interpretation of dimension 1' induces the 26.82/7.71 complexity certificate YES(?,O(n^1)) on application of dependency 26.82/7.71 pairs {5}. These cover all (indirect) predecessors of dependency 26.82/7.71 pairs {3,4,5}, their number of application is equally bounded. The 26.82/7.71 dependency pairs are shifted into the weak component. 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) } 26.82/7.71 Weak DPs: 26.82/7.71 { div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 The following weak DPs constitute a sub-graph of the DG that is 26.82/7.71 closed under successors. The DPs are removed. 26.82/7.71 26.82/7.71 { div^#(x, y) -> c_7(quot^#(x, y, y)) 26.82/7.71 , quot^#(x, 0(), s(z)) -> c_9(div^#(x, s(z))) 26.82/7.71 , quot^#(s(x), s(y), z) -> c_11(quot^#(x, y, z)) } 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(n^2)). 26.82/7.71 26.82/7.71 Strict DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(n^2)) 26.82/7.71 26.82/7.71 We use the processor 'Small Polynomial Path Order (PS,2-bounded)' 26.82/7.71 to orient following rules strictly. 26.82/7.71 26.82/7.71 DPs: 26.82/7.71 { 1: plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , 2: times^#(s(x), y) -> 26.82/7.71 c_5(plus^#(y, times(x, y)), times^#(x, y)) } 26.82/7.71 Trs: 26.82/7.71 { plus(0(), y) -> y 26.82/7.71 , times(0(), y) -> 0() } 26.82/7.71 26.82/7.71 Sub-proof: 26.82/7.71 ---------- 26.82/7.71 The input was oriented with the instance of 'Small Polynomial Path 26.82/7.71 Order (PS,2-bounded)' as induced by the safe mapping 26.82/7.71 26.82/7.71 safe(plus) = {}, safe(0) = {}, safe(s) = {1}, safe(times) = {}, 26.82/7.71 safe(plus^#) = {2}, safe(c_3) = {}, safe(times^#) = {}, 26.82/7.71 safe(c_5) = {}, safe(div^#) = {}, safe(c_7) = {}, 26.82/7.71 safe(quot^#) = {}, safe(c_9) = {}, safe(c_11) = {} 26.82/7.71 26.82/7.71 and precedence 26.82/7.71 26.82/7.71 times > plus, times > plus^#, times^# > plus, times^# > plus^#, 26.82/7.71 plus ~ plus^#, times ~ times^# . 26.82/7.71 26.82/7.71 Following symbols are considered recursive: 26.82/7.71 26.82/7.71 {plus, times, plus^#, times^#} 26.82/7.71 26.82/7.71 The recursion depth is 2. 26.82/7.71 26.82/7.71 Further, following argument filtering is employed: 26.82/7.71 26.82/7.71 pi(plus) = [2], pi(0) = [], pi(s) = [1], pi(times) = [], 26.82/7.71 pi(plus^#) = [1], pi(c_3) = [1], pi(times^#) = [1, 2], 26.82/7.71 pi(c_5) = [1, 2], pi(div^#) = [], pi(c_7) = [], pi(quot^#) = [], 26.82/7.71 pi(c_9) = [], pi(c_11) = [] 26.82/7.71 26.82/7.71 Usable defined function symbols are a subset of: 26.82/7.71 26.82/7.71 {plus^#, times^#, div^#, quot^#} 26.82/7.71 26.82/7.71 For your convenience, here are the satisfied ordering constraints: 26.82/7.71 26.82/7.71 pi(plus^#(s(x), y)) = plus^#(s(; x);) 26.82/7.71 > c_3(plus^#(x;);) 26.82/7.71 = pi(c_3(plus^#(x, y))) 26.82/7.71 26.82/7.71 pi(times^#(s(x), y)) = times^#(s(; x), y;) 26.82/7.71 > c_5(plus^#(y;), times^#(x, y;);) 26.82/7.71 = pi(c_5(plus^#(y, times(x, y)), times^#(x, y))) 26.82/7.71 26.82/7.71 26.82/7.71 The strictly oriented rules are moved into the weak component. 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(1)). 26.82/7.71 26.82/7.71 Weak DPs: 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) } 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(1)) 26.82/7.71 26.82/7.71 The following weak DPs constitute a sub-graph of the DG that is 26.82/7.71 closed under successors. The DPs are removed. 26.82/7.71 26.82/7.71 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 26.82/7.71 , times^#(s(x), y) -> c_5(plus^#(y, times(x, y)), times^#(x, y)) } 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(1)). 26.82/7.71 26.82/7.71 Weak Trs: 26.82/7.71 { plus(x, 0()) -> x 26.82/7.71 , plus(0(), y) -> y 26.82/7.71 , plus(s(x), y) -> s(plus(x, y)) 26.82/7.71 , times(0(), y) -> 0() 26.82/7.71 , times(s(x), y) -> plus(y, times(x, y)) 26.82/7.71 , times(s(0()), y) -> y } 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(1)) 26.82/7.71 26.82/7.71 No rule is usable, rules are removed from the input problem. 26.82/7.71 26.82/7.71 We are left with following problem, upon which TcT provides the 26.82/7.71 certificate YES(O(1),O(1)). 26.82/7.71 26.82/7.71 Rules: Empty 26.82/7.71 Obligation: 26.82/7.71 innermost runtime complexity 26.82/7.71 Answer: 26.82/7.71 YES(O(1),O(1)) 26.82/7.71 26.82/7.71 Empty rules are trivially bounded 26.82/7.71 26.82/7.71 Hurray, we answered YES(O(1),O(n^2)) 26.82/7.71 EOF