YES(O(1),O(n^2)) 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict Trs: 556.26/148.03 { insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r)) 556.26/148.03 , isort(Nil(), r) -> Nil() 556.26/148.03 , inssort(xs) -> isort(xs, Nil()) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 We add the following dependency tuples: 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , isort^#(Nil(), r) -> c_3() 556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5() 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs)) 556.26/148.03 , <^#(x, 0()) -> c_7() 556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 556.26/148.03 , <^#(0(), S(y)) -> c_9() } 556.26/148.03 556.26/148.03 and mark the set of starting terms. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , isort^#(Nil(), r) -> c_3() 556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5() 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs)) 556.26/148.03 , <^#(x, 0()) -> c_7() 556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 556.26/148.03 , <^#(0(), S(y)) -> c_9() } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() 556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r)) 556.26/148.03 , isort(Nil(), r) -> Nil() 556.26/148.03 , inssort(xs) -> isort(xs, Nil()) } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 We estimate the number of application of {3} by applications of 556.26/148.03 Pre({3}) = {2,4}. Here rules are labeled as follows: 556.26/148.03 556.26/148.03 DPs: 556.26/148.03 { 1: insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) 556.26/148.03 , 2: isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , 3: isort^#(Nil(), r) -> c_3() 556.26/148.03 , 4: inssort^#(xs) -> c_4(isort^#(xs, Nil())) 556.26/148.03 , 5: insert[Ite]^#(True(), x, r) -> c_5() 556.26/148.03 , 6: insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_6(insert^#(x', xs)) 556.26/148.03 , 7: <^#(x, 0()) -> c_7() 556.26/148.03 , 8: <^#(S(x), S(y)) -> c_8(<^#(x, y)) 556.26/148.03 , 9: <^#(0(), S(y)) -> c_9() } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5() 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs)) 556.26/148.03 , <^#(x, 0()) -> c_7() 556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 556.26/148.03 , <^#(0(), S(y)) -> c_9() 556.26/148.03 , isort^#(Nil(), r) -> c_3() } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() 556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r)) 556.26/148.03 , isort(Nil(), r) -> Nil() 556.26/148.03 , inssort(xs) -> isort(xs, Nil()) } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is 556.26/148.03 closed under successors. The DPs are removed. 556.26/148.03 556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5() 556.26/148.03 , <^#(x, 0()) -> c_7() 556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y)) 556.26/148.03 , <^#(0(), S(y)) -> c_9() 556.26/148.03 , isort^#(Nil(), r) -> c_3() } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_6(insert^#(x', xs)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() 556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r)) 556.26/148.03 , isort(Nil(), r) -> Nil() 556.26/148.03 , inssort(xs) -> isort(xs, Nil()) } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 Due to missing edges in the dependency-graph, the right-hand sides 556.26/148.03 of following rules could be simplified: 556.26/148.03 556.26/148.03 { insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , inssort^#(xs) -> c_3(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() 556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r)) 556.26/148.03 , isort(Nil(), r) -> Nil() 556.26/148.03 , inssort(xs) -> isort(xs, Nil()) } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 We replace rewrite rules by usable rules: 556.26/148.03 556.26/148.03 Weak Usable Rules: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 , inssort^#(xs) -> c_3(isort^#(xs, Nil())) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 Consider the dependency graph 556.26/148.03 556.26/148.03 1: insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 -->_1 insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) :4 556.26/148.03 556.26/148.03 2: isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) 556.26/148.03 -->_1 isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) :2 556.26/148.03 -->_2 insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r)) :1 556.26/148.03 556.26/148.03 3: inssort^#(xs) -> c_3(isort^#(xs, Nil())) 556.26/148.03 -->_1 isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) :2 556.26/148.03 556.26/148.03 4: insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs)) 556.26/148.03 -->_1 insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r)) :1 556.26/148.03 556.26/148.03 556.26/148.03 Following roots of the dependency graph are removed, as the 556.26/148.03 considered set of starting terms is closed under reduction with 556.26/148.03 respect to these rules (modulo compound contexts). 556.26/148.03 556.26/148.03 { inssort^#(xs) -> c_3(isort^#(xs, Nil())) } 556.26/148.03 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^2)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^2)) 556.26/148.03 556.26/148.03 We decompose the input problem according to the dependency graph 556.26/148.03 into the upper component 556.26/148.03 556.26/148.03 { isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 556.26/148.03 and lower component 556.26/148.03 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) } 556.26/148.03 556.26/148.03 Further, following extension rules are added to the lower 556.26/148.03 component. 556.26/148.03 556.26/148.03 { isort^#(Cons(x, xs), r) -> insert^#(x, r) 556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) } 556.26/148.03 556.26/148.03 TcT solves the upper component with certificate YES(O(1),O(n^1)). 556.26/148.03 556.26/148.03 Sub-proof: 556.26/148.03 ---------- 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^1)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^1)) 556.26/148.03 556.26/148.03 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 556.26/148.03 to orient following rules strictly. 556.26/148.03 556.26/148.03 DPs: 556.26/148.03 { 1: isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 Trs: 556.26/148.03 { <(x, 0()) -> False() 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 556.26/148.03 Sub-proof: 556.26/148.03 ---------- 556.26/148.03 The input was oriented with the instance of 'Small Polynomial Path 556.26/148.03 Order (PS,1-bounded)' as induced by the safe mapping 556.26/148.03 556.26/148.03 safe(insert[Ite]) = {1}, safe(insert) = {}, safe(True) = {}, 556.26/148.03 safe(S) = {1}, safe(<) = {}, safe(Cons) = {1, 2}, safe(0) = {}, 556.26/148.03 safe(False) = {}, safe(insert^#) = {}, safe(isort^#) = {2}, 556.26/148.03 safe(c_2) = {} 556.26/148.03 556.26/148.03 and precedence 556.26/148.03 556.26/148.03 insert[Ite] > insert, insert[Ite] > <, insert > <, 556.26/148.03 isort^# > insert, isort^# > < . 556.26/148.03 556.26/148.03 Following symbols are considered recursive: 556.26/148.03 556.26/148.03 {insert[Ite], isort^#} 556.26/148.03 556.26/148.03 The recursion depth is 1. 556.26/148.03 556.26/148.03 Further, following argument filtering is employed: 556.26/148.03 556.26/148.03 pi(insert[Ite]) = [1], pi(insert) = [1, 2], pi(True) = [], 556.26/148.03 pi(S) = [], pi(<) = [1, 2], pi(Cons) = [1, 2], pi(0) = [], 556.26/148.03 pi(False) = [], pi(insert^#) = [1], pi(isort^#) = [1], 556.26/148.03 pi(c_2) = [1, 2] 556.26/148.03 556.26/148.03 Usable defined function symbols are a subset of: 556.26/148.03 556.26/148.03 {insert^#, isort^#} 556.26/148.03 556.26/148.03 For your convenience, here are the satisfied ordering constraints: 556.26/148.03 556.26/148.03 pi(isort^#(Cons(x, xs), r)) = isort^#(Cons(; x, xs);) 556.26/148.03 > c_2(isort^#(xs;), insert^#(x;);) 556.26/148.03 = pi(c_2(isort^#(xs, insert(x, r)), insert^#(x, r))) 556.26/148.03 556.26/148.03 556.26/148.03 The strictly oriented rules are moved into the weak component. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Weak DPs: 556.26/148.03 { isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is 556.26/148.03 closed under successors. The DPs are removed. 556.26/148.03 556.26/148.03 { isort^#(Cons(x, xs), r) -> 556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 No rule is usable, rules are removed from the input problem. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Rules: Empty 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 Empty rules are trivially bounded 556.26/148.03 556.26/148.03 We return to the main proof. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(n^1)). 556.26/148.03 556.26/148.03 Strict DPs: 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) } 556.26/148.03 Weak DPs: 556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r) 556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(n^1)) 556.26/148.03 556.26/148.03 We use the processor 'matrix interpretation of dimension 1' to 556.26/148.03 orient following rules strictly. 556.26/148.03 556.26/148.03 DPs: 556.26/148.03 { 2: insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) 556.26/148.03 , 3: isort^#(Cons(x, xs), r) -> insert^#(x, r) } 556.26/148.03 556.26/148.03 Sub-proof: 556.26/148.03 ---------- 556.26/148.03 The following argument positions are usable: 556.26/148.03 Uargs(c_1) = {1}, Uargs(c_4) = {1} 556.26/148.03 556.26/148.03 TcT has computed the following constructor-based matrix 556.26/148.03 interpretation satisfying not(EDA). 556.26/148.03 556.26/148.03 [insert[Ite]](x1, x2, x3) = [4] x2 + [1] x3 + [4] 556.26/148.03 556.26/148.03 [insert](x1, x2) = [1] x2 + [4] 556.26/148.03 556.26/148.03 [True] = [0] 556.26/148.03 556.26/148.03 [S](x1) = [0] 556.26/148.03 556.26/148.03 [<](x1, x2) = [0] 556.26/148.03 556.26/148.03 [Cons](x1, x2) = [1] x2 + [4] 556.26/148.03 556.26/148.03 [0] = [0] 556.26/148.03 556.26/148.03 [False] = [0] 556.26/148.03 556.26/148.03 [insert^#](x1, x2) = [2] x2 + [0] 556.26/148.03 556.26/148.03 [insert[Ite]^#](x1, x2, x3) = [2] x3 + [0] 556.26/148.03 556.26/148.03 [isort^#](x1, x2) = [2] x1 + [2] x2 + [0] 556.26/148.03 556.26/148.03 [c_1](x1) = [1] x1 + [0] 556.26/148.03 556.26/148.03 [c_4](x1) = [1] x1 + [1] 556.26/148.03 556.26/148.03 The order satisfies the following ordering constraints: 556.26/148.03 556.26/148.03 [insert[Ite](True(), x, r)] = [4] x + [1] r + [4] 556.26/148.03 >= [1] r + [4] 556.26/148.03 = [Cons(x, r)] 556.26/148.03 556.26/148.03 [insert[Ite](False(), x', Cons(x, xs))] = [1] xs + [4] x' + [8] 556.26/148.03 >= [1] xs + [8] 556.26/148.03 = [Cons(x, insert(x', xs))] 556.26/148.03 556.26/148.03 [insert(S(x), r)] = [1] r + [4] 556.26/148.03 >= [1] r + [4] 556.26/148.03 = [insert[Ite](<(S(x), x), S(x), r)] 556.26/148.03 556.26/148.03 [<(x, 0())] = [0] 556.26/148.03 >= [0] 556.26/148.03 = [False()] 556.26/148.03 556.26/148.03 [<(S(x), S(y))] = [0] 556.26/148.03 >= [0] 556.26/148.03 = [<(x, y)] 556.26/148.03 556.26/148.03 [<(0(), S(y))] = [0] 556.26/148.03 >= [0] 556.26/148.03 = [True()] 556.26/148.03 556.26/148.03 [insert^#(S(x), r)] = [2] r + [0] 556.26/148.03 >= [2] r + [0] 556.26/148.03 = [c_1(insert[Ite]^#(<(S(x), x), S(x), r))] 556.26/148.03 556.26/148.03 [insert[Ite]^#(False(), x', Cons(x, xs))] = [2] xs + [8] 556.26/148.03 > [2] xs + [1] 556.26/148.03 = [c_4(insert^#(x', xs))] 556.26/148.03 556.26/148.03 [isort^#(Cons(x, xs), r)] = [2] xs + [2] r + [8] 556.26/148.03 > [2] r + [0] 556.26/148.03 = [insert^#(x, r)] 556.26/148.03 556.26/148.03 [isort^#(Cons(x, xs), r)] = [2] xs + [2] r + [8] 556.26/148.03 >= [2] xs + [2] r + [8] 556.26/148.03 = [isort^#(xs, insert(x, r))] 556.26/148.03 556.26/148.03 556.26/148.03 We return to the main proof. Consider the set of all dependency 556.26/148.03 pairs 556.26/148.03 556.26/148.03 : 556.26/148.03 { 1: insert^#(S(x), r) -> 556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , 2: insert[Ite]^#(False(), x', Cons(x, xs)) -> 556.26/148.03 c_4(insert^#(x', xs)) 556.26/148.03 , 3: isort^#(Cons(x, xs), r) -> insert^#(x, r) 556.26/148.03 , 4: isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) } 556.26/148.03 556.26/148.03 Processor 'matrix interpretation of dimension 1' induces the 556.26/148.03 complexity certificate YES(?,O(n^1)) on application of dependency 556.26/148.03 pairs {2,3}. These cover all (indirect) predecessors of dependency 556.26/148.03 pairs {1,2,3}, their number of application is equally bounded. The 556.26/148.03 dependency pairs are shifted into the weak component. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Weak DPs: 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r) 556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) } 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is 556.26/148.03 closed under successors. The DPs are removed. 556.26/148.03 556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) 556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs)) 556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r) 556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) } 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Weak Trs: 556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r) 556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs)) 556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r) 556.26/148.03 , <(x, 0()) -> False() 556.26/148.03 , <(S(x), S(y)) -> <(x, y) 556.26/148.03 , <(0(), S(y)) -> True() } 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 No rule is usable, rules are removed from the input problem. 556.26/148.03 556.26/148.03 We are left with following problem, upon which TcT provides the 556.26/148.03 certificate YES(O(1),O(1)). 556.26/148.03 556.26/148.03 Rules: Empty 556.26/148.03 Obligation: 556.26/148.03 innermost runtime complexity 556.26/148.03 Answer: 556.26/148.03 YES(O(1),O(1)) 556.26/148.03 556.26/148.03 Empty rules are trivially bounded 556.26/148.03 556.26/148.03 Hurray, we answered YES(O(1),O(n^2)) 556.26/148.07 EOF