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