YES(O(1),O(n^2)) 495.28/148.08 YES(O(1),O(n^2)) 495.28/148.08 495.28/148.08 We are left with following problem, upon which TcT provides the 495.28/148.08 certificate YES(O(1),O(n^2)). 495.28/148.08 495.28/148.08 Strict Trs: 495.28/148.08 { lt(0(), s(X)) -> true() 495.28/148.08 , lt(s(X), 0()) -> false() 495.28/148.08 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.08 , append(nil(), Y) -> Y 495.28/148.08 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.08 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.08 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.08 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.08 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.08 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.08 , qsort(nil()) -> nil() 495.28/148.08 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.08 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.08 Obligation: 495.28/148.08 innermost runtime complexity 495.28/148.08 Answer: 495.28/148.08 YES(O(1),O(n^2)) 495.28/148.08 495.28/148.08 We add the following dependency tuples: 495.28/148.08 495.28/148.08 Strict DPs: 495.28/148.08 { lt^#(0(), s(X)) -> c_1() 495.28/148.08 , lt^#(s(X), 0()) -> c_2() 495.28/148.08 , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y)) 495.28/148.08 , append^#(nil(), Y) -> c_4() 495.28/148.08 , append^#(add(N, X), Y) -> c_5(append^#(X, Y)) 495.28/148.08 , split^#(N, nil()) -> c_6() 495.28/148.08 , split^#(N, add(M, Y)) -> 495.28/148.08 c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) 495.28/148.08 , f_2^#(true(), N, M, Y, X, Z) -> c_9() 495.28/148.08 , f_2^#(false(), N, M, Y, X, Z) -> c_10() 495.28/148.08 , qsort^#(nil()) -> c_11() 495.28/148.08 , qsort^#(add(N, X)) -> 495.28/148.08 c_12(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_13(append^#(qsort(Y), add(X, qsort(Z))), 495.28/148.08 qsort^#(Y), 495.28/148.08 qsort^#(Z)) } 495.28/148.08 495.28/148.08 and mark the set of starting terms. 495.28/148.08 495.28/148.08 We are left with following problem, upon which TcT provides the 495.28/148.08 certificate YES(O(1),O(n^2)). 495.28/148.08 495.28/148.08 Strict DPs: 495.28/148.08 { lt^#(0(), s(X)) -> c_1() 495.28/148.08 , lt^#(s(X), 0()) -> c_2() 495.28/148.08 , lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y)) 495.28/148.08 , append^#(nil(), Y) -> c_4() 495.28/148.08 , append^#(add(N, X), Y) -> c_5(append^#(X, Y)) 495.28/148.08 , split^#(N, nil()) -> c_6() 495.28/148.08 , split^#(N, add(M, Y)) -> 495.28/148.08 c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) 495.28/148.08 , f_2^#(true(), N, M, Y, X, Z) -> c_9() 495.28/148.08 , f_2^#(false(), N, M, Y, X, Z) -> c_10() 495.28/148.08 , qsort^#(nil()) -> c_11() 495.28/148.08 , qsort^#(add(N, X)) -> 495.28/148.08 c_12(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_13(append^#(qsort(Y), add(X, qsort(Z))), 495.28/148.08 qsort^#(Y), 495.28/148.08 qsort^#(Z)) } 495.28/148.08 Weak Trs: 495.28/148.08 { lt(0(), s(X)) -> true() 495.28/148.08 , lt(s(X), 0()) -> false() 495.28/148.08 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.08 , append(nil(), Y) -> Y 495.28/148.08 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.08 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.08 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.08 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.08 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.08 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.08 , qsort(nil()) -> nil() 495.28/148.08 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.08 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.08 Obligation: 495.28/148.08 innermost runtime complexity 495.28/148.08 Answer: 495.28/148.08 YES(O(1),O(n^2)) 495.28/148.08 495.28/148.08 We estimate the number of application of {1,2,4,6,9,10,11} by 495.28/148.08 applications of Pre({1,2,4,6,9,10,11}) = {3,5,7,8,12,13}. Here 495.28/148.08 rules are labeled as follows: 495.28/148.08 495.28/148.08 DPs: 495.28/148.08 { 1: lt^#(0(), s(X)) -> c_1() 495.28/148.08 , 2: lt^#(s(X), 0()) -> c_2() 495.28/148.08 , 3: lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y)) 495.28/148.08 , 4: append^#(nil(), Y) -> c_4() 495.28/148.08 , 5: append^#(add(N, X), Y) -> c_5(append^#(X, Y)) 495.28/148.08 , 6: split^#(N, nil()) -> c_6() 495.28/148.08 , 7: split^#(N, add(M, Y)) -> 495.28/148.08 c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , 8: f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) 495.28/148.08 , 9: f_2^#(true(), N, M, Y, X, Z) -> c_9() 495.28/148.08 , 10: f_2^#(false(), N, M, Y, X, Z) -> c_10() 495.28/148.08 , 11: qsort^#(nil()) -> c_11() 495.28/148.08 , 12: qsort^#(add(N, X)) -> 495.28/148.08 c_12(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , 13: f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_13(append^#(qsort(Y), add(X, qsort(Z))), 495.28/148.08 qsort^#(Y), 495.28/148.08 qsort^#(Z)) } 495.28/148.08 495.28/148.08 We are left with following problem, upon which TcT provides the 495.28/148.08 certificate YES(O(1),O(n^2)). 495.28/148.08 495.28/148.08 Strict DPs: 495.28/148.08 { lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y)) 495.28/148.08 , append^#(add(N, X), Y) -> c_5(append^#(X, Y)) 495.28/148.08 , split^#(N, add(M, Y)) -> 495.28/148.08 c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) 495.28/148.08 , qsort^#(add(N, X)) -> 495.28/148.08 c_12(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_13(append^#(qsort(Y), add(X, qsort(Z))), 495.28/148.08 qsort^#(Y), 495.28/148.08 qsort^#(Z)) } 495.28/148.08 Weak DPs: 495.28/148.08 { lt^#(0(), s(X)) -> c_1() 495.28/148.08 , lt^#(s(X), 0()) -> c_2() 495.28/148.08 , append^#(nil(), Y) -> c_4() 495.28/148.08 , split^#(N, nil()) -> c_6() 495.28/148.08 , f_2^#(true(), N, M, Y, X, Z) -> c_9() 495.28/148.08 , f_2^#(false(), N, M, Y, X, Z) -> c_10() 495.28/148.08 , qsort^#(nil()) -> c_11() } 495.28/148.08 Weak Trs: 495.28/148.08 { lt(0(), s(X)) -> true() 495.28/148.08 , lt(s(X), 0()) -> false() 495.28/148.08 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.08 , append(nil(), Y) -> Y 495.28/148.08 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.08 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.08 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.08 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.08 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.08 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.08 , qsort(nil()) -> nil() 495.28/148.08 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.08 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.08 Obligation: 495.28/148.08 innermost runtime complexity 495.28/148.08 Answer: 495.28/148.08 YES(O(1),O(n^2)) 495.28/148.08 495.28/148.08 The following weak DPs constitute a sub-graph of the DG that is 495.28/148.08 closed under successors. The DPs are removed. 495.28/148.08 495.28/148.08 { lt^#(0(), s(X)) -> c_1() 495.28/148.08 , lt^#(s(X), 0()) -> c_2() 495.28/148.08 , append^#(nil(), Y) -> c_4() 495.28/148.08 , split^#(N, nil()) -> c_6() 495.28/148.08 , f_2^#(true(), N, M, Y, X, Z) -> c_9() 495.28/148.08 , f_2^#(false(), N, M, Y, X, Z) -> c_10() 495.28/148.08 , qsort^#(nil()) -> c_11() } 495.28/148.08 495.28/148.08 We are left with following problem, upon which TcT provides the 495.28/148.08 certificate YES(O(1),O(n^2)). 495.28/148.08 495.28/148.08 Strict DPs: 495.28/148.08 { lt^#(s(X), s(Y)) -> c_3(lt^#(X, Y)) 495.28/148.08 , append^#(add(N, X), Y) -> c_5(append^#(X, Y)) 495.28/148.08 , split^#(N, add(M, Y)) -> 495.28/148.08 c_7(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) 495.28/148.08 , qsort^#(add(N, X)) -> 495.28/148.08 c_12(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_13(append^#(qsort(Y), add(X, qsort(Z))), 495.28/148.08 qsort^#(Y), 495.28/148.08 qsort^#(Z)) } 495.28/148.08 Weak Trs: 495.28/148.08 { lt(0(), s(X)) -> true() 495.28/148.08 , lt(s(X), 0()) -> false() 495.28/148.08 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.08 , append(nil(), Y) -> Y 495.28/148.08 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.08 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.08 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.08 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.08 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.08 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.08 , qsort(nil()) -> nil() 495.28/148.08 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.08 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.08 Obligation: 495.28/148.08 innermost runtime complexity 495.28/148.08 Answer: 495.28/148.08 YES(O(1),O(n^2)) 495.28/148.08 495.28/148.08 Due to missing edges in the dependency-graph, the right-hand sides 495.28/148.08 of following rules could be simplified: 495.28/148.08 495.28/148.08 { f_1^#(pair(X, Z), N, M, Y) -> 495.28/148.08 c_8(f_2^#(lt(N, M), N, M, Y, X, Z), lt^#(N, M)) } 495.28/148.08 495.28/148.08 We are left with following problem, upon which TcT provides the 495.28/148.08 certificate YES(O(1),O(n^2)). 495.28/148.08 495.28/148.08 Strict DPs: 495.28/148.08 { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) 495.28/148.08 , append^#(add(N, X), Y) -> c_2(append^#(X, Y)) 495.28/148.08 , split^#(N, add(M, Y)) -> 495.28/148.08 c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.08 , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) 495.28/148.08 , qsort^#(add(N, X)) -> 495.28/148.08 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.08 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.08 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.08 Weak Trs: 495.28/148.08 { lt(0(), s(X)) -> true() 495.28/148.08 , lt(s(X), 0()) -> false() 495.28/148.08 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.08 , append(nil(), Y) -> Y 495.28/148.08 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.08 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.08 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.08 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.08 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.08 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.08 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^2)) 495.28/148.09 495.28/148.09 We decompose the input problem according to the dependency graph 495.28/148.09 into the upper component 495.28/148.09 495.28/148.09 { qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.09 495.28/148.09 and lower component 495.28/148.09 495.28/148.09 { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) 495.28/148.09 , append^#(add(N, X), Y) -> c_2(append^#(X, Y)) 495.28/148.09 , split^#(N, add(M, Y)) -> 495.28/148.09 c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.09 , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) } 495.28/148.09 495.28/148.09 Further, following extension rules are added to the lower 495.28/148.09 component. 495.28/148.09 495.28/148.09 { qsort^#(add(N, X)) -> split^#(N, X) 495.28/148.09 , qsort^#(add(N, X)) -> f_3^#(split(N, X), N, X) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> append^#(qsort(Y), add(X, qsort(Z))) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Y) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Z) } 495.28/148.09 495.28/148.09 TcT solves the upper component with certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Sub-proof: 495.28/148.09 ---------- 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Strict DPs: 495.28/148.09 { qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^1)) 495.28/148.09 495.28/148.09 We use the processor 'matrix interpretation of dimension 1' to 495.28/148.09 orient following rules strictly. 495.28/148.09 495.28/148.09 DPs: 495.28/148.09 { 1: qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) } 495.28/148.09 495.28/148.09 Sub-proof: 495.28/148.09 ---------- 495.28/148.09 The following argument positions are usable: 495.28/148.09 Uargs(c_5) = {1}, Uargs(c_6) = {1, 2, 3} 495.28/148.09 495.28/148.09 TcT has computed the following constructor-based matrix 495.28/148.09 interpretation satisfying not(EDA). 495.28/148.09 495.28/148.09 [lt](x1, x2) = [0] 495.28/148.09 495.28/148.09 [0] = [0] 495.28/148.09 495.28/148.09 [s](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [true] = [0] 495.28/148.09 495.28/148.09 [false] = [0] 495.28/148.09 495.28/148.09 [append](x1, x2) = [0] 495.28/148.09 495.28/148.09 [nil] = [0] 495.28/148.09 495.28/148.09 [add](x1, x2) = [1] x2 + [1] 495.28/148.09 495.28/148.09 [split](x1, x2) = [1] x2 + [0] 495.28/148.09 495.28/148.09 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 495.28/148.09 495.28/148.09 [f_1](x1, x2, x3, x4) = [1] x1 + [1] 495.28/148.09 495.28/148.09 [f_2](x1, x2, x3, x4, x5, x6) = [1] x5 + [1] x6 + [1] 495.28/148.09 495.28/148.09 [qsort](x1) = [0] 495.28/148.09 495.28/148.09 [f_3](x1, x2, x3) = [3] x2 + [0] 495.28/148.09 495.28/148.09 [append^#](x1, x2) = [0] 495.28/148.09 495.28/148.09 [split^#](x1, x2) = [7] x1 + [7] x2 + [7] 495.28/148.09 495.28/148.09 [qsort^#](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [f_3^#](x1, x2, x3) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [c_5](x1, x2) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [c_6](x1, x2, x3) = [4] x1 + [1] x2 + [1] x3 + [0] 495.28/148.09 495.28/148.09 The order satisfies the following ordering constraints: 495.28/148.09 495.28/148.09 [lt(0(), s(X))] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [true()] 495.28/148.09 495.28/148.09 [lt(s(X), 0())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [false()] 495.28/148.09 495.28/148.09 [lt(s(X), s(Y))] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [lt(X, Y)] 495.28/148.09 495.28/148.09 [append(nil(), Y)] = [0] 495.28/148.09 ? [1] Y + [0] 495.28/148.09 = [Y] 495.28/148.09 495.28/148.09 [append(add(N, X), Y)] = [0] 495.28/148.09 ? [1] 495.28/148.09 = [add(N, append(X, Y))] 495.28/148.09 495.28/148.09 [split(N, nil())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [pair(nil(), nil())] 495.28/148.09 495.28/148.09 [split(N, add(M, Y))] = [1] Y + [1] 495.28/148.09 >= [1] Y + [1] 495.28/148.09 = [f_1(split(N, Y), N, M, Y)] 495.28/148.09 495.28/148.09 [f_1(pair(X, Z), N, M, Y)] = [1] X + [1] Z + [1] 495.28/148.09 >= [1] X + [1] Z + [1] 495.28/148.09 = [f_2(lt(N, M), N, M, Y, X, Z)] 495.28/148.09 495.28/148.09 [f_2(true(), N, M, Y, X, Z)] = [1] X + [1] Z + [1] 495.28/148.09 >= [1] X + [1] Z + [1] 495.28/148.09 = [pair(X, add(M, Z))] 495.28/148.09 495.28/148.09 [f_2(false(), N, M, Y, X, Z)] = [1] X + [1] Z + [1] 495.28/148.09 >= [1] X + [1] Z + [1] 495.28/148.09 = [pair(add(M, X), Z)] 495.28/148.09 495.28/148.09 [qsort(nil())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [nil()] 495.28/148.09 495.28/148.09 [qsort(add(N, X))] = [0] 495.28/148.09 ? [3] N + [0] 495.28/148.09 = [f_3(split(N, X), N, X)] 495.28/148.09 495.28/148.09 [f_3(pair(Y, Z), N, X)] = [3] N + [0] 495.28/148.09 >= [0] 495.28/148.09 = [append(qsort(Y), add(X, qsort(Z)))] 495.28/148.09 495.28/148.09 [qsort^#(add(N, X))] = [1] X + [1] 495.28/148.09 > [1] X + [0] 495.28/148.09 = [c_5(f_3^#(split(N, X), N, X), split^#(N, X))] 495.28/148.09 495.28/148.09 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.28/148.09 >= [1] Y + [1] Z + [0] 495.28/148.09 = [c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z))] 495.28/148.09 495.28/148.09 495.28/148.09 We return to the main proof. Consider the set of all dependency 495.28/148.09 pairs 495.28/148.09 495.28/148.09 : 495.28/148.09 { 1: qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.09 , 2: f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.09 495.28/148.09 Processor 'matrix interpretation of dimension 1' induces the 495.28/148.09 complexity certificate YES(?,O(n^1)) on application of dependency 495.28/148.09 pairs {1}. These cover all (indirect) predecessors of dependency 495.28/148.09 pairs {1,2}, their number of application is equally bounded. The 495.28/148.09 dependency pairs are shifted into the weak component. 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(1)). 495.28/148.09 495.28/148.09 Weak DPs: 495.28/148.09 { qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(1)) 495.28/148.09 495.28/148.09 The following weak DPs constitute a sub-graph of the DG that is 495.28/148.09 closed under successors. The DPs are removed. 495.28/148.09 495.28/148.09 { qsort^#(add(N, X)) -> 495.28/148.09 c_5(f_3^#(split(N, X), N, X), split^#(N, X)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z))), qsort^#(Y), qsort^#(Z)) } 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(1)). 495.28/148.09 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(1)) 495.28/148.09 495.28/148.09 No rule is usable, rules are removed from the input problem. 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(1)). 495.28/148.09 495.28/148.09 Rules: Empty 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(1)) 495.28/148.09 495.28/148.09 Empty rules are trivially bounded 495.28/148.09 495.28/148.09 We return to the main proof. 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Strict DPs: 495.28/148.09 { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) 495.28/148.09 , append^#(add(N, X), Y) -> c_2(append^#(X, Y)) 495.28/148.09 , split^#(N, add(M, Y)) -> 495.28/148.09 c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.09 , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) } 495.28/148.09 Weak DPs: 495.28/148.09 { qsort^#(add(N, X)) -> split^#(N, X) 495.28/148.09 , qsort^#(add(N, X)) -> f_3^#(split(N, X), N, X) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> append^#(qsort(Y), add(X, qsort(Z))) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Y) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Z) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^1)) 495.28/148.09 495.28/148.09 We use the processor 'matrix interpretation of dimension 1' to 495.28/148.09 orient following rules strictly. 495.28/148.09 495.28/148.09 DPs: 495.28/148.09 { 1: lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) } 495.28/148.09 495.28/148.09 Sub-proof: 495.28/148.09 ---------- 495.28/148.09 The following argument positions are usable: 495.28/148.09 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, 495.28/148.09 Uargs(c_4) = {1} 495.28/148.09 495.28/148.09 TcT has computed the following constructor-based matrix 495.28/148.09 interpretation satisfying not(EDA). 495.28/148.09 495.28/148.09 [lt](x1, x2) = [0] 495.28/148.09 495.28/148.09 [0] = [0] 495.28/148.09 495.28/148.09 [s](x1) = [1] x1 + [4] 495.28/148.09 495.28/148.09 [true] = [0] 495.28/148.09 495.28/148.09 [false] = [0] 495.28/148.09 495.28/148.09 [append](x1, x2) = [0] 495.28/148.09 495.28/148.09 [nil] = [0] 495.28/148.09 495.28/148.09 [add](x1, x2) = [1] x1 + [1] x2 + [0] 495.28/148.09 495.28/148.09 [split](x1, x2) = [1] x2 + [0] 495.28/148.09 495.28/148.09 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 495.28/148.09 495.28/148.09 [f_1](x1, x2, x3, x4) = [1] x1 + [1] x3 + [0] 495.28/148.09 495.28/148.09 [f_2](x1, x2, x3, x4, x5, x6) = [1] x3 + [1] x5 + [1] x6 + [0] 495.28/148.09 495.28/148.09 [qsort](x1) = [0] 495.28/148.09 495.28/148.09 [f_3](x1, x2, x3) = [7] x2 + [0] 495.28/148.09 495.28/148.09 [lt^#](x1, x2) = [1] x2 + [0] 495.28/148.09 495.28/148.09 [append^#](x1, x2) = [0] 495.28/148.09 495.28/148.09 [split^#](x1, x2) = [1] x2 + [0] 495.28/148.09 495.28/148.09 [f_1^#](x1, x2, x3, x4) = [1] x3 + [0] 495.28/148.09 495.28/148.09 [qsort^#](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [f_3^#](x1, x2, x3) = [1] x1 + [1] x2 + [0] 495.28/148.09 495.28/148.09 [c_1](x1) = [1] x1 + [1] 495.28/148.09 495.28/148.09 [c_2](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [c_3](x1, x2) = [1] x1 + [1] x2 + [0] 495.28/148.09 495.28/148.09 [c_4](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 The order satisfies the following ordering constraints: 495.28/148.09 495.28/148.09 [lt(0(), s(X))] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [true()] 495.28/148.09 495.28/148.09 [lt(s(X), 0())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [false()] 495.28/148.09 495.28/148.09 [lt(s(X), s(Y))] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [lt(X, Y)] 495.28/148.09 495.28/148.09 [append(nil(), Y)] = [0] 495.28/148.09 ? [1] Y + [0] 495.28/148.09 = [Y] 495.28/148.09 495.28/148.09 [append(add(N, X), Y)] = [0] 495.28/148.09 ? [1] N + [0] 495.28/148.09 = [add(N, append(X, Y))] 495.28/148.09 495.28/148.09 [split(N, nil())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [pair(nil(), nil())] 495.28/148.09 495.28/148.09 [split(N, add(M, Y))] = [1] Y + [1] M + [0] 495.28/148.09 >= [1] Y + [1] M + [0] 495.28/148.09 = [f_1(split(N, Y), N, M, Y)] 495.28/148.09 495.28/148.09 [f_1(pair(X, Z), N, M, Y)] = [1] X + [1] M + [1] Z + [0] 495.28/148.09 >= [1] X + [1] M + [1] Z + [0] 495.28/148.09 = [f_2(lt(N, M), N, M, Y, X, Z)] 495.28/148.09 495.28/148.09 [f_2(true(), N, M, Y, X, Z)] = [1] X + [1] M + [1] Z + [0] 495.28/148.09 >= [1] X + [1] M + [1] Z + [0] 495.28/148.09 = [pair(X, add(M, Z))] 495.28/148.09 495.28/148.09 [f_2(false(), N, M, Y, X, Z)] = [1] X + [1] M + [1] Z + [0] 495.28/148.09 >= [1] X + [1] M + [1] Z + [0] 495.28/148.09 = [pair(add(M, X), Z)] 495.28/148.09 495.28/148.09 [qsort(nil())] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [nil()] 495.28/148.09 495.28/148.09 [qsort(add(N, X))] = [0] 495.28/148.09 ? [7] N + [0] 495.28/148.09 = [f_3(split(N, X), N, X)] 495.28/148.09 495.28/148.09 [f_3(pair(Y, Z), N, X)] = [7] N + [0] 495.28/148.09 >= [0] 495.28/148.09 = [append(qsort(Y), add(X, qsort(Z)))] 495.28/148.09 495.28/148.09 [lt^#(s(X), s(Y))] = [1] Y + [4] 495.28/148.09 > [1] Y + [1] 495.28/148.09 = [c_1(lt^#(X, Y))] 495.28/148.09 495.28/148.09 [append^#(add(N, X), Y)] = [0] 495.28/148.09 >= [0] 495.28/148.09 = [c_2(append^#(X, Y))] 495.28/148.09 495.28/148.09 [split^#(N, add(M, Y))] = [1] Y + [1] M + [0] 495.28/148.09 >= [1] Y + [1] M + [0] 495.28/148.09 = [c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))] 495.28/148.09 495.28/148.09 [f_1^#(pair(X, Z), N, M, Y)] = [1] M + [0] 495.28/148.09 >= [1] M + [0] 495.28/148.09 = [c_4(lt^#(N, M))] 495.28/148.09 495.28/148.09 [qsort^#(add(N, X))] = [1] X + [1] N + [0] 495.28/148.09 >= [1] X + [0] 495.28/148.09 = [split^#(N, X)] 495.28/148.09 495.28/148.09 [qsort^#(add(N, X))] = [1] X + [1] N + [0] 495.28/148.09 >= [1] X + [1] N + [0] 495.28/148.09 = [f_3^#(split(N, X), N, X)] 495.28/148.09 495.28/148.09 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] N + [1] Z + [0] 495.28/148.09 >= [0] 495.28/148.09 = [append^#(qsort(Y), add(X, qsort(Z)))] 495.28/148.09 495.28/148.09 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] N + [1] Z + [0] 495.28/148.09 >= [1] Y + [0] 495.28/148.09 = [qsort^#(Y)] 495.28/148.09 495.28/148.09 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] N + [1] Z + [0] 495.28/148.09 >= [1] Z + [0] 495.28/148.09 = [qsort^#(Z)] 495.28/148.09 495.28/148.09 495.28/148.09 The strictly oriented rules are moved into the weak component. 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Strict DPs: 495.28/148.09 { append^#(add(N, X), Y) -> c_2(append^#(X, Y)) 495.28/148.09 , split^#(N, add(M, Y)) -> 495.28/148.09 c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.09 , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) } 495.28/148.09 Weak DPs: 495.28/148.09 { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) 495.28/148.09 , qsort^#(add(N, X)) -> split^#(N, X) 495.28/148.09 , qsort^#(add(N, X)) -> f_3^#(split(N, X), N, X) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> append^#(qsort(Y), add(X, qsort(Z))) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Y) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Z) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^1)) 495.28/148.09 495.28/148.09 The following weak DPs constitute a sub-graph of the DG that is 495.28/148.09 closed under successors. The DPs are removed. 495.28/148.09 495.28/148.09 { lt^#(s(X), s(Y)) -> c_1(lt^#(X, Y)) } 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Strict DPs: 495.28/148.09 { append^#(add(N, X), Y) -> c_2(append^#(X, Y)) 495.28/148.09 , split^#(N, add(M, Y)) -> 495.28/148.09 c_3(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.09 , f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) } 495.28/148.09 Weak DPs: 495.28/148.09 { qsort^#(add(N, X)) -> split^#(N, X) 495.28/148.09 , qsort^#(add(N, X)) -> f_3^#(split(N, X), N, X) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> append^#(qsort(Y), add(X, qsort(Z))) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Y) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> qsort^#(Z) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^1)) 495.28/148.09 495.28/148.09 Due to missing edges in the dependency-graph, the right-hand sides 495.28/148.09 of following rules could be simplified: 495.28/148.09 495.28/148.09 { f_1^#(pair(X, Z), N, M, Y) -> c_4(lt^#(N, M)) } 495.28/148.09 495.28/148.09 We are left with following problem, upon which TcT provides the 495.28/148.09 certificate YES(O(1),O(n^1)). 495.28/148.09 495.28/148.09 Strict DPs: 495.28/148.09 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.28/148.09 , split^#(N, add(M, Y)) -> 495.28/148.09 c_2(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) 495.28/148.09 , f_1^#(pair(X, Z), N, M, Y) -> c_3() } 495.28/148.09 Weak DPs: 495.28/148.09 { qsort^#(add(N, X)) -> c_4(split^#(N, X)) 495.28/148.09 , qsort^#(add(N, X)) -> c_5(f_3^#(split(N, X), N, X)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> 495.28/148.09 c_6(append^#(qsort(Y), add(X, qsort(Z)))) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Y)) 495.28/148.09 , f_3^#(pair(Y, Z), N, X) -> c_8(qsort^#(Z)) } 495.28/148.09 Weak Trs: 495.28/148.09 { lt(0(), s(X)) -> true() 495.28/148.09 , lt(s(X), 0()) -> false() 495.28/148.09 , lt(s(X), s(Y)) -> lt(X, Y) 495.28/148.09 , append(nil(), Y) -> Y 495.28/148.09 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.28/148.09 , split(N, nil()) -> pair(nil(), nil()) 495.28/148.09 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.28/148.09 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.28/148.09 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.28/148.09 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.28/148.09 , qsort(nil()) -> nil() 495.28/148.09 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.28/148.09 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.28/148.09 Obligation: 495.28/148.09 innermost runtime complexity 495.28/148.09 Answer: 495.28/148.09 YES(O(1),O(n^1)) 495.28/148.09 495.28/148.09 We use the processor 'matrix interpretation of dimension 1' to 495.28/148.09 orient following rules strictly. 495.28/148.09 495.28/148.09 DPs: 495.28/148.09 { 3: f_1^#(pair(X, Z), N, M, Y) -> c_3() 495.28/148.09 , 4: qsort^#(add(N, X)) -> c_4(split^#(N, X)) } 495.28/148.09 495.28/148.09 Sub-proof: 495.28/148.09 ---------- 495.28/148.09 The following argument positions are usable: 495.28/148.09 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_4) = {1}, 495.28/148.09 Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, 495.28/148.09 Uargs(c_8) = {1} 495.28/148.09 495.28/148.09 TcT has computed the following constructor-based matrix 495.28/148.09 interpretation satisfying not(EDA). 495.28/148.09 495.28/148.09 [lt](x1, x2) = [1] 495.28/148.09 495.28/148.09 [0] = [0] 495.28/148.09 495.28/148.09 [s](x1) = [1] x1 + [0] 495.28/148.09 495.28/148.09 [true] = [1] 495.28/148.09 495.28/148.09 [false] = [1] 495.28/148.09 495.28/148.10 [append](x1, x2) = [0] 495.28/148.10 495.28/148.10 [nil] = [0] 495.28/148.10 495.28/148.10 [add](x1, x2) = [1] x2 + [2] 495.28/148.10 495.28/148.10 [split](x1, x2) = [1] x2 + [0] 495.28/148.10 495.28/148.10 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 495.28/148.10 495.28/148.10 [f_1](x1, x2, x3, x4) = [1] x1 + [2] 495.28/148.10 495.28/148.10 [f_2](x1, x2, x3, x4, x5, x6) = [1] x1 + [1] x5 + [1] x6 + [1] 495.28/148.10 495.28/148.10 [qsort](x1) = [0] 495.28/148.10 495.28/148.10 [f_3](x1, x2, x3) = [3] x2 + [0] 495.28/148.10 495.28/148.10 [lt^#](x1, x2) = [7] x1 + [7] x2 + [0] 495.28/148.10 495.28/148.10 [append^#](x1, x2) = [0] 495.28/148.10 495.28/148.10 [split^#](x1, x2) = [1] x2 + [0] 495.28/148.10 495.28/148.10 [f_1^#](x1, x2, x3, x4) = [1] 495.28/148.10 495.28/148.10 [qsort^#](x1) = [1] x1 + [0] 495.28/148.10 495.28/148.10 [f_3^#](x1, x2, x3) = [1] x1 + [0] 495.28/148.10 495.28/148.10 [c_1](x1) = [7] x1 + [0] 495.28/148.10 495.28/148.10 [c_2](x1) = [7] x1 + [0] 495.28/148.10 495.28/148.10 [c_3](x1, x2) = [7] x1 + [7] x2 + [0] 495.28/148.10 495.28/148.10 [c_4](x1) = [7] x1 + [0] 495.28/148.10 495.28/148.10 [c] = [0] 495.28/148.10 495.28/148.10 [c_1](x1) = [4] x1 + [0] 495.28/148.10 495.28/148.10 [c_2](x1, x2) = [2] x1 + [1] x2 + [0] 495.28/148.10 495.28/148.10 [c_3] = [0] 495.28/148.10 495.28/148.10 [c_4](x1) = [1] x1 + [1] 495.28/148.10 495.28/148.10 [c_5](x1) = [1] x1 + [2] 495.28/148.10 495.28/148.10 [c_6](x1) = [2] x1 + [0] 495.28/148.10 495.28/148.10 [c_7](x1) = [1] x1 + [0] 495.28/148.10 495.28/148.10 [c_8](x1) = [1] x1 + [0] 495.28/148.10 495.28/148.10 The order satisfies the following ordering constraints: 495.28/148.10 495.28/148.10 [lt(0(), s(X))] = [1] 495.28/148.10 >= [1] 495.28/148.10 = [true()] 495.28/148.10 495.28/148.10 [lt(s(X), 0())] = [1] 495.28/148.10 >= [1] 495.28/148.10 = [false()] 495.28/148.10 495.28/148.10 [lt(s(X), s(Y))] = [1] 495.28/148.10 >= [1] 495.28/148.10 = [lt(X, Y)] 495.28/148.10 495.28/148.10 [append(nil(), Y)] = [0] 495.28/148.10 ? [1] Y + [0] 495.28/148.10 = [Y] 495.28/148.10 495.28/148.10 [append(add(N, X), Y)] = [0] 495.28/148.10 ? [2] 495.28/148.10 = [add(N, append(X, Y))] 495.28/148.10 495.28/148.10 [split(N, nil())] = [0] 495.28/148.10 >= [0] 495.28/148.10 = [pair(nil(), nil())] 495.28/148.10 495.28/148.10 [split(N, add(M, Y))] = [1] Y + [2] 495.28/148.10 >= [1] Y + [2] 495.28/148.10 = [f_1(split(N, Y), N, M, Y)] 495.28/148.10 495.28/148.10 [f_1(pair(X, Z), N, M, Y)] = [1] X + [1] Z + [2] 495.28/148.10 >= [1] X + [1] Z + [2] 495.28/148.10 = [f_2(lt(N, M), N, M, Y, X, Z)] 495.28/148.10 495.28/148.10 [f_2(true(), N, M, Y, X, Z)] = [1] X + [1] Z + [2] 495.28/148.10 >= [1] X + [1] Z + [2] 495.28/148.10 = [pair(X, add(M, Z))] 495.28/148.10 495.28/148.10 [f_2(false(), N, M, Y, X, Z)] = [1] X + [1] Z + [2] 495.28/148.10 >= [1] X + [1] Z + [2] 495.28/148.10 = [pair(add(M, X), Z)] 495.28/148.10 495.28/148.10 [qsort(nil())] = [0] 495.28/148.10 >= [0] 495.28/148.10 = [nil()] 495.28/148.10 495.28/148.10 [qsort(add(N, X))] = [0] 495.28/148.10 ? [3] N + [0] 495.28/148.10 = [f_3(split(N, X), N, X)] 495.28/148.10 495.28/148.10 [f_3(pair(Y, Z), N, X)] = [3] N + [0] 495.28/148.10 >= [0] 495.52/148.10 = [append(qsort(Y), add(X, qsort(Z)))] 495.52/148.10 495.52/148.10 [append^#(add(N, X), Y)] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [c_1(append^#(X, Y))] 495.52/148.10 495.52/148.10 [split^#(N, add(M, Y))] = [1] Y + [2] 495.52/148.10 >= [1] Y + [2] 495.52/148.10 = [c_2(f_1^#(split(N, Y), N, M, Y), split^#(N, Y))] 495.52/148.10 495.52/148.10 [f_1^#(pair(X, Z), N, M, Y)] = [1] 495.52/148.10 > [0] 495.52/148.10 = [c_3()] 495.52/148.10 495.52/148.10 [qsort^#(add(N, X))] = [1] X + [2] 495.52/148.10 > [1] X + [1] 495.52/148.10 = [c_4(split^#(N, X))] 495.52/148.10 495.52/148.10 [qsort^#(add(N, X))] = [1] X + [2] 495.52/148.10 >= [1] X + [2] 495.52/148.10 = [c_5(f_3^#(split(N, X), N, X))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [0] 495.52/148.10 = [c_6(append^#(qsort(Y), add(X, qsort(Z))))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [1] Y + [0] 495.52/148.10 = [c_7(qsort^#(Y))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [1] Z + [0] 495.52/148.10 = [c_8(qsort^#(Z))] 495.52/148.10 495.52/148.10 495.52/148.10 The strictly oriented rules are moved into the weak component. 495.52/148.10 495.52/148.10 We are left with following problem, upon which TcT provides the 495.52/148.10 certificate YES(O(1),O(n^1)). 495.52/148.10 495.52/148.10 Strict DPs: 495.52/148.10 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.10 , split^#(N, add(M, Y)) -> 495.52/148.10 c_2(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) } 495.52/148.10 Weak DPs: 495.52/148.10 { f_1^#(pair(X, Z), N, M, Y) -> c_3() 495.52/148.10 , qsort^#(add(N, X)) -> c_4(split^#(N, X)) 495.52/148.10 , qsort^#(add(N, X)) -> c_5(f_3^#(split(N, X), N, X)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_6(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Y)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_8(qsort^#(Z)) } 495.52/148.10 Weak Trs: 495.52/148.10 { lt(0(), s(X)) -> true() 495.52/148.10 , lt(s(X), 0()) -> false() 495.52/148.10 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.10 , append(nil(), Y) -> Y 495.52/148.10 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.10 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.10 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.10 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.10 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.10 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.10 , qsort(nil()) -> nil() 495.52/148.10 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.10 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.10 Obligation: 495.52/148.10 innermost runtime complexity 495.52/148.10 Answer: 495.52/148.10 YES(O(1),O(n^1)) 495.52/148.10 495.52/148.10 The following weak DPs constitute a sub-graph of the DG that is 495.52/148.10 closed under successors. The DPs are removed. 495.52/148.10 495.52/148.10 { f_1^#(pair(X, Z), N, M, Y) -> c_3() } 495.52/148.10 495.52/148.10 We are left with following problem, upon which TcT provides the 495.52/148.10 certificate YES(O(1),O(n^1)). 495.52/148.10 495.52/148.10 Strict DPs: 495.52/148.10 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.10 , split^#(N, add(M, Y)) -> 495.52/148.10 c_2(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) } 495.52/148.10 Weak DPs: 495.52/148.10 { qsort^#(add(N, X)) -> c_4(split^#(N, X)) 495.52/148.10 , qsort^#(add(N, X)) -> c_5(f_3^#(split(N, X), N, X)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_6(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Y)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_8(qsort^#(Z)) } 495.52/148.10 Weak Trs: 495.52/148.10 { lt(0(), s(X)) -> true() 495.52/148.10 , lt(s(X), 0()) -> false() 495.52/148.10 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.10 , append(nil(), Y) -> Y 495.52/148.10 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.10 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.10 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.10 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.10 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.10 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.10 , qsort(nil()) -> nil() 495.52/148.10 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.10 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.10 Obligation: 495.52/148.10 innermost runtime complexity 495.52/148.10 Answer: 495.52/148.10 YES(O(1),O(n^1)) 495.52/148.10 495.52/148.10 Due to missing edges in the dependency-graph, the right-hand sides 495.52/148.10 of following rules could be simplified: 495.52/148.10 495.52/148.10 { split^#(N, add(M, Y)) -> 495.52/148.10 c_2(f_1^#(split(N, Y), N, M, Y), split^#(N, Y)) } 495.52/148.10 495.52/148.10 We are left with following problem, upon which TcT provides the 495.52/148.10 certificate YES(O(1),O(n^1)). 495.52/148.10 495.52/148.10 Strict DPs: 495.52/148.10 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.10 , split^#(N, add(M, Y)) -> c_2(split^#(N, Y)) } 495.52/148.10 Weak DPs: 495.52/148.10 { qsort^#(add(N, X)) -> c_3(split^#(N, X)) 495.52/148.10 , qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.10 Weak Trs: 495.52/148.10 { lt(0(), s(X)) -> true() 495.52/148.10 , lt(s(X), 0()) -> false() 495.52/148.10 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.10 , append(nil(), Y) -> Y 495.52/148.10 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.10 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.10 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.10 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.10 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.10 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.10 , qsort(nil()) -> nil() 495.52/148.10 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.10 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.10 Obligation: 495.52/148.10 innermost runtime complexity 495.52/148.10 Answer: 495.52/148.10 YES(O(1),O(n^1)) 495.52/148.10 495.52/148.10 We use the processor 'matrix interpretation of dimension 1' to 495.52/148.10 orient following rules strictly. 495.52/148.10 495.52/148.10 DPs: 495.52/148.10 { 2: split^#(N, add(M, Y)) -> c_2(split^#(N, Y)) 495.52/148.10 , 4: qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) } 495.52/148.10 495.52/148.10 Sub-proof: 495.52/148.10 ---------- 495.52/148.10 The following argument positions are usable: 495.52/148.10 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 495.52/148.10 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 495.52/148.10 Uargs(c_7) = {1} 495.52/148.10 495.52/148.10 TcT has computed the following constructor-based matrix 495.52/148.10 interpretation satisfying not(EDA). 495.52/148.10 495.52/148.10 [lt](x1, x2) = [0] 495.52/148.10 495.52/148.10 [0] = [0] 495.52/148.10 495.52/148.10 [s](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [true] = [0] 495.52/148.10 495.52/148.10 [false] = [0] 495.52/148.10 495.52/148.10 [append](x1, x2) = [0] 495.52/148.10 495.52/148.10 [nil] = [0] 495.52/148.10 495.52/148.10 [add](x1, x2) = [1] x2 + [4] 495.52/148.10 495.52/148.10 [split](x1, x2) = [1] x2 + [0] 495.52/148.10 495.52/148.10 [pair](x1, x2) = [1] x1 + [1] x2 + [0] 495.52/148.10 495.52/148.10 [f_1](x1, x2, x3, x4) = [1] x1 + [4] 495.52/148.10 495.52/148.10 [f_2](x1, x2, x3, x4, x5, x6) = [1] x5 + [1] x6 + [4] 495.52/148.10 495.52/148.10 [qsort](x1) = [0] 495.52/148.10 495.52/148.10 [f_3](x1, x2, x3) = [7] x2 + [0] 495.52/148.10 495.52/148.10 [lt^#](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [append^#](x1, x2) = [0] 495.52/148.10 495.52/148.10 [split^#](x1, x2) = [1] x2 + [4] 495.52/148.10 495.52/148.10 [f_1^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] 495.52/148.10 495.52/148.10 [qsort^#](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [f_3^#](x1, x2, x3) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_3](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c] = [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [c_3] = [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_5](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_6](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_7](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_8](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c] = [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [2] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1) = [1] x1 + [1] 495.52/148.10 495.52/148.10 [c_3](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [1] x1 + [3] 495.52/148.10 495.52/148.10 [c_5](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_6](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_7](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 The order satisfies the following ordering constraints: 495.52/148.10 495.52/148.10 [lt(0(), s(X))] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [true()] 495.52/148.10 495.52/148.10 [lt(s(X), 0())] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [false()] 495.52/148.10 495.52/148.10 [lt(s(X), s(Y))] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [lt(X, Y)] 495.52/148.10 495.52/148.10 [append(nil(), Y)] = [0] 495.52/148.10 ? [1] Y + [0] 495.52/148.10 = [Y] 495.52/148.10 495.52/148.10 [append(add(N, X), Y)] = [0] 495.52/148.10 ? [4] 495.52/148.10 = [add(N, append(X, Y))] 495.52/148.10 495.52/148.10 [split(N, nil())] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [pair(nil(), nil())] 495.52/148.10 495.52/148.10 [split(N, add(M, Y))] = [1] Y + [4] 495.52/148.10 >= [1] Y + [4] 495.52/148.10 = [f_1(split(N, Y), N, M, Y)] 495.52/148.10 495.52/148.10 [f_1(pair(X, Z), N, M, Y)] = [1] X + [1] Z + [4] 495.52/148.10 >= [1] X + [1] Z + [4] 495.52/148.10 = [f_2(lt(N, M), N, M, Y, X, Z)] 495.52/148.10 495.52/148.10 [f_2(true(), N, M, Y, X, Z)] = [1] X + [1] Z + [4] 495.52/148.10 >= [1] X + [1] Z + [4] 495.52/148.10 = [pair(X, add(M, Z))] 495.52/148.10 495.52/148.10 [f_2(false(), N, M, Y, X, Z)] = [1] X + [1] Z + [4] 495.52/148.10 >= [1] X + [1] Z + [4] 495.52/148.10 = [pair(add(M, X), Z)] 495.52/148.10 495.52/148.10 [qsort(nil())] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [nil()] 495.52/148.10 495.52/148.10 [qsort(add(N, X))] = [0] 495.52/148.10 ? [7] N + [0] 495.52/148.10 = [f_3(split(N, X), N, X)] 495.52/148.10 495.52/148.10 [f_3(pair(Y, Z), N, X)] = [7] N + [0] 495.52/148.10 >= [0] 495.52/148.10 = [append(qsort(Y), add(X, qsort(Z)))] 495.52/148.10 495.52/148.10 [append^#(add(N, X), Y)] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [c_1(append^#(X, Y))] 495.52/148.10 495.52/148.10 [split^#(N, add(M, Y))] = [1] Y + [8] 495.52/148.10 > [1] Y + [5] 495.52/148.10 = [c_2(split^#(N, Y))] 495.52/148.10 495.52/148.10 [qsort^#(add(N, X))] = [1] X + [4] 495.52/148.10 >= [1] X + [4] 495.52/148.10 = [c_3(split^#(N, X))] 495.52/148.10 495.52/148.10 [qsort^#(add(N, X))] = [1] X + [4] 495.52/148.10 > [1] X + [3] 495.52/148.10 = [c_4(f_3^#(split(N, X), N, X))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [0] 495.52/148.10 = [c_5(append^#(qsort(Y), add(X, qsort(Z))))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [1] Y + [0] 495.52/148.10 = [c_6(qsort^#(Y))] 495.52/148.10 495.52/148.10 [f_3^#(pair(Y, Z), N, X)] = [1] Y + [1] Z + [0] 495.52/148.10 >= [1] Z + [0] 495.52/148.10 = [c_7(qsort^#(Z))] 495.52/148.10 495.52/148.10 495.52/148.10 We return to the main proof. Consider the set of all dependency 495.52/148.10 pairs 495.52/148.10 495.52/148.10 : 495.52/148.10 { 1: append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.10 , 2: split^#(N, add(M, Y)) -> c_2(split^#(N, Y)) 495.52/148.10 , 3: qsort^#(add(N, X)) -> c_3(split^#(N, X)) 495.52/148.10 , 4: qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.10 , 5: f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , 6: f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.10 , 7: f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.10 495.52/148.10 Processor 'matrix interpretation of dimension 1' induces the 495.52/148.10 complexity certificate YES(?,O(n^1)) on application of dependency 495.52/148.10 pairs {2,4}. These cover all (indirect) predecessors of dependency 495.52/148.10 pairs {2,3,4,5,6,7}, their number of application is equally 495.52/148.10 bounded. The dependency pairs are shifted into the weak component. 495.52/148.10 495.52/148.10 We are left with following problem, upon which TcT provides the 495.52/148.10 certificate YES(O(1),O(n^1)). 495.52/148.10 495.52/148.10 Strict DPs: { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) } 495.52/148.10 Weak DPs: 495.52/148.10 { split^#(N, add(M, Y)) -> c_2(split^#(N, Y)) 495.52/148.10 , qsort^#(add(N, X)) -> c_3(split^#(N, X)) 495.52/148.10 , qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.10 Weak Trs: 495.52/148.10 { lt(0(), s(X)) -> true() 495.52/148.10 , lt(s(X), 0()) -> false() 495.52/148.10 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.10 , append(nil(), Y) -> Y 495.52/148.10 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.10 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.10 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.10 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.10 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.10 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.10 , qsort(nil()) -> nil() 495.52/148.10 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.10 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.10 Obligation: 495.52/148.10 innermost runtime complexity 495.52/148.10 Answer: 495.52/148.10 YES(O(1),O(n^1)) 495.52/148.10 495.52/148.10 The following weak DPs constitute a sub-graph of the DG that is 495.52/148.10 closed under successors. The DPs are removed. 495.52/148.10 495.52/148.10 { split^#(N, add(M, Y)) -> c_2(split^#(N, Y)) 495.52/148.10 , qsort^#(add(N, X)) -> c_3(split^#(N, X)) } 495.52/148.10 495.52/148.10 We are left with following problem, upon which TcT provides the 495.52/148.10 certificate YES(O(1),O(n^1)). 495.52/148.10 495.52/148.10 Strict DPs: { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) } 495.52/148.10 Weak DPs: 495.52/148.10 { qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.10 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.10 Weak Trs: 495.52/148.10 { lt(0(), s(X)) -> true() 495.52/148.10 , lt(s(X), 0()) -> false() 495.52/148.10 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.10 , append(nil(), Y) -> Y 495.52/148.10 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.10 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.10 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.10 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.10 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.10 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.10 , qsort(nil()) -> nil() 495.52/148.10 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.10 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.10 Obligation: 495.52/148.10 innermost runtime complexity 495.52/148.10 Answer: 495.52/148.10 YES(O(1),O(n^1)) 495.52/148.10 495.52/148.10 We use the processor 'matrix interpretation of dimension 1' to 495.52/148.10 orient following rules strictly. 495.52/148.10 495.52/148.10 DPs: 495.52/148.10 { 1: append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.10 , 3: f_3^#(pair(Y, Z), N, X) -> 495.52/148.10 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.10 , 4: f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.10 , 5: f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.10 495.52/148.10 Sub-proof: 495.52/148.10 ---------- 495.52/148.10 The following argument positions are usable: 495.52/148.10 Uargs(c_1) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, 495.52/148.10 Uargs(c_6) = {1}, Uargs(c_7) = {1} 495.52/148.10 495.52/148.10 TcT has computed the following constructor-based matrix 495.52/148.10 interpretation satisfying not(EDA). 495.52/148.10 495.52/148.10 [lt](x1, x2) = [0] 495.52/148.10 495.52/148.10 [0] = [0] 495.52/148.10 495.52/148.10 [s](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [true] = [0] 495.52/148.10 495.52/148.10 [false] = [0] 495.52/148.10 495.52/148.10 [append](x1, x2) = [1] x1 + [1] x2 + [0] 495.52/148.10 495.52/148.10 [nil] = [0] 495.52/148.10 495.52/148.10 [add](x1, x2) = [1] x2 + [1] 495.52/148.10 495.52/148.10 [split](x1, x2) = [1] x2 + [1] 495.52/148.10 495.52/148.10 [pair](x1, x2) = [1] x1 + [1] x2 + [1] 495.52/148.10 495.52/148.10 [f_1](x1, x2, x3, x4) = [1] x1 + [1] 495.52/148.10 495.52/148.10 [f_2](x1, x2, x3, x4, x5, x6) = [1] x5 + [1] x6 + [2] 495.52/148.10 495.52/148.10 [qsort](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [f_3](x1, x2, x3) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [lt^#](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [append^#](x1, x2) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [split^#](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [f_1^#](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] 495.52/148.10 495.52/148.10 [qsort^#](x1) = [4] x1 + [0] 495.52/148.10 495.52/148.10 [f_3^#](x1, x2, x3) = [4] x1 + [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_3](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c] = [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1, x2) = [7] x1 + [7] x2 + [0] 495.52/148.10 495.52/148.10 [c_3] = [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_5](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_6](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_7](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_8](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c] = [0] 495.52/148.10 495.52/148.10 [c_1](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_2](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_3](x1) = [7] x1 + [0] 495.52/148.10 495.52/148.10 [c_4](x1) = [1] x1 + [0] 495.52/148.10 495.52/148.10 [c_5](x1) = [4] x1 + [3] 495.52/148.10 495.52/148.10 [c_6](x1) = [1] x1 + [1] 495.52/148.10 495.52/148.10 [c_7](x1) = [1] x1 + [1] 495.52/148.10 495.52/148.10 The order satisfies the following ordering constraints: 495.52/148.10 495.52/148.10 [lt(0(), s(X))] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [true()] 495.52/148.10 495.52/148.10 [lt(s(X), 0())] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [false()] 495.52/148.10 495.52/148.10 [lt(s(X), s(Y))] = [0] 495.52/148.10 >= [0] 495.52/148.10 = [lt(X, Y)] 495.52/148.10 495.52/148.10 [append(nil(), Y)] = [1] Y + [0] 495.52/148.10 >= [1] Y + [0] 495.52/148.10 = [Y] 495.52/148.10 495.52/148.10 [append(add(N, X), Y)] = [1] X + [1] Y + [1] 495.52/148.10 >= [1] X + [1] Y + [1] 495.52/148.10 = [add(N, append(X, Y))] 495.52/148.10 495.52/148.10 [split(N, nil())] = [1] 495.52/148.10 >= [1] 495.52/148.10 = [pair(nil(), nil())] 495.52/148.10 495.52/148.10 [split(N, add(M, Y))] = [1] Y + [2] 495.52/148.10 >= [1] Y + [2] 495.52/148.10 = [f_1(split(N, Y), N, M, Y)] 495.52/148.10 495.52/148.10 [f_1(pair(X, Z), N, M, Y)] = [1] X + [1] Z + [2] 495.52/148.11 >= [1] X + [1] Z + [2] 495.52/148.11 = [f_2(lt(N, M), N, M, Y, X, Z)] 495.52/148.11 495.52/148.11 [f_2(true(), N, M, Y, X, Z)] = [1] X + [1] Z + [2] 495.52/148.11 >= [1] X + [1] Z + [2] 495.52/148.11 = [pair(X, add(M, Z))] 495.52/148.11 495.52/148.11 [f_2(false(), N, M, Y, X, Z)] = [1] X + [1] Z + [2] 495.52/148.11 >= [1] X + [1] Z + [2] 495.52/148.11 = [pair(add(M, X), Z)] 495.52/148.11 495.52/148.11 [qsort(nil())] = [0] 495.52/148.11 >= [0] 495.52/148.11 = [nil()] 495.52/148.11 495.52/148.11 [qsort(add(N, X))] = [1] X + [1] 495.52/148.11 >= [1] X + [1] 495.52/148.11 = [f_3(split(N, X), N, X)] 495.52/148.11 495.52/148.11 [f_3(pair(Y, Z), N, X)] = [1] Y + [1] Z + [1] 495.52/148.11 >= [1] Y + [1] Z + [1] 495.52/148.11 = [append(qsort(Y), add(X, qsort(Z)))] 495.52/148.11 495.52/148.11 [append^#(add(N, X), Y)] = [1] X + [1] 495.52/148.11 > [1] X + [0] 495.52/148.11 = [c_1(append^#(X, Y))] 495.52/148.11 495.52/148.11 [qsort^#(add(N, X))] = [4] X + [4] 495.52/148.11 >= [4] X + [4] 495.52/148.11 = [c_4(f_3^#(split(N, X), N, X))] 495.52/148.11 495.52/148.11 [f_3^#(pair(Y, Z), N, X)] = [4] Y + [4] Z + [4] 495.52/148.11 > [4] Y + [3] 495.52/148.11 = [c_5(append^#(qsort(Y), add(X, qsort(Z))))] 495.52/148.11 495.52/148.11 [f_3^#(pair(Y, Z), N, X)] = [4] Y + [4] Z + [4] 495.52/148.11 > [4] Y + [1] 495.52/148.11 = [c_6(qsort^#(Y))] 495.52/148.11 495.52/148.11 [f_3^#(pair(Y, Z), N, X)] = [4] Y + [4] Z + [4] 495.52/148.11 > [4] Z + [1] 495.52/148.11 = [c_7(qsort^#(Z))] 495.52/148.11 495.52/148.11 495.52/148.11 We return to the main proof. Consider the set of all dependency 495.52/148.11 pairs 495.52/148.11 495.52/148.11 : 495.52/148.11 { 1: append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.11 , 2: qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.11 , 3: f_3^#(pair(Y, Z), N, X) -> 495.52/148.11 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.11 , 4: f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.11 , 5: f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.11 495.52/148.11 Processor 'matrix interpretation of dimension 1' induces the 495.52/148.11 complexity certificate YES(?,O(n^1)) on application of dependency 495.52/148.11 pairs {1,3,4,5}. These cover all (indirect) predecessors of 495.52/148.11 dependency pairs {1,2,3,4,5}, their number of application is 495.52/148.11 equally bounded. The dependency pairs are shifted into the weak 495.52/148.11 component. 495.52/148.11 495.52/148.11 We are left with following problem, upon which TcT provides the 495.52/148.11 certificate YES(O(1),O(1)). 495.52/148.11 495.52/148.11 Weak DPs: 495.52/148.11 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.11 , qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.11 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.11 Weak Trs: 495.52/148.11 { lt(0(), s(X)) -> true() 495.52/148.11 , lt(s(X), 0()) -> false() 495.52/148.11 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.11 , append(nil(), Y) -> Y 495.52/148.11 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.11 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.11 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.11 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.11 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.11 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.11 , qsort(nil()) -> nil() 495.52/148.11 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.11 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.11 Obligation: 495.52/148.11 innermost runtime complexity 495.52/148.11 Answer: 495.52/148.11 YES(O(1),O(1)) 495.52/148.11 495.52/148.11 The following weak DPs constitute a sub-graph of the DG that is 495.52/148.11 closed under successors. The DPs are removed. 495.52/148.11 495.52/148.11 { append^#(add(N, X), Y) -> c_1(append^#(X, Y)) 495.52/148.11 , qsort^#(add(N, X)) -> c_4(f_3^#(split(N, X), N, X)) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> 495.52/148.11 c_5(append^#(qsort(Y), add(X, qsort(Z)))) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> c_6(qsort^#(Y)) 495.52/148.11 , f_3^#(pair(Y, Z), N, X) -> c_7(qsort^#(Z)) } 495.52/148.11 495.52/148.11 We are left with following problem, upon which TcT provides the 495.52/148.11 certificate YES(O(1),O(1)). 495.52/148.11 495.52/148.11 Weak Trs: 495.52/148.11 { lt(0(), s(X)) -> true() 495.52/148.11 , lt(s(X), 0()) -> false() 495.52/148.11 , lt(s(X), s(Y)) -> lt(X, Y) 495.52/148.11 , append(nil(), Y) -> Y 495.52/148.11 , append(add(N, X), Y) -> add(N, append(X, Y)) 495.52/148.11 , split(N, nil()) -> pair(nil(), nil()) 495.52/148.11 , split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y) 495.52/148.11 , f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z) 495.52/148.11 , f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z)) 495.52/148.11 , f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z) 495.52/148.11 , qsort(nil()) -> nil() 495.52/148.11 , qsort(add(N, X)) -> f_3(split(N, X), N, X) 495.52/148.11 , f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z))) } 495.52/148.11 Obligation: 495.52/148.11 innermost runtime complexity 495.52/148.11 Answer: 495.52/148.11 YES(O(1),O(1)) 495.52/148.11 495.52/148.11 No rule is usable, rules are removed from the input problem. 495.52/148.11 495.52/148.11 We are left with following problem, upon which TcT provides the 495.52/148.11 certificate YES(O(1),O(1)). 495.52/148.11 495.52/148.11 Rules: Empty 495.52/148.11 Obligation: 495.52/148.11 innermost runtime complexity 495.52/148.11 Answer: 495.52/148.11 YES(O(1),O(1)) 495.52/148.11 495.52/148.11 Empty rules are trivially bounded 495.52/148.11 495.52/148.11 Hurray, we answered YES(O(1),O(n^2)) 495.52/148.13 EOF