YES(O(1),O(n^2)) 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(n^2)). 185.13/81.54 185.13/81.54 Strict Trs: 185.13/81.54 { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) 185.13/81.54 , :(:(x, y), z) -> :(x, :(y, z)) 185.13/81.54 , :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We add the following weak dependency pairs: 185.13/81.54 185.13/81.54 Strict DPs: 185.13/81.54 { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 185.13/81.54 and mark the set of starting terms. 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(n^2)). 185.13/81.54 185.13/81.54 Strict DPs: 185.13/81.54 { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Strict Trs: 185.13/81.54 { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) 185.13/81.54 , :(:(x, y), z) -> :(x, :(y, z)) 185.13/81.54 , :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We estimate the number of application of {1} by applications of 185.13/81.54 Pre({1}) = {3}. Here rules are labeled as follows: 185.13/81.54 185.13/81.54 DPs: 185.13/81.54 { 1: :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , 2: :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , 3: :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(n^2)). 185.13/81.54 185.13/81.54 Strict DPs: 185.13/81.54 { :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Strict Trs: 185.13/81.54 { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) 185.13/81.54 , :(:(x, y), z) -> :(x, :(y, z)) 185.13/81.54 , :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Weak DPs: { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We use the processor 'polynomial interpretation' to orient 185.13/81.54 following rules strictly. 185.13/81.54 185.13/81.54 DPs: { :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Trs: { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) } 185.13/81.54 185.13/81.54 The induced complexity on above rules (modulo remaining rules) is 185.13/81.54 YES(?,O(n^2)) . These rules are moved into the corresponding weak 185.13/81.54 component(s). 185.13/81.54 185.13/81.54 Sub-proof: 185.13/81.54 ---------- 185.13/81.54 We consider the following typing: 185.13/81.54 185.13/81.54 : :: (b,b) -> b 185.13/81.54 + :: (b,b) -> b 185.13/81.54 f :: a -> b 185.13/81.54 g :: (b,a) -> b 185.13/81.54 a :: b 185.13/81.54 :^# :: (b,b) -> c 185.13/81.54 c_1 :: c -> c 185.13/81.54 c_2 :: c -> c 185.13/81.54 c_3 :: (c,c) -> c 185.13/81.54 185.13/81.54 The following argument positions are considered usable: 185.13/81.54 185.13/81.54 Uargs(:) = {2}, Uargs(+) = {1, 2}, Uargs(:^#) = {2}, 185.13/81.54 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} 185.13/81.54 185.13/81.54 TcT has computed the following constructor-restricted 185.13/81.54 typedpolynomial interpretation. 185.13/81.54 185.13/81.54 [:](x1, x2) = x1 + x1*x2 + x2 185.13/81.54 185.13/81.54 [+](x1, x2) = 1 + x1 + x2 185.13/81.54 185.13/81.54 [f](x1) = 2 185.13/81.54 185.13/81.54 [g](x1, x2) = 0 185.13/81.54 185.13/81.54 [a]() = 1 185.13/81.54 185.13/81.54 [:^#](x1, x2) = 2*x1 + x1*x2 + x2 185.13/81.54 185.13/81.54 [c_1](x1) = x1 185.13/81.54 185.13/81.54 [c_2](x1) = x1 185.13/81.54 185.13/81.54 [c_3](x1, x2) = x1 + x2 185.13/81.54 185.13/81.54 185.13/81.54 This order satisfies the following ordering constraints. 185.13/81.54 185.13/81.54 [:(z, +(x, f(y)))] = 4*z + z*x + 3 + x 185.13/81.54 > 2 + x 185.13/81.54 = [:(g(z, y), +(x, a()))] 185.13/81.54 185.13/81.54 [:(:(x, y), z)] = x + x*y + y + x*z + x*y*z + y*z + z 185.13/81.54 >= x + x*y + x*y*z + x*z + y + y*z + z 185.13/81.54 = [:(x, :(y, z))] 185.13/81.54 185.13/81.54 [:(+(x, y), z)] = 1 + x + y + 2*z + x*z + y*z 185.13/81.54 >= 1 + x + x*z + 2*z + y + y*z 185.13/81.54 = [+(:(x, z), :(y, z))] 185.13/81.54 185.13/81.54 185.13/81.54 We return to the main proof. 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(n^2)). 185.13/81.54 185.13/81.54 Strict DPs: { :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) } 185.13/81.54 Strict Trs: 185.13/81.54 { :(:(x, y), z) -> :(x, :(y, z)) 185.13/81.54 , :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Weak DPs: 185.13/81.54 { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Weak Trs: { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We use the processor 'polynomial interpretation' to orient 185.13/81.54 following rules strictly. 185.13/81.54 185.13/81.54 DPs: { :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) } 185.13/81.54 Trs: { :(:(x, y), z) -> :(x, :(y, z)) } 185.13/81.54 185.13/81.54 The induced complexity on above rules (modulo remaining rules) is 185.13/81.54 YES(?,O(n^2)) . These rules are moved into the corresponding weak 185.13/81.54 component(s). 185.13/81.54 185.13/81.54 Sub-proof: 185.13/81.54 ---------- 185.13/81.54 We consider the following typing: 185.13/81.54 185.13/81.54 : :: (b,b) -> b 185.13/81.54 + :: (b,b) -> b 185.13/81.54 f :: a -> b 185.13/81.54 g :: (b,a) -> b 185.13/81.54 a :: b 185.13/81.54 :^# :: (b,b) -> c 185.13/81.54 c_1 :: c -> c 185.13/81.54 c_2 :: c -> c 185.13/81.54 c_3 :: (c,c) -> c 185.13/81.54 185.13/81.54 The following argument positions are considered usable: 185.13/81.54 185.13/81.54 Uargs(:) = {2}, Uargs(+) = {1, 2}, Uargs(:^#) = {2}, 185.13/81.54 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} 185.13/81.54 185.13/81.54 TcT has computed the following constructor-restricted 185.13/81.54 typedpolynomial interpretation. 185.13/81.54 185.13/81.54 [:](x1, x2) = 1 + x1 + x1*x2 + x1^2 + x2 185.13/81.54 185.13/81.54 [+](x1, x2) = 1 + x1 + x2 185.13/81.54 185.13/81.54 [f](x1) = 2 185.13/81.54 185.13/81.54 [g](x1, x2) = 0 185.13/81.54 185.13/81.54 [a]() = 1 185.13/81.54 185.13/81.54 [:^#](x1, x2) = 2*x1 + x1*x2 + x1^2 + x2 185.13/81.54 185.13/81.54 [c_1](x1) = x1 185.13/81.54 185.13/81.54 [c_2](x1) = x1 185.13/81.54 185.13/81.54 [c_3](x1, x2) = 1 + x1 + x2 185.13/81.54 185.13/81.54 185.13/81.54 This order satisfies the following ordering constraints. 185.13/81.54 185.13/81.54 [:(z, +(x, f(y)))] = 4 + 4*z + z*x + z^2 + x 185.13/81.54 > 3 + x 185.13/81.54 = [:(g(z, y), +(x, a()))] 185.13/81.54 185.13/81.54 [:(:(x, y), z)] = 3 + 3*x + 4*x*y + 4*x^2 + 3*y + 2*z + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 185.13/81.54 > 2 + 2*x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z 185.13/81.54 = [:(x, :(y, z))] 185.13/81.54 185.13/81.54 [:(+(x, y), z)] = 3 + 3*x + 3*y + 2*z + x*z + y*z + x^2 + x*y + y*x + y^2 185.13/81.54 >= 3 + x + x*z + x^2 + 2*z + y + y*z + y^2 185.13/81.54 = [+(:(x, z), :(y, z))] 185.13/81.54 185.13/81.54 185.13/81.54 We return to the main proof. 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(n^2)). 185.13/81.54 185.13/81.54 Strict Trs: { :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Weak DPs: 185.13/81.54 { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Weak Trs: 185.13/81.54 { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) 185.13/81.54 , :(:(x, y), z) -> :(x, :(y, z)) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(n^2)) 185.13/81.54 185.13/81.54 We use the processor 'polynomial interpretation' to orient 185.13/81.54 following rules strictly. 185.13/81.54 185.13/81.54 Trs: { :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 185.13/81.54 The induced complexity on above rules (modulo remaining rules) is 185.13/81.54 YES(?,O(n^2)) . These rules are moved into the corresponding weak 185.13/81.54 component(s). 185.13/81.54 185.13/81.54 Sub-proof: 185.13/81.54 ---------- 185.13/81.54 We consider the following typing: 185.13/81.54 185.13/81.54 : :: (b,b) -> b 185.13/81.54 + :: (b,b) -> b 185.13/81.54 f :: a -> b 185.13/81.54 g :: (b,a) -> b 185.13/81.54 a :: b 185.13/81.54 :^# :: (b,b) -> c 185.13/81.54 c_1 :: c -> c 185.13/81.54 c_2 :: c -> c 185.13/81.54 c_3 :: (c,c) -> c 185.13/81.54 185.13/81.54 The following argument positions are considered usable: 185.13/81.54 185.13/81.54 Uargs(:) = {2}, Uargs(+) = {1, 2}, Uargs(:^#) = {2}, 185.13/81.54 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} 185.13/81.54 185.13/81.54 TcT has computed the following constructor-restricted 185.13/81.54 typedpolynomial interpretation. 185.13/81.54 185.13/81.54 [:](x1, x2) = x1 + x1*x2 + x1^2 + x2 185.13/81.54 185.13/81.54 [+](x1, x2) = 1 + x1 + x2 185.13/81.54 185.13/81.54 [f](x1) = 1 185.13/81.54 185.13/81.54 [g](x1, x2) = 0 185.13/81.54 185.13/81.54 [a]() = 0 185.13/81.54 185.13/81.54 [:^#](x1, x2) = x1 + 2*x1*x2 + x1^2 + x2 185.13/81.54 185.13/81.54 [c_1](x1) = x1 185.13/81.54 185.13/81.54 [c_2](x1) = x1 185.13/81.54 185.13/81.54 [c_3](x1, x2) = x1 + x2 185.13/81.54 185.13/81.54 185.13/81.54 This order satisfies the following ordering constraints. 185.13/81.54 185.13/81.54 [:(z, +(x, f(y)))] = 3*z + z*x + z^2 + 2 + x 185.13/81.54 > 1 + x 185.13/81.54 = [:(g(z, y), +(x, a()))] 185.13/81.54 185.13/81.54 [:(:(x, y), z)] = x + 2*x*y + 2*x^2 + y + x*z + x*y*z + x^2*z + y*z + 3*x^2*y + 2*x^3 + x^2*y^2 + 2*x^3*y + x*y^2 + x^4 + y*x + y^2*x + y*x^2 + y^2 + z 185.13/81.54 >= x + x*y + x*y*z + x*y^2 + x*z + x^2 + y + y*z + y^2 + z 185.13/81.54 = [:(x, :(y, z))] 185.13/81.54 185.13/81.54 [:(+(x, y), z)] = 2 + 3*x + 3*y + 2*z + x*z + y*z + x^2 + x*y + y*x + y^2 185.13/81.54 > 1 + x + x*z + x^2 + 2*z + y + y*z + y^2 185.13/81.54 = [+(:(x, z), :(y, z))] 185.13/81.54 185.13/81.54 185.13/81.54 We return to the main proof. 185.13/81.54 185.13/81.54 We are left with following problem, upon which TcT provides the 185.13/81.54 certificate YES(O(1),O(1)). 185.13/81.54 185.13/81.54 Weak DPs: 185.13/81.54 { :^#(z, +(x, f(y))) -> c_1(:^#(g(z, y), +(x, a()))) 185.13/81.54 , :^#(:(x, y), z) -> c_2(:^#(x, :(y, z))) 185.13/81.54 , :^#(+(x, y), z) -> c_3(:^#(x, z), :^#(y, z)) } 185.13/81.54 Weak Trs: 185.13/81.54 { :(z, +(x, f(y))) -> :(g(z, y), +(x, a())) 185.13/81.54 , :(:(x, y), z) -> :(x, :(y, z)) 185.13/81.54 , :(+(x, y), z) -> +(:(x, z), :(y, z)) } 185.13/81.54 Obligation: 185.13/81.54 runtime complexity 185.13/81.54 Answer: 185.13/81.54 YES(O(1),O(1)) 185.13/81.54 185.13/81.54 Empty rules are trivially bounded 185.13/81.54 185.13/81.54 Hurray, we answered YES(O(1),O(n^2)) 185.32/81.63 EOF