YES(O(1),O(n^2)) 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict Trs: 34.81/15.28 { selects(x', revprefix, Cons(x, xs)) -> 34.81/15.28 Cons(Cons(x', revapp(revprefix, Cons(x, xs))), 34.81/15.28 selects(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects(x, revprefix, Nil()) -> 34.81/15.28 Cons(Cons(x, revapp(revprefix, Nil())), Nil()) 34.81/15.28 , revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest)) 34.81/15.28 , revapp(Nil(), rest) -> rest 34.81/15.28 , select(Cons(x, xs)) -> selects(x, Nil(), xs) 34.81/15.28 , select(Nil()) -> Nil() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 We add the following weak dependency pairs: 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) 34.81/15.28 , select^#(Nil()) -> c_6() } 34.81/15.28 34.81/15.28 and mark the set of starting terms. 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) 34.81/15.28 , select^#(Nil()) -> c_6() } 34.81/15.28 Strict Trs: 34.81/15.28 { selects(x', revprefix, Cons(x, xs)) -> 34.81/15.28 Cons(Cons(x', revapp(revprefix, Cons(x, xs))), 34.81/15.28 selects(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects(x, revprefix, Nil()) -> 34.81/15.28 Cons(Cons(x, revapp(revprefix, Nil())), Nil()) 34.81/15.28 , revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest)) 34.81/15.28 , revapp(Nil(), rest) -> rest 34.81/15.28 , select(Cons(x, xs)) -> selects(x, Nil(), xs) 34.81/15.28 , select(Nil()) -> Nil() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 No rule is usable, rules are removed from the input problem. 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) 34.81/15.28 , select^#(Nil()) -> c_6() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 The weightgap principle applies (using the following constant 34.81/15.28 growth matrix-interpretation) 34.81/15.28 34.81/15.28 The following argument positions are usable: 34.81/15.28 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 34.81/15.28 Uargs(c_5) = {1} 34.81/15.28 34.81/15.28 TcT has computed the following constructor-restricted matrix 34.81/15.28 interpretation. 34.81/15.28 34.81/15.28 [Cons](x1, x2) = [0] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [Nil] = [0] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [selects^#](x1, x2, x3) = [0] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 34.81/15.28 [0 1] [0 1] [2] 34.81/15.28 34.81/15.28 [revapp^#](x1, x2) = [0] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [c_2](x1) = [1 0] x1 + [1] 34.81/15.28 [0 1] [2] 34.81/15.28 34.81/15.28 [c_3](x1) = [1 0] x1 + [1] 34.81/15.28 [0 1] [0] 34.81/15.28 34.81/15.28 [c_4] = [1] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [select^#](x1) = [1] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 [c_5](x1) = [1 0] x1 + [1] 34.81/15.28 [0 1] [2] 34.81/15.28 34.81/15.28 [c_6] = [0] 34.81/15.28 [0] 34.81/15.28 34.81/15.28 The order satisfies the following ordering constraints: 34.81/15.28 34.81/15.28 [selects^#(x', revprefix, Cons(x, xs))] = [0] 34.81/15.28 [0] 34.81/15.28 ? [1] 34.81/15.28 [2] 34.81/15.28 = [c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs))] 34.81/15.28 34.81/15.28 [selects^#(x, revprefix, Nil())] = [0] 34.81/15.28 [0] 34.81/15.28 ? [1] 34.81/15.28 [2] 34.81/15.28 = [c_2(revapp^#(revprefix, Nil()))] 34.81/15.28 34.81/15.28 [revapp^#(Cons(x, xs), rest)] = [0] 34.81/15.28 [0] 34.81/15.28 ? [1] 34.81/15.28 [0] 34.81/15.28 = [c_3(revapp^#(xs, Cons(x, rest)))] 34.81/15.28 34.81/15.28 [revapp^#(Nil(), rest)] = [0] 34.81/15.28 [0] 34.81/15.28 ? [1] 34.81/15.28 [0] 34.81/15.28 = [c_4()] 34.81/15.28 34.81/15.28 [select^#(Cons(x, xs))] = [1] 34.81/15.28 [0] 34.81/15.28 ? [1] 34.81/15.28 [2] 34.81/15.28 = [c_5(selects^#(x, Nil(), xs))] 34.81/15.28 34.81/15.28 [select^#(Nil())] = [1] 34.81/15.28 [0] 34.81/15.28 > [0] 34.81/15.28 [0] 34.81/15.28 = [c_6()] 34.81/15.28 34.81/15.28 34.81/15.28 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) } 34.81/15.28 Weak DPs: { select^#(Nil()) -> c_6() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 We estimate the number of application of {4} by applications of 34.81/15.28 Pre({4}) = {1,2,3}. Here rules are labeled as follows: 34.81/15.28 34.81/15.28 DPs: 34.81/15.28 { 1: selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , 2: selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , 3: revapp^#(Cons(x, xs), rest) -> 34.81/15.28 c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , 4: revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , 5: select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) 34.81/15.28 , 6: select^#(Nil()) -> c_6() } 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) } 34.81/15.28 Weak DPs: 34.81/15.28 { revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Nil()) -> c_6() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 The following weak DPs constitute a sub-graph of the DG that is 34.81/15.28 closed under successors. The DPs are removed. 34.81/15.28 34.81/15.28 { revapp^#(Nil(), rest) -> c_4() 34.81/15.28 , select^#(Nil()) -> c_6() } 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 , select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 Consider the dependency graph 34.81/15.28 34.81/15.28 1: selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 -->_1 revapp^#(Cons(x, xs), rest) -> 34.81/15.28 c_3(revapp^#(xs, Cons(x, rest))) :3 34.81/15.28 -->_2 selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) :2 34.81/15.28 -->_2 selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) :1 34.81/15.28 34.81/15.28 2: selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) 34.81/15.28 -->_1 revapp^#(Cons(x, xs), rest) -> 34.81/15.28 c_3(revapp^#(xs, Cons(x, rest))) :3 34.81/15.28 34.81/15.28 3: revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) 34.81/15.28 -->_1 revapp^#(Cons(x, xs), rest) -> 34.81/15.28 c_3(revapp^#(xs, Cons(x, rest))) :3 34.81/15.28 34.81/15.28 4: select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) 34.81/15.28 -->_1 selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) :2 34.81/15.28 -->_1 selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) :1 34.81/15.28 34.81/15.28 34.81/15.28 Following roots of the dependency graph are removed, as the 34.81/15.28 considered set of starting terms is closed under reduction with 34.81/15.28 respect to these rules (modulo compound contexts). 34.81/15.28 34.81/15.28 { select^#(Cons(x, xs)) -> c_5(selects^#(x, Nil(), xs)) } 34.81/15.28 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^2)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2(revapp^#(revprefix, Nil())) 34.81/15.28 , revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^2)) 34.81/15.28 34.81/15.28 We use the processor 'polynomial interpretation' to orient 34.81/15.28 following rules strictly. 34.81/15.28 34.81/15.28 DPs: 34.81/15.28 { 3: revapp^#(Cons(x, xs), rest) -> 34.81/15.28 c_3(revapp^#(xs, Cons(x, rest))) } 34.81/15.28 34.81/15.28 Sub-proof: 34.81/15.28 ---------- 34.81/15.28 We consider the following typing: 34.81/15.28 34.81/15.28 Cons :: (a,b) -> b 34.81/15.28 Nil :: b 34.81/15.28 selects^# :: (a,b,b) -> c 34.81/15.28 c_1 :: (d,c) -> c 34.81/15.28 revapp^# :: (b,b) -> d 34.81/15.28 c_2 :: d -> c 34.81/15.28 c_3 :: d -> d 34.81/15.28 34.81/15.28 The following argument positions are considered usable: 34.81/15.28 34.81/15.28 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1} 34.81/15.28 34.81/15.28 TcT has computed the following constructor-restricted 34.81/15.28 typedpolynomial interpretation. 34.81/15.28 34.81/15.28 [Cons](x1, x2) = 1 + x2 34.81/15.28 34.81/15.28 [Nil]() = 0 34.81/15.28 34.81/15.28 [selects^#](x1, x2, x3) = 2*x2 + 2*x2*x3 + x3 + 2*x3^2 34.81/15.28 34.81/15.28 [c_1](x1, x2) = x1 + x2 34.81/15.28 34.81/15.28 [revapp^#](x1, x2) = 2*x1 + x2 34.81/15.28 34.81/15.28 [c_2](x1) = x1 34.81/15.28 34.81/15.28 [c_3](x1) = x1 34.81/15.28 34.81/15.28 34.81/15.28 This order satisfies the following ordering constraints. 34.81/15.28 34.81/15.28 [selects^#(x', revprefix, Cons(x, xs))] = 4*revprefix + 2*revprefix*xs + 3 + 5*xs + 2*xs^2 34.81/15.28 >= 4*revprefix + 3 + 4*xs + 2*revprefix*xs + 2*xs^2 34.81/15.28 = [c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs))] 34.81/15.28 34.81/15.28 [selects^#(x, revprefix, Nil())] = 2*revprefix 34.81/15.28 >= 2*revprefix 34.81/15.28 = [c_2(revapp^#(revprefix, Nil()))] 34.81/15.28 34.81/15.28 [revapp^#(Cons(x, xs), rest)] = 2 + 2*xs + rest 34.81/15.28 > 2*xs + 1 + rest 34.81/15.28 = [c_3(revapp^#(xs, Cons(x, rest)))] 34.81/15.28 34.81/15.28 34.81/15.28 The strictly oriented rules are moved into the weak component. 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^1)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) } 34.81/15.28 Weak DPs: 34.81/15.28 { revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^1)) 34.81/15.28 34.81/15.28 The following weak DPs constitute a sub-graph of the DG that is 34.81/15.28 closed under successors. The DPs are removed. 34.81/15.28 34.81/15.28 { revapp^#(Cons(x, xs), rest) -> c_3(revapp^#(xs, Cons(x, rest))) } 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^1)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^1)) 34.81/15.28 34.81/15.28 Due to missing edges in the dependency-graph, the right-hand sides 34.81/15.28 of following rules could be simplified: 34.81/15.28 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(revapp^#(revprefix, Cons(x, xs)), 34.81/15.28 selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> 34.81/15.28 c_2(revapp^#(revprefix, Nil())) } 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(n^1)). 34.81/15.28 34.81/15.28 Strict DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(n^1)) 34.81/15.28 34.81/15.28 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 34.81/15.28 to orient following rules strictly. 34.81/15.28 34.81/15.28 DPs: 34.81/15.28 { 1: selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , 2: selects^#(x, revprefix, Nil()) -> c_2() } 34.81/15.28 34.81/15.28 Sub-proof: 34.81/15.28 ---------- 34.81/15.28 The input was oriented with the instance of 'Small Polynomial Path 34.81/15.28 Order (PS,1-bounded)' as induced by the safe mapping 34.81/15.28 34.81/15.28 safe(Cons) = {1, 2}, safe(Nil) = {}, safe(selects^#) = {1, 2}, 34.81/15.28 safe(c_1) = {}, safe(revapp^#) = {}, safe(c_2) = {}, 34.81/15.28 safe(c_3) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {} 34.81/15.28 34.81/15.28 and precedence 34.81/15.28 34.81/15.28 empty . 34.81/15.28 34.81/15.28 Following symbols are considered recursive: 34.81/15.28 34.81/15.28 {selects^#} 34.81/15.28 34.81/15.28 The recursion depth is 1. 34.81/15.28 34.81/15.28 Further, following argument filtering is employed: 34.81/15.28 34.81/15.28 pi(Cons) = [1, 2], pi(Nil) = [], pi(selects^#) = [1, 2, 3], 34.81/15.28 pi(c_1) = [], pi(revapp^#) = [], pi(c_2) = [], pi(c_3) = [], 34.81/15.28 pi(c) = [], pi(c_1) = [1], pi(c_2) = [] 34.81/15.28 34.81/15.28 Usable defined function symbols are a subset of: 34.81/15.28 34.81/15.28 {selects^#, revapp^#} 34.81/15.28 34.81/15.28 For your convenience, here are the satisfied ordering constraints: 34.81/15.28 34.81/15.28 pi(selects^#(x', revprefix, Cons(x, xs))) = selects^#(Cons(; x, xs); x', revprefix) 34.81/15.28 > c_1(selects^#(xs; x, Cons(; x', revprefix));) 34.81/15.28 = pi(c_1(selects^#(x, Cons(x', revprefix), xs))) 34.81/15.28 34.81/15.28 pi(selects^#(x, revprefix, Nil())) = selects^#(Nil(); x, revprefix) 34.81/15.28 > c_2() 34.81/15.28 = pi(c_2()) 34.81/15.28 34.81/15.28 34.81/15.28 The strictly oriented rules are moved into the weak component. 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(1)). 34.81/15.28 34.81/15.28 Weak DPs: 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2() } 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(1)) 34.81/15.28 34.81/15.28 The following weak DPs constitute a sub-graph of the DG that is 34.81/15.28 closed under successors. The DPs are removed. 34.81/15.28 34.81/15.28 { selects^#(x', revprefix, Cons(x, xs)) -> 34.81/15.28 c_1(selects^#(x, Cons(x', revprefix), xs)) 34.81/15.28 , selects^#(x, revprefix, Nil()) -> c_2() } 34.81/15.28 34.81/15.28 We are left with following problem, upon which TcT provides the 34.81/15.28 certificate YES(O(1),O(1)). 34.81/15.28 34.81/15.28 Rules: Empty 34.81/15.28 Obligation: 34.81/15.28 innermost runtime complexity 34.81/15.28 Answer: 34.81/15.28 YES(O(1),O(1)) 34.81/15.28 34.81/15.28 Empty rules are trivially bounded 34.81/15.28 34.81/15.28 Hurray, we answered YES(O(1),O(n^2)) 35.04/15.32 EOF