YES(O(1),O(n^2)) 897.31/297.77 YES(O(1),O(n^2)) 897.31/297.77 897.31/297.77 We are left with following problem, upon which TcT provides the 897.31/297.77 certificate YES(O(1),O(n^2)). 897.31/297.77 897.31/297.77 Strict Trs: 897.31/297.77 { f(0()) -> 1() 897.31/297.77 , f(s(x)) -> g(x, s(x)) 897.31/297.77 , g(0(), y) -> y 897.31/297.77 , g(s(x), y) -> g(x, s(+(y, x))) 897.31/297.77 , g(s(x), y) -> g(x, +(y, s(x))) 897.31/297.77 , +(x, 0()) -> x 897.31/297.77 , +(x, s(y)) -> s(+(x, y)) } 897.31/297.77 Obligation: 897.31/297.77 runtime complexity 897.31/297.77 Answer: 897.31/297.77 YES(O(1),O(n^2)) 897.31/297.77 897.31/297.77 The weightgap principle applies (using the following nonconstant 897.31/297.77 growth matrix-interpretation) 897.31/297.77 897.31/297.77 The following argument positions are usable: 897.31/297.77 Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1} 897.31/297.77 897.31/297.77 TcT has computed the following matrix interpretation satisfying 897.31/297.77 not(EDA) and not(IDA(1)). 897.31/297.77 897.31/297.77 [f](x1) = [1] x1 + [7] 897.31/297.77 897.31/297.77 [0] = [7] 897.31/297.77 897.31/297.77 [1] = [5] 897.31/297.77 897.31/297.77 [s](x1) = [1] x1 + [7] 897.31/297.77 897.31/297.77 [g](x1, x2) = [1] x2 + [1] 897.31/297.77 897.31/297.77 [+](x1, x2) = [1] x1 + [7] 897.31/297.77 897.31/297.77 The order satisfies the following ordering constraints: 897.31/297.77 897.31/297.77 [f(0())] = [14] 897.31/297.77 > [5] 897.31/297.77 = [1()] 897.31/297.77 897.31/297.77 [f(s(x))] = [1] x + [14] 897.31/297.77 > [1] x + [8] 897.31/297.77 = [g(x, s(x))] 897.31/297.77 897.31/297.77 [g(0(), y)] = [1] y + [1] 897.31/297.77 > [1] y + [0] 897.31/297.77 = [y] 897.31/297.77 897.31/297.77 [g(s(x), y)] = [1] y + [1] 897.31/297.77 ? [1] y + [15] 897.31/297.77 = [g(x, s(+(y, x)))] 897.31/297.77 897.31/297.77 [g(s(x), y)] = [1] y + [1] 897.31/297.77 ? [1] y + [8] 897.31/297.77 = [g(x, +(y, s(x)))] 897.31/297.77 897.31/297.77 [+(x, 0())] = [1] x + [7] 897.31/297.77 > [1] x + [0] 897.31/297.77 = [x] 897.31/297.77 897.31/297.77 [+(x, s(y))] = [1] x + [7] 897.31/297.77 ? [1] x + [14] 897.31/297.77 = [s(+(x, y))] 897.31/297.77 897.31/297.77 897.31/297.77 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 897.31/297.77 897.31/297.77 We are left with following problem, upon which TcT provides the 897.31/297.77 certificate YES(O(1),O(n^2)). 897.31/297.77 897.31/297.77 Strict Trs: 897.31/297.77 { g(s(x), y) -> g(x, s(+(y, x))) 897.31/297.77 , g(s(x), y) -> g(x, +(y, s(x))) 897.31/297.77 , +(x, s(y)) -> s(+(x, y)) } 897.31/297.77 Weak Trs: 897.31/297.77 { f(0()) -> 1() 897.31/297.77 , f(s(x)) -> g(x, s(x)) 897.31/297.77 , g(0(), y) -> y 897.31/297.77 , +(x, 0()) -> x } 897.31/297.77 Obligation: 897.31/297.77 runtime complexity 897.31/297.77 Answer: 897.31/297.77 YES(O(1),O(n^2)) 897.31/297.77 897.31/297.77 We use the processor 'polynomial interpretation' to orient 897.31/297.77 following rules strictly. 897.31/297.77 897.31/297.77 Trs: 897.31/297.77 { g(s(x), y) -> g(x, s(+(y, x))) 897.31/297.77 , +(x, s(y)) -> s(+(x, y)) } 897.31/297.77 897.31/297.77 The induced complexity on above rules (modulo remaining rules) is 897.31/297.77 YES(?,O(n^2)) . These rules are moved into the corresponding weak 897.31/297.77 component(s). 897.31/297.77 897.31/297.77 Sub-proof: 897.31/297.77 ---------- 897.31/297.77 We consider the following typing: 897.31/297.77 897.31/297.77 f :: a -> a 897.31/297.77 0 :: a 897.31/297.77 1 :: a 897.31/297.77 s :: a -> a 897.31/297.77 g :: (a,a) -> a 897.31/297.77 + :: (a,a) -> a 897.31/297.77 897.31/297.77 The following argument positions are considered usable: 897.31/297.77 897.31/297.77 Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1} 897.31/297.77 897.31/297.77 TcT has computed the following constructor-restricted 897.31/297.77 typedpolynomial interpretation. 897.31/297.77 897.31/297.77 [f](x1) = x1^2 897.31/297.77 897.31/297.77 [0]() = 0 897.31/297.77 897.31/297.77 [1]() = 0 897.31/297.77 897.31/297.77 [s](x1) = 1 + x1 897.31/297.77 897.31/297.77 [g](x1, x2) = x1 + x1^2 + x2 897.31/297.77 897.31/297.77 [+](x1, x2) = x1 + 2*x2 897.31/297.77 897.31/297.77 897.31/297.77 This order satisfies the following ordering constraints. 897.31/297.77 897.31/297.77 [f(0())] = 897.31/297.77 >= 897.31/297.77 = [1()] 897.31/297.77 897.31/297.77 [f(s(x))] = 1 + 2*x + x^2 897.31/297.77 >= 2*x + x^2 + 1 897.31/297.77 = [g(x, s(x))] 897.31/297.77 897.31/297.77 [g(0(), y)] = y 897.31/297.77 >= y 897.31/297.77 = [y] 897.31/297.77 897.31/297.77 [g(s(x), y)] = 2 + 3*x + x^2 + y 897.31/297.77 > 3*x + x^2 + 1 + y 897.31/297.77 = [g(x, s(+(y, x)))] 897.31/297.77 897.31/297.77 [g(s(x), y)] = 2 + 3*x + x^2 + y 897.31/297.77 >= 3*x + x^2 + y + 2 897.31/297.77 = [g(x, +(y, s(x)))] 897.31/297.77 897.31/297.77 [+(x, 0())] = x 897.31/297.77 >= x 897.31/297.77 = [x] 897.31/297.77 897.31/297.77 [+(x, s(y))] = x + 2 + 2*y 897.31/297.77 > 1 + x + 2*y 897.31/297.77 = [s(+(x, y))] 897.31/297.77 897.31/297.77 897.31/297.77 We return to the main proof. 897.31/297.77 897.31/297.77 We are left with following problem, upon which TcT provides the 897.31/297.77 certificate YES(O(1),O(n^2)). 897.31/297.77 897.31/297.77 Strict Trs: { g(s(x), y) -> g(x, +(y, s(x))) } 897.31/297.77 Weak Trs: 897.31/297.77 { f(0()) -> 1() 897.31/297.77 , f(s(x)) -> g(x, s(x)) 897.31/297.77 , g(0(), y) -> y 897.31/297.77 , g(s(x), y) -> g(x, s(+(y, x))) 897.31/297.77 , +(x, 0()) -> x 897.31/297.77 , +(x, s(y)) -> s(+(x, y)) } 897.31/297.77 Obligation: 897.31/297.77 runtime complexity 897.31/297.77 Answer: 897.31/297.77 YES(O(1),O(n^2)) 897.31/297.77 897.31/297.77 We use the processor 'polynomial interpretation' to orient 897.31/297.77 following rules strictly. 897.31/297.77 897.31/297.77 Trs: { g(s(x), y) -> g(x, +(y, s(x))) } 897.31/297.77 897.31/297.77 The induced complexity on above rules (modulo remaining rules) is 897.31/297.77 YES(?,O(n^2)) . These rules are moved into the corresponding weak 897.31/297.77 component(s). 897.31/297.77 897.31/297.77 Sub-proof: 897.31/297.77 ---------- 897.31/297.77 We consider the following typing: 897.31/297.77 897.31/297.77 f :: a -> a 897.31/297.77 0 :: a 897.31/297.77 1 :: a 897.31/297.77 s :: a -> a 897.31/297.77 g :: (a,a) -> a 897.31/297.77 + :: (a,a) -> a 897.31/297.77 897.31/297.77 The following argument positions are considered usable: 897.31/297.77 897.31/297.77 Uargs(s) = {1}, Uargs(g) = {2}, Uargs(+) = {1} 897.31/297.77 897.31/297.77 TcT has computed the following constructor-restricted 897.31/297.77 typedpolynomial interpretation. 897.31/297.77 897.31/297.77 [f](x1) = x1^2 897.31/297.77 897.31/297.77 [0]() = 0 897.31/297.77 897.31/297.77 [1]() = 0 897.31/297.77 897.31/297.77 [s](x1) = 1 + x1 897.31/297.77 897.31/297.77 [g](x1, x2) = x1 + x1^2 + x2 897.31/297.77 897.31/297.77 [+](x1, x2) = x1 + x2 897.31/297.77 897.31/297.77 897.31/297.77 This order satisfies the following ordering constraints. 897.31/297.77 897.31/297.77 [f(0())] = 897.31/297.77 >= 897.31/297.77 = [1()] 897.31/297.77 897.31/297.77 [f(s(x))] = 1 + 2*x + x^2 897.31/297.77 >= 2*x + x^2 + 1 897.31/297.77 = [g(x, s(x))] 897.31/297.77 897.31/297.77 [g(0(), y)] = y 897.31/297.77 >= y 897.31/297.77 = [y] 897.31/297.77 897.31/297.77 [g(s(x), y)] = 2 + 3*x + x^2 + y 897.31/297.77 > 2*x + x^2 + 1 + y 897.31/297.77 = [g(x, s(+(y, x)))] 897.31/297.77 897.31/297.77 [g(s(x), y)] = 2 + 3*x + x^2 + y 897.31/297.77 > 2*x + x^2 + y + 1 897.31/297.77 = [g(x, +(y, s(x)))] 897.31/297.77 897.31/297.77 [+(x, 0())] = x 897.31/297.77 >= x 897.31/297.77 = [x] 897.31/297.77 897.31/297.77 [+(x, s(y))] = x + 1 + y 897.31/297.77 >= 1 + x + y 897.31/297.77 = [s(+(x, y))] 897.31/297.77 897.31/297.77 897.31/297.77 We return to the main proof. 897.31/297.77 897.31/297.77 We are left with following problem, upon which TcT provides the 897.31/297.77 certificate YES(O(1),O(1)). 897.31/297.77 897.31/297.77 Weak Trs: 897.31/297.77 { f(0()) -> 1() 897.31/297.77 , f(s(x)) -> g(x, s(x)) 897.31/297.77 , g(0(), y) -> y 897.31/297.77 , g(s(x), y) -> g(x, s(+(y, x))) 897.31/297.77 , g(s(x), y) -> g(x, +(y, s(x))) 897.31/297.77 , +(x, 0()) -> x 897.31/297.77 , +(x, s(y)) -> s(+(x, y)) } 897.31/297.77 Obligation: 897.31/297.77 runtime complexity 897.31/297.77 Answer: 897.31/297.77 YES(O(1),O(1)) 897.31/297.77 897.31/297.77 Empty rules are trivially bounded 897.31/297.77 897.31/297.77 Hurray, we answered YES(O(1),O(n^2)) 897.84/298.03 EOF