YES(O(1),O(n^1)) 0.00/0.33 YES(O(1),O(n^1)) 0.00/0.33 0.00/0.33 We are left with following problem, upon which TcT provides the 0.00/0.33 certificate YES(O(1),O(n^1)). 0.00/0.33 0.00/0.33 Strict Trs: 0.00/0.33 { ordered(Cons(x', Cons(x, xs))) -> 0.00/0.33 ordered[Ite][True][Ite][True][Ite](<(x', x), 0.00/0.33 Cons(x', Cons(x, xs))) 0.00/0.33 , ordered(Cons(x, Nil())) -> True() 0.00/0.33 , ordered(Nil()) -> True() 0.00/0.33 , notEmpty(Cons(x, xs)) -> True() 0.00/0.33 , notEmpty(Nil()) -> False() 0.00/0.33 , goal(xs) -> ordered(xs) } 0.00/0.33 Weak Trs: 0.00/0.33 { <(x, 0()) -> False() 0.00/0.33 , <(S(x), S(y)) -> <(x, y) 0.00/0.33 , <(0(), S(y)) -> True() } 0.00/0.33 Obligation: 0.00/0.33 innermost runtime complexity 0.00/0.33 Answer: 0.00/0.33 YES(O(1),O(n^1)) 0.00/0.33 0.00/0.33 We add the following weak dependency pairs: 0.00/0.33 0.00/0.33 Strict DPs: 0.00/0.33 { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x)) 0.00/0.33 , ordered^#(Cons(x, Nil())) -> c_2() 0.00/0.33 , ordered^#(Nil()) -> c_3() 0.00/0.33 , notEmpty^#(Cons(x, xs)) -> c_4() 0.00/0.33 , notEmpty^#(Nil()) -> c_5() 0.00/0.33 , goal^#(xs) -> c_6(ordered^#(xs)) } 0.00/0.33 Weak DPs: 0.00/0.33 { <^#(x, 0()) -> c_7() 0.00/0.33 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 0.00/0.33 , <^#(0(), S(y)) -> c_9() } 0.00/0.33 0.00/0.33 and mark the set of starting terms. 0.00/0.33 0.00/0.33 We are left with following problem, upon which TcT provides the 0.00/0.33 certificate YES(O(1),O(n^1)). 0.00/0.33 0.00/0.33 Strict DPs: 0.00/0.33 { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x)) 0.00/0.33 , ordered^#(Cons(x, Nil())) -> c_2() 0.00/0.33 , ordered^#(Nil()) -> c_3() 0.00/0.33 , notEmpty^#(Cons(x, xs)) -> c_4() 0.00/0.33 , notEmpty^#(Nil()) -> c_5() 0.00/0.33 , goal^#(xs) -> c_6(ordered^#(xs)) } 0.00/0.33 Strict Trs: 0.00/0.33 { ordered(Cons(x', Cons(x, xs))) -> 0.00/0.33 ordered[Ite][True][Ite][True][Ite](<(x', x), 0.00/0.33 Cons(x', Cons(x, xs))) 0.00/0.33 , ordered(Cons(x, Nil())) -> True() 0.00/0.33 , ordered(Nil()) -> True() 0.00/0.33 , notEmpty(Cons(x, xs)) -> True() 0.00/0.33 , notEmpty(Nil()) -> False() 0.00/0.33 , goal(xs) -> ordered(xs) } 0.00/0.33 Weak DPs: 0.00/0.33 { <^#(x, 0()) -> c_7() 0.00/0.33 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 0.00/0.33 , <^#(0(), S(y)) -> c_9() } 0.00/0.33 Weak Trs: 0.00/0.33 { <(x, 0()) -> False() 0.00/0.33 , <(S(x), S(y)) -> <(x, y) 0.00/0.33 , <(0(), S(y)) -> True() } 0.00/0.33 Obligation: 0.00/0.33 innermost runtime complexity 0.00/0.33 Answer: 0.00/0.33 YES(O(1),O(n^1)) 0.00/0.33 0.00/0.33 No rule is usable, rules are removed from the input problem. 0.00/0.33 0.00/0.33 We are left with following problem, upon which TcT provides the 0.00/0.33 certificate YES(O(1),O(n^1)). 0.00/0.33 0.00/0.33 Strict DPs: 0.00/0.33 { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x)) 0.00/0.33 , ordered^#(Cons(x, Nil())) -> c_2() 0.00/0.33 , ordered^#(Nil()) -> c_3() 0.00/0.33 , notEmpty^#(Cons(x, xs)) -> c_4() 0.00/0.33 , notEmpty^#(Nil()) -> c_5() 0.00/0.33 , goal^#(xs) -> c_6(ordered^#(xs)) } 0.00/0.33 Weak DPs: 0.00/0.33 { <^#(x, 0()) -> c_7() 0.00/0.33 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 0.00/0.33 , <^#(0(), S(y)) -> c_9() } 0.00/0.33 Obligation: 0.00/0.33 innermost runtime complexity 0.00/0.33 Answer: 0.00/0.33 YES(O(1),O(n^1)) 0.00/0.33 0.00/0.33 The weightgap principle applies (using the following constant 0.00/0.33 growth matrix-interpretation) 0.00/0.33 0.00/0.33 The following argument positions are usable: 0.00/0.33 Uargs(c_1) = {1}, Uargs(c_6) = {1}, Uargs(c_8) = {1} 0.00/0.33 0.00/0.33 TcT has computed the following constructor-restricted matrix 0.00/0.33 interpretation. 0.00/0.33 0.00/0.33 [S](x1) = [1 0] x1 + [0] 0.00/0.33 [0 0] [0] 0.00/0.33 0.00/0.33 [Cons](x1, x2) = [1 0] x1 + [0] 0.00/0.33 [0 0] [0] 0.00/0.33 0.00/0.33 [Nil] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [0] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [ordered^#](x1) = [1] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [c_1](x1) = [1 0] x1 + [0] 0.00/0.33 [0 1] [0] 0.00/0.33 0.00/0.33 [<^#](x1, x2) = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [c_2] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [c_3] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [notEmpty^#](x1) = [1 1] x1 + [2] 0.00/0.33 [1 1] [2] 0.00/0.33 0.00/0.33 [c_4] = [1] 0.00/0.33 [1] 0.00/0.33 0.00/0.33 [c_5] = [1] 0.00/0.33 [2] 0.00/0.33 0.00/0.33 [goal^#](x1) = [2 1] x1 + [2] 0.00/0.33 [2 1] [2] 0.00/0.33 0.00/0.33 [c_6](x1) = [1 0] x1 + [0] 0.00/0.33 [0 1] [2] 0.00/0.33 0.00/0.33 [c_7] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 [c_8](x1) = [1 0] x1 + [0] 0.00/0.33 [0 1] [0] 0.00/0.33 0.00/0.33 [c_9] = [0] 0.00/0.33 [0] 0.00/0.33 0.00/0.33 The order satisfies the following ordering constraints: 0.00/0.33 0.00/0.33 [ordered^#(Cons(x', Cons(x, xs)))] = [1] 0.00/0.33 [0] 0.00/0.33 > [0] 0.00/0.33 [0] 0.00/0.33 = [c_1(<^#(x', x))] 0.00/0.33 0.00/0.33 [ordered^#(Cons(x, Nil()))] = [1] 0.00/0.33 [0] 0.00/0.33 > [0] 0.00/0.33 [0] 0.00/0.33 = [c_2()] 0.00/0.33 0.00/0.33 [ordered^#(Nil())] = [1] 0.00/0.33 [0] 0.00/0.33 > [0] 0.00/0.33 [0] 0.00/0.33 = [c_3()] 0.00/0.33 0.00/0.33 [<^#(x, 0())] = [0] 0.00/0.33 [0] 0.00/0.33 >= [0] 0.00/0.33 [0] 0.00/0.33 = [c_7()] 0.00/0.33 0.00/0.33 [<^#(S(x), S(y))] = [0] 0.00/0.33 [0] 0.00/0.33 >= [0] 0.00/0.33 [0] 0.00/0.33 = [c_8(<^#(x, y))] 0.00/0.33 0.00/0.33 [<^#(0(), S(y))] = [0] 0.00/0.33 [0] 0.00/0.33 >= [0] 0.00/0.33 [0] 0.00/0.33 = [c_9()] 0.00/0.33 0.00/0.33 [notEmpty^#(Cons(x, xs))] = [1 0] x + [2] 0.00/0.33 [1 0] [2] 0.00/0.33 > [1] 0.00/0.33 [1] 0.00/0.33 = [c_4()] 0.00/0.33 0.00/0.33 [notEmpty^#(Nil())] = [2] 0.00/0.33 [2] 0.00/0.33 > [1] 0.00/0.33 [2] 0.00/0.33 = [c_5()] 0.00/0.33 0.00/0.33 [goal^#(xs)] = [2 1] xs + [2] 0.00/0.33 [2 1] [2] 0.00/0.33 > [1] 0.00/0.33 [2] 0.00/0.33 = [c_6(ordered^#(xs))] 0.00/0.33 0.00/0.33 0.00/0.33 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 0.00/0.33 0.00/0.33 We are left with following problem, upon which TcT provides the 0.00/0.33 certificate YES(O(1),O(1)). 0.00/0.33 0.00/0.33 Weak DPs: 0.00/0.33 { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x)) 0.00/0.33 , ordered^#(Cons(x, Nil())) -> c_2() 0.00/0.33 , ordered^#(Nil()) -> c_3() 0.00/0.33 , <^#(x, 0()) -> c_7() 0.00/0.33 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 0.00/0.33 , <^#(0(), S(y)) -> c_9() 0.00/0.33 , notEmpty^#(Cons(x, xs)) -> c_4() 0.00/0.33 , notEmpty^#(Nil()) -> c_5() 0.00/0.33 , goal^#(xs) -> c_6(ordered^#(xs)) } 0.00/0.33 Obligation: 0.00/0.33 innermost runtime complexity 0.00/0.33 Answer: 0.00/0.33 YES(O(1),O(1)) 0.00/0.33 0.00/0.33 The following weak DPs constitute a sub-graph of the DG that is 0.00/0.33 closed under successors. The DPs are removed. 0.00/0.33 0.00/0.33 { ordered^#(Cons(x', Cons(x, xs))) -> c_1(<^#(x', x)) 0.00/0.33 , ordered^#(Cons(x, Nil())) -> c_2() 0.00/0.33 , ordered^#(Nil()) -> c_3() 0.00/0.33 , <^#(x, 0()) -> c_7() 0.00/0.33 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 0.00/0.33 , <^#(0(), S(y)) -> c_9() 0.00/0.33 , notEmpty^#(Cons(x, xs)) -> c_4() 0.00/0.33 , notEmpty^#(Nil()) -> c_5() 0.00/0.33 , goal^#(xs) -> c_6(ordered^#(xs)) } 0.00/0.33 0.00/0.33 We are left with following problem, upon which TcT provides the 0.00/0.33 certificate YES(O(1),O(1)). 0.00/0.33 0.00/0.33 Rules: Empty 0.00/0.33 Obligation: 0.00/0.33 innermost runtime complexity 0.00/0.33 Answer: 0.00/0.33 YES(O(1),O(1)) 0.00/0.33 0.00/0.33 Empty rules are trivially bounded 0.00/0.33 0.00/0.33 Hurray, we answered YES(O(1),O(n^1)) 0.00/0.33 EOF