YES(O(1),O(n^1)) 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) 60.96/18.59 , plus(0(), y) -> y 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 The weightgap principle applies (using the following nonconstant 60.96/18.59 growth matrix-interpretation) 60.96/18.59 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following matrix interpretation satisfying 60.96/18.59 not(EDA) and not(IDA(1)). 60.96/18.59 60.96/18.59 [minus](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [0] = [7] 60.96/18.59 60.96/18.59 [s](x1) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [quot](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [plus](x1, x2) = [1] x1 + [1] x2 + [7] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [7] 60.96/18.59 >= [7] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [1] x + [1] y + [7] 60.96/18.59 >= [1] x + [1] y + [7] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [1] y + [14] 60.96/18.59 > [1] y + [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [1] x + [1] y + [7] 60.96/18.59 >= [1] x + [1] y + [7] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Weak Trs: { plus(0(), y) -> y } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 The weightgap principle applies (using the following nonconstant 60.96/18.59 growth matrix-interpretation) 60.96/18.59 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following matrix interpretation satisfying 60.96/18.59 not(EDA) and not(IDA(1)). 60.96/18.59 60.96/18.59 [minus](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [0] = [0] 60.96/18.59 60.96/18.59 [s](x1) = [1] x1 + [4] 60.96/18.59 60.96/18.59 [quot](x1, x2) = [1] x1 + [1] x2 + [0] 60.96/18.59 60.96/18.59 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1] x + [4] 60.96/18.59 > [1] x + [0] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [1] y + [4] 60.96/18.59 > [0] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [1] x + [1] y + [8] 60.96/18.59 >= [1] x + [1] y + [8] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [1] x + [1] y + [0] 60.96/18.59 >= [1] x + [1] y + [0] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [1] y + [0] 60.96/18.59 >= [1] y + [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [1] x + [1] y + [4] 60.96/18.59 >= [1] x + [1] y + [4] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Weak Trs: 60.96/18.59 { minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , plus(0(), y) -> y } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 The weightgap principle applies (using the following nonconstant 60.96/18.59 growth matrix-interpretation) 60.96/18.59 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following matrix interpretation satisfying 60.96/18.59 not(EDA) and not(IDA(1)). 60.96/18.59 60.96/18.59 [minus](x1, x2) = [1] x1 + [4] 60.96/18.59 60.96/18.59 [0] = [3] 60.96/18.59 60.96/18.59 [s](x1) = [1] x1 + [4] 60.96/18.59 60.96/18.59 [quot](x1, x2) = [1] x1 + [1] 60.96/18.59 60.96/18.59 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1] x + [4] 60.96/18.59 > [1] x + [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1] x + [8] 60.96/18.59 > [1] x + [4] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [4] 60.96/18.59 > [3] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [1] x + [5] 60.96/18.59 ? [1] x + [9] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [1] x + [1] y + [8] 60.96/18.59 >= [1] x + [1] y + [8] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [1] y + [3] 60.96/18.59 > [1] y + [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [1] x + [1] y + [4] 60.96/18.59 >= [1] x + [1] y + [4] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Weak Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , plus(0(), y) -> y } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 We use the processor 'matrix interpretation of dimension 1' to 60.96/18.59 orient following rules strictly. 60.96/18.59 60.96/18.59 Trs: { plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 60.96/18.59 The induced complexity on above rules (modulo remaining rules) is 60.96/18.59 YES(?,O(n^1)) . These rules are moved into the corresponding weak 60.96/18.59 component(s). 60.96/18.59 60.96/18.59 Sub-proof: 60.96/18.59 ---------- 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following constructor-based matrix 60.96/18.59 interpretation satisfying not(EDA). 60.96/18.59 60.96/18.59 [minus](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [0] = [0] 60.96/18.59 60.96/18.59 [s](x1) = [1] x1 + [1] 60.96/18.59 60.96/18.59 [quot](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [plus](x1, x2) = [4] x1 + [4] x2 + [0] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1] x + [1] 60.96/18.59 > [1] x + [0] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [0] 60.96/18.59 >= [0] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [1] x + [1] 60.96/18.59 >= [1] x + [1] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [4] x + [4] y + [0] 60.96/18.59 >= [4] x + [4] y + [0] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [4] y + [0] 60.96/18.59 >= [1] y + [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [4] x + [4] y + [4] 60.96/18.59 > [4] x + [4] y + [1] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 We return to the main proof. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) } 60.96/18.59 Weak Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , plus(0(), y) -> y 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 We use the processor 'matrix interpretation of dimension 1' to 60.96/18.59 orient following rules strictly. 60.96/18.59 60.96/18.59 Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 60.96/18.59 60.96/18.59 The induced complexity on above rules (modulo remaining rules) is 60.96/18.59 YES(?,O(n^1)) . These rules are moved into the corresponding weak 60.96/18.59 component(s). 60.96/18.59 60.96/18.59 Sub-proof: 60.96/18.59 ---------- 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following constructor-based matrix 60.96/18.59 interpretation satisfying not(EDA). 60.96/18.59 60.96/18.59 [minus](x1, x2) = [1] x1 + [0] 60.96/18.59 60.96/18.59 [0] = [4] 60.96/18.59 60.96/18.59 [s](x1) = [1] x1 + [4] 60.96/18.59 60.96/18.59 [quot](x1, x2) = [2] x1 + [0] 60.96/18.59 60.96/18.59 [plus](x1, x2) = [2] x1 + [2] x2 + [0] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1] x + [0] 60.96/18.59 >= [1] x + [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1] x + [4] 60.96/18.59 > [1] x + [0] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [8] 60.96/18.59 > [4] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [2] x + [8] 60.96/18.59 > [2] x + [4] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [2] x + [2] y + [0] 60.96/18.59 >= [2] x + [2] y + [0] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [2] y + [8] 60.96/18.59 > [1] y + [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [2] x + [2] y + [8] 60.96/18.59 > [2] x + [2] y + [4] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 We return to the main proof. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(n^1)). 60.96/18.59 60.96/18.59 Strict Trs: 60.96/18.59 { plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) } 60.96/18.59 Weak Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(0(), y) -> y 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(n^1)) 60.96/18.59 60.96/18.59 We use the processor 'matrix interpretation of dimension 3' to 60.96/18.59 orient following rules strictly. 60.96/18.59 60.96/18.59 Trs: 60.96/18.59 { plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) } 60.96/18.59 60.96/18.59 The induced complexity on above rules (modulo remaining rules) is 60.96/18.59 YES(?,O(n^1)) . These rules are moved into the corresponding weak 60.96/18.59 component(s). 60.96/18.59 60.96/18.59 Sub-proof: 60.96/18.59 ---------- 60.96/18.59 The following argument positions are usable: 60.96/18.59 Uargs(s) = {1}, Uargs(quot) = {1} 60.96/18.59 60.96/18.59 TcT has computed the following constructor-based matrix 60.96/18.59 interpretation satisfying not(EDA) and not(IDA(1)). 60.96/18.59 60.96/18.59 [1 0 0] [0 0 0] [0] 60.96/18.59 [minus](x1, x2) = [2 2 2] x1 + [0 0 2] x2 + [0] 60.96/18.59 [0 4 4] [0 1 5] [0] 60.96/18.59 60.96/18.59 [0] 60.96/18.59 [0] = [0] 60.96/18.59 [1] 60.96/18.59 60.96/18.59 [1 0 0] [4] 60.96/18.59 [s](x1) = [0 1 0] x1 + [2] 60.96/18.59 [0 0 1] [0] 60.96/18.59 60.96/18.59 [1 0 0] [4] 60.96/18.59 [quot](x1, x2) = [2 0 0] x1 + [0] 60.96/18.59 [0 0 0] [4] 60.96/18.59 60.96/18.59 [0 2 0] [4 0 1] [0] 60.96/18.59 [plus](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [2] 60.96/18.59 [2 2 0] [6 0 1] [0] 60.96/18.59 60.96/18.59 The order satisfies the following ordering constraints: 60.96/18.59 60.96/18.59 [minus(x, 0())] = [1 0 0] [0] 60.96/18.59 [2 2 2] x + [2] 60.96/18.59 [0 4 4] [5] 60.96/18.59 >= [1 0 0] [0] 60.96/18.59 [0 1 0] x + [0] 60.96/18.59 [0 0 1] [0] 60.96/18.59 = [x] 60.96/18.59 60.96/18.59 [minus(s(x), s(y))] = [1 0 0] [0 0 0] [4] 60.96/18.59 [2 2 2] x + [0 0 2] y + [12] 60.96/18.59 [0 4 4] [0 1 5] [10] 60.96/18.59 > [1 0 0] [0 0 0] [0] 60.96/18.59 [2 2 2] x + [0 0 2] y + [0] 60.96/18.59 [0 4 4] [0 1 5] [0] 60.96/18.59 = [minus(x, y)] 60.96/18.59 60.96/18.59 [quot(0(), s(y))] = [4] 60.96/18.59 [0] 60.96/18.59 [4] 60.96/18.59 > [0] 60.96/18.59 [0] 60.96/18.59 [1] 60.96/18.59 = [0()] 60.96/18.59 60.96/18.59 [quot(s(x), s(y))] = [1 0 0] [8] 60.96/18.59 [2 0 0] x + [8] 60.96/18.59 [0 0 0] [4] 60.96/18.59 >= [1 0 0] [8] 60.96/18.59 [2 0 0] x + [2] 60.96/18.59 [0 0 0] [4] 60.96/18.59 = [s(quot(minus(x, y), s(y)))] 60.96/18.59 60.96/18.59 [plus(minus(x, s(0())), minus(y, s(s(z))))] = [4 4 4] [4 4 4] [0 1 5] [8] 60.96/18.59 [2 2 2] x + [2 2 2] y + [0 0 2] z + [4] 60.96/18.59 [6 4 4] [6 4 4] [0 1 5] [8] 60.96/18.59 > [4 4 4] [4 4 4] [0 0 4] [7] 60.96/18.59 [2 2 2] x + [2 2 2] y + [0 0 2] z + [4] 60.96/18.59 [6 4 4] [6 4 4] [0 0 4] [7] 60.96/18.59 = [plus(minus(y, s(s(z))), minus(x, s(0())))] 60.96/18.59 60.96/18.59 [plus(0(), y)] = [4 0 1] [0] 60.96/18.59 [0 1 0] y + [2] 60.96/18.59 [6 0 1] [0] 60.96/18.59 >= [1 0 0] [0] 60.96/18.59 [0 1 0] y + [0] 60.96/18.59 [0 0 1] [0] 60.96/18.59 = [y] 60.96/18.59 60.96/18.59 [plus(s(x), y)] = [0 2 0] [4 0 1] [4] 60.96/18.59 [0 1 0] x + [0 1 0] y + [4] 60.96/18.59 [2 2 0] [6 0 1] [12] 60.96/18.59 >= [0 2 0] [4 0 1] [4] 60.96/18.59 [0 1 0] x + [0 1 0] y + [4] 60.96/18.59 [2 2 0] [6 0 1] [0] 60.96/18.59 = [s(plus(x, y))] 60.96/18.59 60.96/18.59 60.96/18.59 We return to the main proof. 60.96/18.59 60.96/18.59 We are left with following problem, upon which TcT provides the 60.96/18.59 certificate YES(O(1),O(1)). 60.96/18.59 60.96/18.59 Weak Trs: 60.96/18.59 { minus(x, 0()) -> x 60.96/18.59 , minus(s(x), s(y)) -> minus(x, y) 60.96/18.59 , quot(0(), s(y)) -> 0() 60.96/18.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 60.96/18.59 , plus(minus(x, s(0())), minus(y, s(s(z)))) -> 60.96/18.59 plus(minus(y, s(s(z))), minus(x, s(0()))) 60.96/18.59 , plus(0(), y) -> y 60.96/18.59 , plus(s(x), y) -> s(plus(x, y)) } 60.96/18.59 Obligation: 60.96/18.59 innermost runtime complexity 60.96/18.59 Answer: 60.96/18.59 YES(O(1),O(1)) 60.96/18.59 60.96/18.59 Empty rules are trivially bounded 60.96/18.59 60.96/18.59 Hurray, we answered YES(O(1),O(n^1)) 61.38/18.71 EOF