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