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