YES(O(1),O(n^2)) 360.90/107.64 YES(O(1),O(n^2)) 360.90/107.64 360.90/107.64 We are left with following problem, upon which TcT provides the 360.90/107.64 certificate YES(O(1),O(n^2)). 360.90/107.64 360.90/107.64 Strict Trs: 360.90/107.64 { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) 360.90/107.64 , f(cons(nil(), y)) -> y 360.90/107.64 , copy(0(), y, z) -> f(z) 360.90/107.64 , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) } 360.90/107.64 Obligation: 360.90/107.64 runtime complexity 360.90/107.64 Answer: 360.90/107.64 YES(O(1),O(n^2)) 360.90/107.64 360.90/107.64 We use the processor 'polynomial interpretation' to orient 360.90/107.64 following rules strictly. 360.90/107.64 360.90/107.64 Trs: { copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) } 360.90/107.64 360.90/107.64 The induced complexity on above rules (modulo remaining rules) is 360.90/107.64 YES(?,O(n^2)) . These rules are moved into the corresponding weak 360.90/107.64 component(s). 360.90/107.64 360.90/107.64 Sub-proof: 360.90/107.64 ---------- 360.90/107.64 We consider the following typing: 360.90/107.64 360.90/107.64 f :: a -> a 360.90/107.64 cons :: (a,a) -> a 360.90/107.64 nil :: a 360.90/107.64 copy :: (b,a,a) -> a 360.90/107.64 n :: b 360.90/107.64 0 :: b 360.90/107.64 s :: b -> b 360.90/107.64 360.90/107.64 The following argument positions are considered usable: 360.90/107.64 360.90/107.64 Uargs(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3} 360.90/107.64 360.90/107.64 TcT has computed the following constructor-restricted 360.90/107.64 typedpolynomial interpretation. 360.90/107.64 360.90/107.64 [f](x1) = x1 360.90/107.64 360.90/107.64 [cons](x1, x2) = x1 + x2 360.90/107.64 360.90/107.64 [nil]() = 0 360.90/107.64 360.90/107.64 [copy](x1, x2, x3) = 2*x1 + x1*x2 + x2 + x3 360.90/107.64 360.90/107.64 [n]() = 0 360.90/107.64 360.90/107.64 [0]() = 0 360.90/107.64 360.90/107.64 [s](x1) = 2 + x1 360.90/107.64 360.90/107.64 360.90/107.64 This order satisfies the following ordering constraints. 360.90/107.64 360.90/107.64 [f(cons(f(cons(nil(), y)), z))] = y + z 360.90/107.64 >= y + z 360.90/107.64 = [copy(n(), y, z)] 360.90/107.64 360.90/107.64 [f(cons(nil(), y))] = y 360.90/107.64 >= y 360.90/107.64 = [y] 360.90/107.64 360.90/107.64 [copy(0(), y, z)] = y + z 360.90/107.64 >= z 360.90/107.64 = [f(z)] 360.90/107.64 360.90/107.64 [copy(s(x), y, z)] = 4 + 2*x + 3*y + x*y + z 360.90/107.64 > 2*x + x*y + 2*y + z 360.90/107.64 = [copy(x, y, cons(f(y), z))] 360.90/107.64 360.90/107.64 360.90/107.64 We return to the main proof. 360.90/107.64 360.90/107.64 We are left with following problem, upon which TcT provides the 360.90/107.64 certificate YES(O(1),O(n^2)). 360.90/107.64 360.90/107.64 Strict Trs: 360.90/107.64 { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) 360.90/107.64 , f(cons(nil(), y)) -> y 360.90/107.64 , copy(0(), y, z) -> f(z) } 360.90/107.64 Weak Trs: { copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) } 360.90/107.64 Obligation: 360.90/107.64 runtime complexity 360.90/107.64 Answer: 360.90/107.64 YES(O(1),O(n^2)) 360.90/107.64 360.90/107.64 We use the processor 'polynomial interpretation' to orient 360.90/107.64 following rules strictly. 360.90/107.64 360.90/107.64 Trs: { copy(0(), y, z) -> f(z) } 360.90/107.64 360.90/107.64 The induced complexity on above rules (modulo remaining rules) is 360.90/107.64 YES(?,O(n^2)) . These rules are moved into the corresponding weak 360.90/107.64 component(s). 360.90/107.64 360.90/107.64 Sub-proof: 360.90/107.64 ---------- 360.90/107.64 We consider the following typing: 360.90/107.64 360.90/107.64 f :: a -> a 360.90/107.64 cons :: (a,a) -> a 360.90/107.64 nil :: a 360.90/107.64 copy :: (b,a,a) -> a 360.90/107.64 n :: b 360.90/107.64 0 :: b 360.90/107.64 s :: b -> b 360.90/107.64 360.90/107.64 The following argument positions are considered usable: 360.90/107.64 360.90/107.64 Uargs(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3} 360.90/107.64 360.90/107.64 TcT has computed the following constructor-restricted 360.90/107.64 typedpolynomial interpretation. 360.90/107.64 360.90/107.64 [f](x1) = 2*x1 360.90/107.64 360.90/107.64 [cons](x1, x2) = x1 + x2 360.90/107.64 360.90/107.64 [nil]() = 0 360.90/107.64 360.90/107.64 [copy](x1, x2, x3) = 2*x1*x2 + x1^2 + x2 + 2*x3 360.90/107.64 360.90/107.64 [n]() = 0 360.90/107.64 360.90/107.64 [0]() = 2 360.90/107.64 360.90/107.64 [s](x1) = 2 + x1 360.90/107.64 360.90/107.64 360.90/107.64 This order satisfies the following ordering constraints. 360.90/107.64 360.90/107.64 [f(cons(f(cons(nil(), y)), z))] = 4*y + 2*z 360.90/107.64 >= y + 2*z 360.90/107.64 = [copy(n(), y, z)] 360.90/107.64 360.90/107.64 [f(cons(nil(), y))] = 2*y 360.90/107.64 >= y 360.90/107.64 = [y] 360.90/107.64 360.90/107.64 [copy(0(), y, z)] = 5*y + 4 + 2*z 360.90/107.64 > 2*z 360.90/107.64 = [f(z)] 360.90/107.64 360.90/107.64 [copy(s(x), y, z)] = 5*y + 2*x*y + 4 + 4*x + x^2 + 2*z 360.90/107.64 > 2*x*y + x^2 + 5*y + 2*z 360.90/107.64 = [copy(x, y, cons(f(y), z))] 360.90/107.64 360.90/107.64 360.90/107.64 We return to the main proof. 360.90/107.64 360.90/107.64 We are left with following problem, upon which TcT provides the 360.90/107.64 certificate YES(O(1),O(n^2)). 360.90/107.64 360.90/107.64 Strict Trs: 360.90/107.64 { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) 360.90/107.64 , f(cons(nil(), y)) -> y } 360.90/107.64 Weak Trs: 360.90/107.64 { copy(0(), y, z) -> f(z) 360.90/107.64 , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) } 360.90/107.64 Obligation: 360.90/107.64 runtime complexity 360.90/107.64 Answer: 360.90/107.64 YES(O(1),O(n^2)) 360.90/107.64 360.90/107.64 We use the processor 'polynomial interpretation' to orient 360.90/107.64 following rules strictly. 360.90/107.64 360.90/107.64 Trs: 360.90/107.64 { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) 360.90/107.64 , f(cons(nil(), y)) -> y } 360.90/107.64 360.90/107.64 The induced complexity on above rules (modulo remaining rules) is 360.90/107.64 YES(?,O(n^2)) . These rules are moved into the corresponding weak 360.90/107.64 component(s). 360.90/107.64 360.90/107.64 Sub-proof: 360.90/107.64 ---------- 360.90/107.64 We consider the following typing: 360.90/107.64 360.90/107.64 f :: a -> a 360.90/107.64 cons :: (a,a) -> a 360.90/107.64 nil :: a 360.90/107.64 copy :: (b,a,a) -> a 360.90/107.64 n :: b 360.90/107.64 0 :: b 360.90/107.64 s :: b -> b 360.90/107.64 360.90/107.64 The following argument positions are considered usable: 360.90/107.64 360.90/107.64 Uargs(f) = {1}, Uargs(cons) = {1, 2}, Uargs(copy) = {2, 3} 360.90/107.64 360.90/107.64 TcT has computed the following constructor-restricted 360.90/107.64 typedpolynomial interpretation. 360.90/107.64 360.90/107.64 [f](x1) = x1 360.90/107.64 360.90/107.64 [cons](x1, x2) = x1 + x2 360.90/107.64 360.90/107.64 [nil]() = 1 360.90/107.64 360.90/107.64 [copy](x1, x2, x3) = 2*x1 + x1*x2 + x2 + x3 360.90/107.64 360.90/107.64 [n]() = 0 360.90/107.64 360.90/107.64 [0]() = 0 360.90/107.64 360.90/107.64 [s](x1) = 2 + x1 360.90/107.64 360.90/107.64 360.90/107.64 This order satisfies the following ordering constraints. 360.90/107.64 360.90/107.64 [f(cons(f(cons(nil(), y)), z))] = 1 + y + z 360.90/107.64 > y + z 360.90/107.64 = [copy(n(), y, z)] 360.90/107.64 360.90/107.64 [f(cons(nil(), y))] = 1 + y 360.90/107.64 > y 360.90/107.64 = [y] 360.90/107.64 360.90/107.64 [copy(0(), y, z)] = y + z 360.90/107.64 >= z 360.90/107.64 = [f(z)] 360.90/107.64 360.90/107.64 [copy(s(x), y, z)] = 4 + 2*x + 3*y + x*y + z 360.90/107.64 > 2*x + x*y + 2*y + z 360.90/107.64 = [copy(x, y, cons(f(y), z))] 360.90/107.64 360.90/107.64 360.90/107.64 We return to the main proof. 360.90/107.64 360.90/107.64 We are left with following problem, upon which TcT provides the 360.90/107.64 certificate YES(O(1),O(1)). 360.90/107.64 360.90/107.64 Weak Trs: 360.90/107.64 { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) 360.90/107.64 , f(cons(nil(), y)) -> y 360.90/107.64 , copy(0(), y, z) -> f(z) 360.90/107.64 , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) } 360.90/107.64 Obligation: 360.90/107.64 runtime complexity 360.90/107.64 Answer: 360.90/107.64 YES(O(1),O(1)) 360.90/107.64 360.90/107.64 Empty rules are trivially bounded 360.90/107.64 360.90/107.64 Hurray, we answered YES(O(1),O(n^2)) 361.16/107.79 EOF