YES(O(1),O(n^2)) 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) 156.56/59.87 , car(.(x, y)) -> x 156.56/59.87 , cdr(.(x, y)) -> y 156.56/59.87 , null(nil()) -> true() 156.56/59.87 , null(.(x, y)) -> false() } 156.56/59.87 Obligation: 156.56/59.87 runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 The input is overlay and right-linear. Switching to innermost 156.56/59.87 rewriting. 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) 156.56/59.87 , car(.(x, y)) -> x 156.56/59.87 , cdr(.(x, y)) -> y 156.56/59.87 , null(nil()) -> true() 156.56/59.87 , null(.(x, y)) -> false() } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 We add the following dependency tuples: 156.56/59.87 156.56/59.87 Strict DPs: 156.56/59.87 { rev^#(nil()) -> c_1() 156.56/59.87 , rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(nil(), y) -> c_3() 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) 156.56/59.87 , car^#(.(x, y)) -> c_5() 156.56/59.87 , cdr^#(.(x, y)) -> c_6() 156.56/59.87 , null^#(nil()) -> c_7() 156.56/59.87 , null^#(.(x, y)) -> c_8() } 156.56/59.87 156.56/59.87 and mark the set of starting terms. 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict DPs: 156.56/59.87 { rev^#(nil()) -> c_1() 156.56/59.87 , rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(nil(), y) -> c_3() 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) 156.56/59.87 , car^#(.(x, y)) -> c_5() 156.56/59.87 , cdr^#(.(x, y)) -> c_6() 156.56/59.87 , null^#(nil()) -> c_7() 156.56/59.87 , null^#(.(x, y)) -> c_8() } 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) 156.56/59.87 , car(.(x, y)) -> x 156.56/59.87 , cdr(.(x, y)) -> y 156.56/59.87 , null(nil()) -> true() 156.56/59.87 , null(.(x, y)) -> false() } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 We estimate the number of application of {1,3,5,6,7,8} by 156.56/59.87 applications of Pre({1,3,5,6,7,8}) = {2,4}. Here rules are labeled 156.56/59.87 as follows: 156.56/59.87 156.56/59.87 DPs: 156.56/59.87 { 1: rev^#(nil()) -> c_1() 156.56/59.87 , 2: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , 3: ++^#(nil(), y) -> c_3() 156.56/59.87 , 4: ++^#(.(x, y), z) -> c_4(++^#(y, z)) 156.56/59.87 , 5: car^#(.(x, y)) -> c_5() 156.56/59.87 , 6: cdr^#(.(x, y)) -> c_6() 156.56/59.87 , 7: null^#(nil()) -> c_7() 156.56/59.87 , 8: null^#(.(x, y)) -> c_8() } 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict DPs: 156.56/59.87 { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 Weak DPs: 156.56/59.87 { rev^#(nil()) -> c_1() 156.56/59.87 , ++^#(nil(), y) -> c_3() 156.56/59.87 , car^#(.(x, y)) -> c_5() 156.56/59.87 , cdr^#(.(x, y)) -> c_6() 156.56/59.87 , null^#(nil()) -> c_7() 156.56/59.87 , null^#(.(x, y)) -> c_8() } 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) 156.56/59.87 , car(.(x, y)) -> x 156.56/59.87 , cdr(.(x, y)) -> y 156.56/59.87 , null(nil()) -> true() 156.56/59.87 , null(.(x, y)) -> false() } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 The following weak DPs constitute a sub-graph of the DG that is 156.56/59.87 closed under successors. The DPs are removed. 156.56/59.87 156.56/59.87 { rev^#(nil()) -> c_1() 156.56/59.87 , ++^#(nil(), y) -> c_3() 156.56/59.87 , car^#(.(x, y)) -> c_5() 156.56/59.87 , cdr^#(.(x, y)) -> c_6() 156.56/59.87 , null^#(nil()) -> c_7() 156.56/59.87 , null^#(.(x, y)) -> c_8() } 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict DPs: 156.56/59.87 { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) 156.56/59.87 , car(.(x, y)) -> x 156.56/59.87 , cdr(.(x, y)) -> y 156.56/59.87 , null(nil()) -> true() 156.56/59.87 , null(.(x, y)) -> false() } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 We replace rewrite rules by usable rules: 156.56/59.87 156.56/59.87 Weak Usable Rules: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) } 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(n^2)). 156.56/59.87 156.56/59.87 Strict DPs: 156.56/59.87 { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(n^2)) 156.56/59.87 156.56/59.87 We use the processor 'polynomial interpretation' to orient 156.56/59.87 following rules strictly. 156.56/59.87 156.56/59.87 DPs: 156.56/59.87 { 1: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , 2: ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 156.56/59.87 Sub-proof: 156.56/59.87 ---------- 156.56/59.87 We consider the following typing: 156.56/59.87 156.56/59.87 rev :: c -> c 156.56/59.87 nil :: c 156.56/59.87 . :: (a,c) -> c 156.56/59.87 ++ :: (c,c) -> c 156.56/59.87 rev^# :: c -> b 156.56/59.87 c_2 :: (d,b) -> b 156.56/59.87 ++^# :: (c,c) -> d 156.56/59.87 c_4 :: d -> d 156.56/59.87 156.56/59.87 The following argument positions are considered usable: 156.56/59.87 156.56/59.87 Uargs(c_2) = {1, 2}, Uargs(c_4) = {1} 156.56/59.87 156.56/59.87 TcT has computed the following constructor-restricted 156.56/59.87 typedpolynomial interpretation. 156.56/59.87 156.56/59.87 [rev](x1) = x1 156.56/59.87 156.56/59.87 [nil]() = 0 156.56/59.87 156.56/59.87 [.](x1, x2) = 1 + x2 156.56/59.87 156.56/59.87 [++](x1, x2) = x1 + x2 156.56/59.87 156.56/59.87 [rev^#](x1) = 2*x1^2 156.56/59.87 156.56/59.87 [c_2](x1, x2) = 1 + 2*x1 + x2 156.56/59.87 156.56/59.87 [++^#](x1, x2) = 2*x1 156.56/59.87 156.56/59.87 [c_4](x1) = x1 156.56/59.87 156.56/59.87 156.56/59.87 This order satisfies the following ordering constraints. 156.56/59.87 156.56/59.87 [rev(nil())] = 156.56/59.87 >= 156.56/59.87 = [nil()] 156.56/59.87 156.56/59.87 [rev(.(x, y))] = 1 + y 156.56/59.87 >= y + 1 156.56/59.87 = [++(rev(y), .(x, nil()))] 156.56/59.87 156.56/59.87 [++(nil(), y)] = y 156.56/59.87 >= y 156.56/59.87 = [y] 156.56/59.87 156.56/59.87 [++(.(x, y), z)] = 1 + y + z 156.56/59.87 >= 1 + y + z 156.56/59.87 = [.(x, ++(y, z))] 156.56/59.87 156.56/59.87 [rev^#(.(x, y))] = 2 + 4*y + 2*y^2 156.56/59.87 > 1 + 4*y + 2*y^2 156.56/59.87 = [c_2(++^#(rev(y), .(x, nil())), rev^#(y))] 156.56/59.87 156.56/59.87 [++^#(.(x, y), z)] = 2 + 2*y 156.56/59.87 > 2*y 156.56/59.87 = [c_4(++^#(y, z))] 156.56/59.87 156.56/59.87 156.56/59.87 The strictly oriented rules are moved into the weak component. 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(1)). 156.56/59.87 156.56/59.87 Weak DPs: 156.56/59.87 { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(1)) 156.56/59.87 156.56/59.87 The following weak DPs constitute a sub-graph of the DG that is 156.56/59.87 closed under successors. The DPs are removed. 156.56/59.87 156.56/59.87 { rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())), rev^#(y)) 156.56/59.87 , ++^#(.(x, y), z) -> c_4(++^#(y, z)) } 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(1)). 156.56/59.87 156.56/59.87 Weak Trs: 156.56/59.87 { rev(nil()) -> nil() 156.56/59.87 , rev(.(x, y)) -> ++(rev(y), .(x, nil())) 156.56/59.87 , ++(nil(), y) -> y 156.56/59.87 , ++(.(x, y), z) -> .(x, ++(y, z)) } 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(1)) 156.56/59.87 156.56/59.87 No rule is usable, rules are removed from the input problem. 156.56/59.87 156.56/59.87 We are left with following problem, upon which TcT provides the 156.56/59.87 certificate YES(O(1),O(1)). 156.56/59.87 156.56/59.87 Rules: Empty 156.56/59.87 Obligation: 156.56/59.87 innermost runtime complexity 156.56/59.87 Answer: 156.56/59.87 YES(O(1),O(1)) 156.56/59.87 156.56/59.87 Empty rules are trivially bounded 156.56/59.87 156.56/59.87 Hurray, we answered YES(O(1),O(n^2)) 156.84/59.92 EOF