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