YES(O(1),O(n^3)) 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^3)). 606.81/174.00 606.81/174.00 Strict Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 606.81/174.00 , selsort(cons(N, L)) -> 606.81/174.00 ifselsort(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.00 , selsort(nil()) -> nil() 606.81/174.00 , ifselsort(true(), cons(N, L)) -> cons(N, selsort(L)) 606.81/174.00 , ifselsort(false(), cons(N, L)) -> 606.81/174.00 cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 We add the following dependency tuples: 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { eq^#(0(), 0()) -> c_1() 606.81/174.00 , eq^#(0(), s(Y)) -> c_2() 606.81/174.00 , eq^#(s(X), 0()) -> c_3() 606.81/174.00 , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(0(), Y) -> c_5() 606.81/174.00 , le^#(s(X), 0()) -> c_6() 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , min^#(cons(0(), nil())) -> c_9() 606.81/174.00 , min^#(cons(s(N), nil())) -> c_10() 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , replace^#(N, M, nil()) -> c_14() 606.81/174.00 , ifrepl^#(true(), N, M, cons(K, L)) -> c_15() 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , selsort^#(nil()) -> c_18() 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 606.81/174.00 and mark the set of starting terms. 606.81/174.00 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^3)). 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { eq^#(0(), 0()) -> c_1() 606.81/174.00 , eq^#(0(), s(Y)) -> c_2() 606.81/174.00 , eq^#(s(X), 0()) -> c_3() 606.81/174.00 , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(0(), Y) -> c_5() 606.81/174.00 , le^#(s(X), 0()) -> c_6() 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , min^#(cons(0(), nil())) -> c_9() 606.81/174.00 , min^#(cons(s(N), nil())) -> c_10() 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , replace^#(N, M, nil()) -> c_14() 606.81/174.00 , ifrepl^#(true(), N, M, cons(K, L)) -> c_15() 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , selsort^#(nil()) -> c_18() 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 Weak Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 606.81/174.00 , selsort(cons(N, L)) -> 606.81/174.00 ifselsort(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.00 , selsort(nil()) -> nil() 606.81/174.00 , ifselsort(true(), cons(N, L)) -> cons(N, selsort(L)) 606.81/174.00 , ifselsort(false(), cons(N, L)) -> 606.81/174.00 cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 We estimate the number of application of {1,2,3,5,6,9,10,14,15,18} 606.81/174.00 by applications of Pre({1,2,3,5,6,9,10,14,15,18}) = 606.81/174.00 {4,7,8,11,12,13,16,17,19,20}. Here rules are labeled as follows: 606.81/174.00 606.81/174.00 DPs: 606.81/174.00 { 1: eq^#(0(), 0()) -> c_1() 606.81/174.00 , 2: eq^#(0(), s(Y)) -> c_2() 606.81/174.00 , 3: eq^#(s(X), 0()) -> c_3() 606.81/174.00 , 4: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , 5: le^#(0(), Y) -> c_5() 606.81/174.00 , 6: le^#(s(X), 0()) -> c_6() 606.81/174.00 , 7: le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , 8: min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , 9: min^#(cons(0(), nil())) -> c_9() 606.81/174.00 , 10: min^#(cons(s(N), nil())) -> c_10() 606.81/174.00 , 11: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.00 c_11(min^#(cons(N, L))) 606.81/174.00 , 12: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.00 c_12(min^#(cons(M, L))) 606.81/174.00 , 13: replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , 14: replace^#(N, M, nil()) -> c_14() 606.81/174.00 , 15: ifrepl^#(true(), N, M, cons(K, L)) -> c_15() 606.81/174.00 , 16: ifrepl^#(false(), N, M, cons(K, L)) -> 606.81/174.00 c_16(replace^#(N, M, L)) 606.81/174.00 , 17: selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , 18: selsort^#(nil()) -> c_18() 606.81/174.00 , 19: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , 20: ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^3)). 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 Weak DPs: 606.81/174.00 { eq^#(0(), 0()) -> c_1() 606.81/174.00 , eq^#(0(), s(Y)) -> c_2() 606.81/174.00 , eq^#(s(X), 0()) -> c_3() 606.81/174.00 , le^#(0(), Y) -> c_5() 606.81/174.00 , le^#(s(X), 0()) -> c_6() 606.81/174.00 , min^#(cons(0(), nil())) -> c_9() 606.81/174.00 , min^#(cons(s(N), nil())) -> c_10() 606.81/174.00 , replace^#(N, M, nil()) -> c_14() 606.81/174.00 , ifrepl^#(true(), N, M, cons(K, L)) -> c_15() 606.81/174.00 , selsort^#(nil()) -> c_18() } 606.81/174.00 Weak Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 606.81/174.00 , selsort(cons(N, L)) -> 606.81/174.00 ifselsort(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.00 , selsort(nil()) -> nil() 606.81/174.00 , ifselsort(true(), cons(N, L)) -> cons(N, selsort(L)) 606.81/174.00 , ifselsort(false(), cons(N, L)) -> 606.81/174.00 cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 The following weak DPs constitute a sub-graph of the DG that is 606.81/174.00 closed under successors. The DPs are removed. 606.81/174.00 606.81/174.00 { eq^#(0(), 0()) -> c_1() 606.81/174.00 , eq^#(0(), s(Y)) -> c_2() 606.81/174.00 , eq^#(s(X), 0()) -> c_3() 606.81/174.00 , le^#(0(), Y) -> c_5() 606.81/174.00 , le^#(s(X), 0()) -> c_6() 606.81/174.00 , min^#(cons(0(), nil())) -> c_9() 606.81/174.00 , min^#(cons(s(N), nil())) -> c_10() 606.81/174.00 , replace^#(N, M, nil()) -> c_14() 606.81/174.00 , ifrepl^#(true(), N, M, cons(K, L)) -> c_15() 606.81/174.00 , selsort^#(nil()) -> c_18() } 606.81/174.00 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^3)). 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 Weak Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 606.81/174.00 , selsort(cons(N, L)) -> 606.81/174.00 ifselsort(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.00 , selsort(nil()) -> nil() 606.81/174.00 , ifselsort(true(), cons(N, L)) -> cons(N, selsort(L)) 606.81/174.00 , ifselsort(false(), cons(N, L)) -> 606.81/174.00 cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 We replace rewrite rules by usable rules: 606.81/174.00 606.81/174.00 Weak Usable Rules: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.00 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^3)). 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 Weak Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^3)) 606.81/174.00 606.81/174.00 We decompose the input problem according to the dependency graph 606.81/174.00 into the upper component 606.81/174.00 606.81/174.00 { selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 606.81/174.00 and lower component 606.81/174.00 606.81/174.00 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.00 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.00 , min^#(cons(N, cons(M, L))) -> 606.81/174.00 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.00 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.00 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.00 , replace^#(N, M, cons(K, L)) -> 606.81/174.00 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.00 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) } 606.81/174.00 606.81/174.00 Further, following extension rules are added to the lower 606.81/174.00 component. 606.81/174.00 606.81/174.00 { selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.00 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.00 , selsort^#(cons(N, L)) -> 606.81/174.00 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 replace^#(min(cons(N, L)), N, L) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.00 606.81/174.00 TcT solves the upper component with certificate YES(O(1),O(n^1)). 606.81/174.00 606.81/174.00 Sub-proof: 606.81/174.00 ---------- 606.81/174.00 We are left with following problem, upon which TcT provides the 606.81/174.00 certificate YES(O(1),O(n^1)). 606.81/174.00 606.81/174.00 Strict DPs: 606.81/174.00 { selsort^#(cons(N, L)) -> 606.81/174.00 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.00 eq^#(N, min(cons(N, L))), 606.81/174.00 min^#(cons(N, L))) 606.81/174.00 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.00 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 Weak Trs: 606.81/174.00 { eq(0(), 0()) -> true() 606.81/174.00 , eq(0(), s(Y)) -> false() 606.81/174.00 , eq(s(X), 0()) -> false() 606.81/174.00 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.00 , le(0(), Y) -> true() 606.81/174.00 , le(s(X), 0()) -> false() 606.81/174.00 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.00 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.00 , min(cons(0(), nil())) -> 0() 606.81/174.00 , min(cons(s(N), nil())) -> s(N) 606.81/174.00 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.00 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.00 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.00 , replace(N, M, nil()) -> nil() 606.81/174.00 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.00 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.00 Obligation: 606.81/174.00 innermost runtime complexity 606.81/174.00 Answer: 606.81/174.00 YES(O(1),O(n^1)) 606.81/174.00 606.81/174.00 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.00 orient following rules strictly. 606.81/174.00 606.81/174.00 DPs: 606.81/174.00 { 3: ifselsort^#(false(), cons(N, L)) -> 606.81/174.00 c_20(min^#(cons(N, L)), 606.81/174.00 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.00 replace^#(min(cons(N, L)), N, L), 606.81/174.00 min^#(cons(N, L))) } 606.81/174.00 606.81/174.00 Sub-proof: 606.81/174.00 ---------- 606.81/174.00 The following argument positions are usable: 606.81/174.00 Uargs(c_17) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {2, 3} 606.81/174.00 606.81/174.00 TcT has computed the following constructor-based matrix 606.81/174.00 interpretation satisfying not(EDA). 606.81/174.00 606.81/174.00 [eq](x1, x2) = [0] 606.81/174.01 606.81/174.01 [0] = [0] 606.81/174.01 606.81/174.01 [true] = [0] 606.81/174.01 606.81/174.01 [s](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [false] = [0] 606.81/174.01 606.81/174.01 [le](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min](x1) = [0] 606.81/174.01 606.81/174.01 [cons](x1, x2) = [1] x2 + [1] 606.81/174.01 606.81/174.01 [nil] = [0] 606.81/174.01 606.81/174.01 [ifmin](x1, x2) = [0] 606.81/174.01 606.81/174.01 [replace](x1, x2, x3) = [1] x3 + [0] 606.81/174.01 606.81/174.01 [ifrepl](x1, x2, x3, x4) = [1] x4 + [0] 606.81/174.01 606.81/174.01 [eq^#](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min^#](x1) = [0] 606.81/174.01 606.81/174.01 [replace^#](x1, x2, x3) = [0] 606.81/174.01 606.81/174.01 [selsort^#](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [c_17](x1, x2, x3) = [1] x1 + [4] x2 + [0] 606.81/174.01 606.81/174.01 [ifselsort^#](x1, x2) = [1] x2 + [0] 606.81/174.01 606.81/174.01 [c_19](x1) = [1] x1 + [1] 606.81/174.01 606.81/174.01 [c_20](x1, x2, x3, x4) = [1] x2 + [4] x3 + [0] 606.81/174.01 606.81/174.01 The order satisfies the following ordering constraints: 606.81/174.01 606.81/174.01 [eq(0(), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [eq(0(), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [eq(X, Y)] 606.81/174.01 606.81/174.01 [le(0(), Y)] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [le(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [le(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [le(X, Y)] 606.81/174.01 606.81/174.01 [min(cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.01 606.81/174.01 [min(cons(0(), nil()))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [0()] 606.81/174.01 606.81/174.01 [min(cons(s(N), nil()))] = [0] 606.81/174.01 ? [1] N + [0] 606.81/174.01 = [s(N)] 606.81/174.01 606.81/174.01 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(N, L))] 606.81/174.01 606.81/174.01 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(M, L))] 606.81/174.01 606.81/174.01 [replace(N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.01 606.81/174.01 [replace(N, M, nil())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [nil()] 606.81/174.01 606.81/174.01 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [cons(M, L)] 606.81/174.01 606.81/174.01 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [cons(K, replace(N, M, L))] 606.81/174.01 606.81/174.01 [selsort^#(cons(N, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 [ifselsort^#(true(), cons(N, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [c_19(selsort^#(L))] 606.81/174.01 606.81/174.01 [ifselsort^#(false(), cons(N, L))] = [1] L + [1] 606.81/174.01 > [1] L + [0] 606.81/174.01 = [c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 606.81/174.01 The strictly oriented rules are moved into the weak component. 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(n^1)). 606.81/174.01 606.81/174.01 Strict DPs: 606.81/174.01 { selsort^#(cons(N, L)) -> 606.81/174.01 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L))) 606.81/174.01 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) } 606.81/174.01 Weak DPs: 606.81/174.01 { ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 Weak Trs: 606.81/174.01 { eq(0(), 0()) -> true() 606.81/174.01 , eq(0(), s(Y)) -> false() 606.81/174.01 , eq(s(X), 0()) -> false() 606.81/174.01 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.01 , le(0(), Y) -> true() 606.81/174.01 , le(s(X), 0()) -> false() 606.81/174.01 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.01 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.01 , min(cons(0(), nil())) -> 0() 606.81/174.01 , min(cons(s(N), nil())) -> s(N) 606.81/174.01 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.01 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.01 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.01 , replace(N, M, nil()) -> nil() 606.81/174.01 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.01 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.01 Obligation: 606.81/174.01 innermost runtime complexity 606.81/174.01 Answer: 606.81/174.01 YES(O(1),O(n^1)) 606.81/174.01 606.81/174.01 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.01 orient following rules strictly. 606.81/174.01 606.81/174.01 DPs: 606.81/174.01 { 2: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) } 606.81/174.01 606.81/174.01 Sub-proof: 606.81/174.01 ---------- 606.81/174.01 The following argument positions are usable: 606.81/174.01 Uargs(c_17) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {2, 3} 606.81/174.01 606.81/174.01 TcT has computed the following constructor-based matrix 606.81/174.01 interpretation satisfying not(EDA). 606.81/174.01 606.81/174.01 [eq](x1, x2) = [0] 606.81/174.01 606.81/174.01 [0] = [0] 606.81/174.01 606.81/174.01 [true] = [0] 606.81/174.01 606.81/174.01 [s](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [false] = [0] 606.81/174.01 606.81/174.01 [le](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min](x1) = [0] 606.81/174.01 606.81/174.01 [cons](x1, x2) = [1] x2 + [1] 606.81/174.01 606.81/174.01 [nil] = [0] 606.81/174.01 606.81/174.01 [ifmin](x1, x2) = [0] 606.81/174.01 606.81/174.01 [replace](x1, x2, x3) = [1] x3 + [0] 606.81/174.01 606.81/174.01 [ifrepl](x1, x2, x3, x4) = [1] x4 + [0] 606.81/174.01 606.81/174.01 [eq^#](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min^#](x1) = [0] 606.81/174.01 606.81/174.01 [replace^#](x1, x2, x3) = [0] 606.81/174.01 606.81/174.01 [selsort^#](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [c_17](x1, x2, x3) = [1] x1 + [1] x2 + [0] 606.81/174.01 606.81/174.01 [ifselsort^#](x1, x2) = [1] x2 + [0] 606.81/174.01 606.81/174.01 [c_19](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [c_20](x1, x2, x3, x4) = [1] x2 + [4] x3 + [1] 606.81/174.01 606.81/174.01 The order satisfies the following ordering constraints: 606.81/174.01 606.81/174.01 [eq(0(), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [eq(0(), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [eq(X, Y)] 606.81/174.01 606.81/174.01 [le(0(), Y)] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [le(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [le(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [le(X, Y)] 606.81/174.01 606.81/174.01 [min(cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.01 606.81/174.01 [min(cons(0(), nil()))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [0()] 606.81/174.01 606.81/174.01 [min(cons(s(N), nil()))] = [0] 606.81/174.01 ? [1] N + [0] 606.81/174.01 = [s(N)] 606.81/174.01 606.81/174.01 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(N, L))] 606.81/174.01 606.81/174.01 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(M, L))] 606.81/174.01 606.81/174.01 [replace(N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.01 606.81/174.01 [replace(N, M, nil())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [nil()] 606.81/174.01 606.81/174.01 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [cons(M, L)] 606.81/174.01 606.81/174.01 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [cons(K, replace(N, M, L))] 606.81/174.01 606.81/174.01 [selsort^#(cons(N, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 [ifselsort^#(true(), cons(N, L))] = [1] L + [1] 606.81/174.01 > [1] L + [0] 606.81/174.01 = [c_19(selsort^#(L))] 606.81/174.01 606.81/174.01 [ifselsort^#(false(), cons(N, L))] = [1] L + [1] 606.81/174.01 >= [1] L + [1] 606.81/174.01 = [c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 606.81/174.01 The strictly oriented rules are moved into the weak component. 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(n^1)). 606.81/174.01 606.81/174.01 Strict DPs: 606.81/174.01 { selsort^#(cons(N, L)) -> 606.81/174.01 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 Weak DPs: 606.81/174.01 { ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.01 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 Weak Trs: 606.81/174.01 { eq(0(), 0()) -> true() 606.81/174.01 , eq(0(), s(Y)) -> false() 606.81/174.01 , eq(s(X), 0()) -> false() 606.81/174.01 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.01 , le(0(), Y) -> true() 606.81/174.01 , le(s(X), 0()) -> false() 606.81/174.01 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.01 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.01 , min(cons(0(), nil())) -> 0() 606.81/174.01 , min(cons(s(N), nil())) -> s(N) 606.81/174.01 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.01 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.01 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.01 , replace(N, M, nil()) -> nil() 606.81/174.01 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.01 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.01 Obligation: 606.81/174.01 innermost runtime complexity 606.81/174.01 Answer: 606.81/174.01 YES(O(1),O(n^1)) 606.81/174.01 606.81/174.01 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.01 orient following rules strictly. 606.81/174.01 606.81/174.01 DPs: 606.81/174.01 { 2: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.01 , 3: ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 606.81/174.01 Sub-proof: 606.81/174.01 ---------- 606.81/174.01 The following argument positions are usable: 606.81/174.01 Uargs(c_17) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {2, 3} 606.81/174.01 606.81/174.01 TcT has computed the following constructor-based matrix 606.81/174.01 interpretation satisfying not(EDA). 606.81/174.01 606.81/174.01 [eq](x1, x2) = [0] 606.81/174.01 606.81/174.01 [0] = [0] 606.81/174.01 606.81/174.01 [true] = [0] 606.81/174.01 606.81/174.01 [s](x1) = [1] x1 + [0] 606.81/174.01 606.81/174.01 [false] = [0] 606.81/174.01 606.81/174.01 [le](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min](x1) = [0] 606.81/174.01 606.81/174.01 [cons](x1, x2) = [1] x2 + [2] 606.81/174.01 606.81/174.01 [nil] = [0] 606.81/174.01 606.81/174.01 [ifmin](x1, x2) = [0] 606.81/174.01 606.81/174.01 [replace](x1, x2, x3) = [1] x3 + [0] 606.81/174.01 606.81/174.01 [ifrepl](x1, x2, x3, x4) = [1] x4 + [0] 606.81/174.01 606.81/174.01 [eq^#](x1, x2) = [0] 606.81/174.01 606.81/174.01 [min^#](x1) = [0] 606.81/174.01 606.81/174.01 [replace^#](x1, x2, x3) = [0] 606.81/174.01 606.81/174.01 [selsort^#](x1) = [2] x1 + [0] 606.81/174.01 606.81/174.01 [c_17](x1, x2, x3) = [1] x1 + [2] x2 + [0] 606.81/174.01 606.81/174.01 [ifselsort^#](x1, x2) = [2] x2 + [0] 606.81/174.01 606.81/174.01 [c_19](x1) = [1] x1 + [1] 606.81/174.01 606.81/174.01 [c_20](x1, x2, x3, x4) = [1] x2 + [4] x3 + [1] 606.81/174.01 606.81/174.01 The order satisfies the following ordering constraints: 606.81/174.01 606.81/174.01 [eq(0(), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [eq(0(), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [eq(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [eq(X, Y)] 606.81/174.01 606.81/174.01 [le(0(), Y)] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [true()] 606.81/174.01 606.81/174.01 [le(s(X), 0())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [false()] 606.81/174.01 606.81/174.01 [le(s(X), s(Y))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [le(X, Y)] 606.81/174.01 606.81/174.01 [min(cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.01 606.81/174.01 [min(cons(0(), nil()))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [0()] 606.81/174.01 606.81/174.01 [min(cons(s(N), nil()))] = [0] 606.81/174.01 ? [1] N + [0] 606.81/174.01 = [s(N)] 606.81/174.01 606.81/174.01 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(N, L))] 606.81/174.01 606.81/174.01 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [min(cons(M, L))] 606.81/174.01 606.81/174.01 [replace(N, M, cons(K, L))] = [1] L + [2] 606.81/174.01 >= [1] L + [2] 606.81/174.01 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.01 606.81/174.01 [replace(N, M, nil())] = [0] 606.81/174.01 >= [0] 606.81/174.01 = [nil()] 606.81/174.01 606.81/174.01 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [2] 606.81/174.01 >= [1] L + [2] 606.81/174.01 = [cons(M, L)] 606.81/174.01 606.81/174.01 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [2] 606.81/174.01 >= [1] L + [2] 606.81/174.01 = [cons(K, replace(N, M, L))] 606.81/174.01 606.81/174.01 [selsort^#(cons(N, L))] = [2] L + [4] 606.81/174.01 >= [2] L + [4] 606.81/174.01 = [c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 [ifselsort^#(true(), cons(N, L))] = [2] L + [4] 606.81/174.01 > [2] L + [1] 606.81/174.01 = [c_19(selsort^#(L))] 606.81/174.01 606.81/174.01 [ifselsort^#(false(), cons(N, L))] = [2] L + [4] 606.81/174.01 > [2] L + [1] 606.81/174.01 = [c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L)))] 606.81/174.01 606.81/174.01 606.81/174.01 We return to the main proof. Consider the set of all dependency 606.81/174.01 pairs 606.81/174.01 606.81/174.01 : 606.81/174.01 { 1: selsort^#(cons(N, L)) -> 606.81/174.01 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L))) 606.81/174.01 , 2: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.01 , 3: ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 606.81/174.01 Processor 'matrix interpretation of dimension 1' induces the 606.81/174.01 complexity certificate YES(?,O(n^1)) on application of dependency 606.81/174.01 pairs {2,3}. These cover all (indirect) predecessors of dependency 606.81/174.01 pairs {1,2,3}, their number of application is equally bounded. The 606.81/174.01 dependency pairs are shifted into the weak component. 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(1)). 606.81/174.01 606.81/174.01 Weak DPs: 606.81/174.01 { selsort^#(cons(N, L)) -> 606.81/174.01 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L))) 606.81/174.01 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.01 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 Weak Trs: 606.81/174.01 { eq(0(), 0()) -> true() 606.81/174.01 , eq(0(), s(Y)) -> false() 606.81/174.01 , eq(s(X), 0()) -> false() 606.81/174.01 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.01 , le(0(), Y) -> true() 606.81/174.01 , le(s(X), 0()) -> false() 606.81/174.01 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.01 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.01 , min(cons(0(), nil())) -> 0() 606.81/174.01 , min(cons(s(N), nil())) -> s(N) 606.81/174.01 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.01 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.01 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.01 , replace(N, M, nil()) -> nil() 606.81/174.01 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.01 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.01 Obligation: 606.81/174.01 innermost runtime complexity 606.81/174.01 Answer: 606.81/174.01 YES(O(1),O(1)) 606.81/174.01 606.81/174.01 The following weak DPs constitute a sub-graph of the DG that is 606.81/174.01 closed under successors. The DPs are removed. 606.81/174.01 606.81/174.01 { selsort^#(cons(N, L)) -> 606.81/174.01 c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)), 606.81/174.01 eq^#(N, min(cons(N, L))), 606.81/174.01 min^#(cons(N, L))) 606.81/174.01 , ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L)) 606.81/174.01 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.01 c_20(min^#(cons(N, L)), 606.81/174.01 selsort^#(replace(min(cons(N, L)), N, L)), 606.81/174.01 replace^#(min(cons(N, L)), N, L), 606.81/174.01 min^#(cons(N, L))) } 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(1)). 606.81/174.01 606.81/174.01 Weak Trs: 606.81/174.01 { eq(0(), 0()) -> true() 606.81/174.01 , eq(0(), s(Y)) -> false() 606.81/174.01 , eq(s(X), 0()) -> false() 606.81/174.01 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.01 , le(0(), Y) -> true() 606.81/174.01 , le(s(X), 0()) -> false() 606.81/174.01 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.01 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.01 , min(cons(0(), nil())) -> 0() 606.81/174.01 , min(cons(s(N), nil())) -> s(N) 606.81/174.01 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.01 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.01 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.01 , replace(N, M, nil()) -> nil() 606.81/174.01 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.01 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.01 Obligation: 606.81/174.01 innermost runtime complexity 606.81/174.01 Answer: 606.81/174.01 YES(O(1),O(1)) 606.81/174.01 606.81/174.01 No rule is usable, rules are removed from the input problem. 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(1)). 606.81/174.01 606.81/174.01 Rules: Empty 606.81/174.01 Obligation: 606.81/174.01 innermost runtime complexity 606.81/174.01 Answer: 606.81/174.01 YES(O(1),O(1)) 606.81/174.01 606.81/174.01 Empty rules are trivially bounded 606.81/174.01 606.81/174.01 We return to the main proof. 606.81/174.01 606.81/174.01 We are left with following problem, upon which TcT provides the 606.81/174.01 certificate YES(O(1),O(n^2)). 606.81/174.01 606.81/174.01 Strict DPs: 606.81/174.01 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.01 , le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.01 , min^#(cons(N, cons(M, L))) -> 606.81/174.02 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.02 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.02 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.02 , replace^#(N, M, cons(K, L)) -> 606.81/174.02 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.02 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) } 606.81/174.02 Weak DPs: 606.81/174.02 { selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.02 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , selsort^#(cons(N, L)) -> 606.81/174.02 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.02 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 replace^#(min(cons(N, L)), N, L) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.02 Weak Trs: 606.81/174.02 { eq(0(), 0()) -> true() 606.81/174.02 , eq(0(), s(Y)) -> false() 606.81/174.02 , eq(s(X), 0()) -> false() 606.81/174.02 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.02 , le(0(), Y) -> true() 606.81/174.02 , le(s(X), 0()) -> false() 606.81/174.02 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.02 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.02 , min(cons(0(), nil())) -> 0() 606.81/174.02 , min(cons(s(N), nil())) -> s(N) 606.81/174.02 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.02 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.02 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.02 , replace(N, M, nil()) -> nil() 606.81/174.02 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.02 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.02 Obligation: 606.81/174.02 innermost runtime complexity 606.81/174.02 Answer: 606.81/174.02 YES(O(1),O(n^2)) 606.81/174.02 606.81/174.02 We use the processor 'matrix interpretation of dimension 2' to 606.81/174.02 orient following rules strictly. 606.81/174.02 606.81/174.02 DPs: 606.81/174.02 { 1: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.02 , 6: replace^#(N, M, cons(K, L)) -> 606.81/174.02 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.02 , 8: selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.02 , 9: selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , 10: selsort^#(cons(N, L)) -> 606.81/174.02 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.02 , 12: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , 13: ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 replace^#(min(cons(N, L)), N, L) } 606.81/174.02 Trs: 606.81/174.02 { min(cons(0(), nil())) -> 0() 606.81/174.02 , min(cons(s(N), nil())) -> s(N) 606.81/174.02 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.02 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.02 , replace(N, M, nil()) -> nil() 606.81/174.02 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.02 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.02 606.81/174.02 Sub-proof: 606.81/174.02 ---------- 606.81/174.02 The following argument positions are usable: 606.81/174.02 Uargs(c_4) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}, 606.81/174.02 Uargs(c_11) = {1}, Uargs(c_12) = {1}, Uargs(c_13) = {1, 2}, 606.81/174.02 Uargs(c_16) = {1} 606.81/174.02 606.81/174.02 TcT has computed the following constructor-based matrix 606.81/174.02 interpretation satisfying not(EDA) and not(IDA(1)). 606.81/174.02 606.81/174.02 [eq](x1, x2) = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [0] = [1] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [true] = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [s](x1) = [1 0] x1 + [4] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [false] = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [le](x1, x2) = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [min](x1) = [0 1] x1 + [0] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [cons](x1, x2) = [0 0] x1 + [0 1] x2 + [0] 606.81/174.02 [1 0] [0 1] [1] 606.81/174.02 606.81/174.02 [nil] = [0] 606.81/174.02 [7] 606.81/174.02 606.81/174.02 [ifmin](x1, x2) = [0 1] x2 + [0] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [replace](x1, x2, x3) = [4 4] x1 + [4 4] x2 + [2 0] x3 + [4] 606.81/174.02 [0 0] [1 0] [0 1] [0] 606.81/174.02 606.81/174.02 [ifrepl](x1, x2, x3, x4) = [4 4] x3 + [1 0] x4 + [4] 606.81/174.02 [1 0] [0 1] [0] 606.81/174.02 606.81/174.02 [eq^#](x1, x2) = [2 0] x2 + [0] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [c_4](x1) = [1 0] x1 + [1] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [le^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 606.81/174.02 [1 0] [1 0] [0] 606.81/174.02 606.81/174.02 [c_7](x1) = [4 0] x1 + [0] 606.81/174.02 [0 0] [7] 606.81/174.02 606.81/174.02 [min^#](x1) = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [c_8](x1, x2) = [2 0] x1 + [4 0] x2 + [0] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 606.81/174.02 [ifmin^#](x1, x2) = [0] 606.81/174.02 [0] 606.81/174.02 606.81/174.02 [c_11](x1) = [1 0] x1 + [0] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [c_12](x1) = [2 0] x1 + [0] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [replace^#](x1, x2, x3) = [0 2] x3 + [2] 606.81/174.02 [0 0] [0] 606.81/174.02 606.81/174.02 [c_13](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 606.81/174.02 [ifrepl^#](x1, x2, x3, x4) = [0 0] x3 + [2 0] x4 + [2] 606.81/174.02 [0 4] [0 0] [4] 606.81/174.02 606.81/174.02 [c_16](x1) = [1 0] x1 + [0] 606.81/174.02 [0 0] [3] 606.81/174.02 606.81/174.02 [selsort^#](x1) = [0 2] x1 + [6] 606.81/174.02 [0 0] [4] 606.81/174.02 606.81/174.02 [ifselsort^#](x1, x2) = [0 2] x2 + [4] 606.81/174.02 [0 0] [4] 606.81/174.02 606.81/174.02 The order satisfies the following ordering constraints: 606.81/174.02 606.81/174.02 [eq(0(), 0())] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [true()] 606.81/174.02 606.81/174.02 [eq(0(), s(Y))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [false()] 606.81/174.02 606.81/174.02 [eq(s(X), 0())] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [false()] 606.81/174.02 606.81/174.02 [eq(s(X), s(Y))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [eq(X, Y)] 606.81/174.02 606.81/174.02 [le(0(), Y)] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [true()] 606.81/174.02 606.81/174.02 [le(s(X), 0())] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [false()] 606.81/174.02 606.81/174.02 [le(s(X), s(Y))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [le(X, Y)] 606.81/174.02 606.81/174.02 [min(cons(N, cons(M, L)))] = [1 0] N + [1 0] M + [0 1] L + [2] 606.81/174.02 [0 0] [0 0] [0 0] [0] 606.81/174.02 >= [1 0] N + [1 0] M + [0 1] L + [2] 606.81/174.02 [0 0] [0 0] [0 0] [0] 606.81/174.02 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.02 606.81/174.02 [min(cons(0(), nil()))] = [9] 606.81/174.02 [0] 606.81/174.02 > [1] 606.81/174.02 [0] 606.81/174.02 = [0()] 606.81/174.02 606.81/174.02 [min(cons(s(N), nil()))] = [1 0] N + [12] 606.81/174.02 [0 0] [0] 606.81/174.02 > [1 0] N + [4] 606.81/174.02 [0 0] [0] 606.81/174.02 = [s(N)] 606.81/174.02 606.81/174.02 [ifmin(true(), cons(N, cons(M, L)))] = [1 0] N + [1 0] M + [0 1] L + [2] 606.81/174.02 [0 0] [0 0] [0 0] [0] 606.81/174.02 > [1 0] N + [0 1] L + [1] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 = [min(cons(N, L))] 606.81/174.02 606.81/174.02 [ifmin(false(), cons(N, cons(M, L)))] = [1 0] N + [1 0] M + [0 1] L + [2] 606.81/174.02 [0 0] [0 0] [0 0] [0] 606.81/174.02 > [1 0] M + [0 1] L + [1] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 = [min(cons(M, L))] 606.81/174.02 606.81/174.02 [replace(N, M, cons(K, L))] = [4 4] N + [4 4] M + [0 2] L + [0 0] K + [4] 606.81/174.02 [0 0] [1 0] [0 1] [1 0] [1] 606.81/174.02 >= [4 4] M + [0 1] L + [0 0] K + [4] 606.81/174.02 [1 0] [0 1] [1 0] [1] 606.81/174.02 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.02 606.81/174.02 [replace(N, M, nil())] = [4 4] N + [4 4] M + [4] 606.81/174.02 [0 0] [1 0] [7] 606.81/174.02 > [0] 606.81/174.02 [7] 606.81/174.02 = [nil()] 606.81/174.02 606.81/174.02 [ifrepl(true(), N, M, cons(K, L))] = [4 4] M + [0 1] L + [0 0] K + [4] 606.81/174.02 [1 0] [0 1] [1 0] [1] 606.81/174.02 > [0 0] M + [0 1] L + [0] 606.81/174.02 [1 0] [0 1] [1] 606.81/174.02 = [cons(M, L)] 606.81/174.02 606.81/174.02 [ifrepl(false(), N, M, cons(K, L))] = [4 4] M + [0 1] L + [0 0] K + [4] 606.81/174.02 [1 0] [0 1] [1 0] [1] 606.81/174.02 > [1 0] M + [0 1] L + [0 0] K + [0] 606.81/174.02 [1 0] [0 1] [1 0] [1] 606.81/174.02 = [cons(K, replace(N, M, L))] 606.81/174.02 606.81/174.02 [eq^#(s(X), s(Y))] = [2 0] Y + [8] 606.81/174.02 [0 0] [0] 606.81/174.02 > [2 0] Y + [1] 606.81/174.02 [0 0] [0] 606.81/174.02 = [c_4(eq^#(X, Y))] 606.81/174.02 606.81/174.02 [le^#(s(X), s(Y))] = [0 0] Y + [0 0] X + [0] 606.81/174.02 [1 0] [1 0] [8] 606.81/174.02 >= [0] 606.81/174.02 [7] 606.81/174.02 = [c_7(le^#(X, Y))] 606.81/174.02 606.81/174.02 [min^#(cons(N, cons(M, L)))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))] 606.81/174.02 606.81/174.02 [ifmin^#(true(), cons(N, cons(M, L)))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [c_11(min^#(cons(N, L)))] 606.81/174.02 606.81/174.02 [ifmin^#(false(), cons(N, cons(M, L)))] = [0] 606.81/174.02 [0] 606.81/174.02 >= [0] 606.81/174.02 [0] 606.81/174.02 = [c_12(min^#(cons(M, L)))] 606.81/174.02 606.81/174.02 [replace^#(N, M, cons(K, L))] = [0 2] L + [2 0] K + [4] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 > [0 2] L + [2 0] K + [3] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 = [c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))] 606.81/174.02 606.81/174.02 [ifrepl^#(false(), N, M, cons(K, L))] = [0 0] M + [0 2] L + [2] 606.81/174.02 [0 4] [0 0] [4] 606.81/174.02 >= [0 2] L + [2] 606.81/174.02 [0 0] [3] 606.81/174.02 = [c_16(replace^#(N, M, L))] 606.81/174.02 606.81/174.02 [selsort^#(cons(N, L))] = [2 0] N + [0 2] L + [8] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 > [2 0] N + [0 2] L + [2] 606.81/174.02 [0 0] [0 0] [0] 606.81/174.02 = [eq^#(N, min(cons(N, L)))] 606.81/174.02 606.81/174.02 [selsort^#(cons(N, L))] = [2 0] N + [0 2] L + [8] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 > [0] 606.81/174.02 [0] 606.81/174.02 = [min^#(cons(N, L))] 606.81/174.02 606.81/174.02 [selsort^#(cons(N, L))] = [2 0] N + [0 2] L + [8] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 > [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 = [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))] 606.81/174.02 606.81/174.02 [ifselsort^#(true(), cons(N, L))] = [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 >= [0 2] L + [6] 606.81/174.02 [0 0] [4] 606.81/174.02 = [selsort^#(L)] 606.81/174.02 606.81/174.02 [ifselsort^#(false(), cons(N, L))] = [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 > [0] 606.81/174.02 [0] 606.81/174.02 = [min^#(cons(N, L))] 606.81/174.02 606.81/174.02 [ifselsort^#(false(), cons(N, L))] = [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 > [0 2] L + [2] 606.81/174.02 [0 0] [0] 606.81/174.02 = [replace^#(min(cons(N, L)), N, L)] 606.81/174.02 606.81/174.02 [ifselsort^#(false(), cons(N, L))] = [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 >= [2 0] N + [0 2] L + [6] 606.81/174.02 [0 0] [0 0] [4] 606.81/174.02 = [selsort^#(replace(min(cons(N, L)), N, L))] 606.81/174.02 606.81/174.02 606.81/174.02 We return to the main proof. Consider the set of all dependency 606.81/174.02 pairs 606.81/174.02 606.81/174.02 : 606.81/174.02 { 1: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.02 , 2: le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.02 , 3: min^#(cons(N, cons(M, L))) -> 606.81/174.02 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.02 , 4: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.02 c_11(min^#(cons(N, L))) 606.81/174.02 , 5: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.02 c_12(min^#(cons(M, L))) 606.81/174.02 , 6: replace^#(N, M, cons(K, L)) -> 606.81/174.02 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.02 , 7: ifrepl^#(false(), N, M, cons(K, L)) -> 606.81/174.02 c_16(replace^#(N, M, L)) 606.81/174.02 , 8: selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.02 , 9: selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , 10: selsort^#(cons(N, L)) -> 606.81/174.02 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.02 , 11: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.02 , 12: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , 13: ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 replace^#(min(cons(N, L)), N, L) 606.81/174.02 , 14: ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.02 606.81/174.02 Processor 'matrix interpretation of dimension 2' induces the 606.81/174.02 complexity certificate YES(?,O(n^1)) on application of dependency 606.81/174.02 pairs {1,6,8,9,10,12,13}. These cover all (indirect) predecessors 606.81/174.02 of dependency pairs {1,6,7,8,9,10,11,12,13,14}, their number of 606.81/174.02 application is equally bounded. The dependency pairs are shifted 606.81/174.02 into the weak component. 606.81/174.02 606.81/174.02 We are left with following problem, upon which TcT provides the 606.81/174.02 certificate YES(O(1),O(n^2)). 606.81/174.02 606.81/174.02 Strict DPs: 606.81/174.02 { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.02 , min^#(cons(N, cons(M, L))) -> 606.81/174.02 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.02 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.02 , ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.02 c_12(min^#(cons(M, L))) } 606.81/174.02 Weak DPs: 606.81/174.02 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.02 , replace^#(N, M, cons(K, L)) -> 606.81/174.02 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.02 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.02 , selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.02 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , selsort^#(cons(N, L)) -> 606.81/174.02 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.02 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 replace^#(min(cons(N, L)), N, L) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.02 Weak Trs: 606.81/174.02 { eq(0(), 0()) -> true() 606.81/174.02 , eq(0(), s(Y)) -> false() 606.81/174.02 , eq(s(X), 0()) -> false() 606.81/174.02 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.02 , le(0(), Y) -> true() 606.81/174.02 , le(s(X), 0()) -> false() 606.81/174.02 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.02 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.02 , min(cons(0(), nil())) -> 0() 606.81/174.02 , min(cons(s(N), nil())) -> s(N) 606.81/174.02 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.02 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.02 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.02 , replace(N, M, nil()) -> nil() 606.81/174.02 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.02 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.02 Obligation: 606.81/174.02 innermost runtime complexity 606.81/174.02 Answer: 606.81/174.02 YES(O(1),O(n^2)) 606.81/174.02 606.81/174.02 The following weak DPs constitute a sub-graph of the DG that is 606.81/174.02 closed under successors. The DPs are removed. 606.81/174.02 606.81/174.02 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 606.81/174.02 , replace^#(N, M, cons(K, L)) -> 606.81/174.02 c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K)) 606.81/174.02 , ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) 606.81/174.02 , selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L))) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 replace^#(min(cons(N, L)), N, L) } 606.81/174.02 606.81/174.02 We are left with following problem, upon which TcT provides the 606.81/174.02 certificate YES(O(1),O(n^2)). 606.81/174.02 606.81/174.02 Strict DPs: 606.81/174.02 { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.02 , min^#(cons(N, cons(M, L))) -> 606.81/174.02 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.02 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.02 , ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.02 c_12(min^#(cons(M, L))) } 606.81/174.02 Weak DPs: 606.81/174.02 { selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , selsort^#(cons(N, L)) -> 606.81/174.02 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.02 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.02 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.02 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.02 Weak Trs: 606.81/174.02 { eq(0(), 0()) -> true() 606.81/174.02 , eq(0(), s(Y)) -> false() 606.81/174.02 , eq(s(X), 0()) -> false() 606.81/174.02 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.02 , le(0(), Y) -> true() 606.81/174.02 , le(s(X), 0()) -> false() 606.81/174.02 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.02 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.02 , min(cons(0(), nil())) -> 0() 606.81/174.02 , min(cons(s(N), nil())) -> s(N) 606.81/174.02 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.02 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.02 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.03 , replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.03 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.03 Obligation: 606.81/174.03 innermost runtime complexity 606.81/174.03 Answer: 606.81/174.03 YES(O(1),O(n^2)) 606.81/174.03 606.81/174.03 We decompose the input problem according to the dependency graph 606.81/174.03 into the upper component 606.81/174.03 606.81/174.03 { min^#(cons(N, cons(M, L))) -> 606.81/174.03 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.03 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.03 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.03 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 606.81/174.03 and lower component 606.81/174.03 606.81/174.03 { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) } 606.81/174.03 606.81/174.03 Further, following extension rules are added to the lower 606.81/174.03 component. 606.81/174.03 606.81/174.03 { min^#(cons(N, cons(M, L))) -> le^#(N, M) 606.81/174.03 , min^#(cons(N, cons(M, L))) -> 606.81/174.03 ifmin^#(le(N, M), cons(N, cons(M, L))) 606.81/174.03 , ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L)) 606.81/174.03 , ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 606.81/174.03 TcT solves the upper component with certificate YES(O(1),O(n^1)). 606.81/174.03 606.81/174.03 Sub-proof: 606.81/174.03 ---------- 606.81/174.03 We are left with following problem, upon which TcT provides the 606.81/174.03 certificate YES(O(1),O(n^1)). 606.81/174.03 606.81/174.03 Strict DPs: 606.81/174.03 { min^#(cons(N, cons(M, L))) -> 606.81/174.03 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.03 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.03 , ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.03 c_12(min^#(cons(M, L))) } 606.81/174.03 Weak DPs: 606.81/174.03 { selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 Weak Trs: 606.81/174.03 { eq(0(), 0()) -> true() 606.81/174.03 , eq(0(), s(Y)) -> false() 606.81/174.03 , eq(s(X), 0()) -> false() 606.81/174.03 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.03 , le(0(), Y) -> true() 606.81/174.03 , le(s(X), 0()) -> false() 606.81/174.03 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.03 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.03 , min(cons(0(), nil())) -> 0() 606.81/174.03 , min(cons(s(N), nil())) -> s(N) 606.81/174.03 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.03 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.03 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.03 , replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.03 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.03 Obligation: 606.81/174.03 innermost runtime complexity 606.81/174.03 Answer: 606.81/174.03 YES(O(1),O(n^1)) 606.81/174.03 606.81/174.03 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.03 orient following rules strictly. 606.81/174.03 606.81/174.03 DPs: 606.81/174.03 { 2: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.03 c_11(min^#(cons(N, L))) 606.81/174.03 , 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , 8: ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 606.81/174.03 Sub-proof: 606.81/174.03 ---------- 606.81/174.03 The following argument positions are usable: 606.81/174.03 Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1} 606.81/174.03 606.81/174.03 TcT has computed the following constructor-based matrix 606.81/174.03 interpretation satisfying not(EDA). 606.81/174.03 606.81/174.03 [eq](x1, x2) = [0] 606.81/174.03 606.81/174.03 [0] = [0] 606.81/174.03 606.81/174.03 [true] = [0] 606.81/174.03 606.81/174.03 [s](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [false] = [0] 606.81/174.03 606.81/174.03 [le](x1, x2) = [0] 606.81/174.03 606.81/174.03 [min](x1) = [0] 606.81/174.03 606.81/174.03 [cons](x1, x2) = [1] x2 + [1] 606.81/174.03 606.81/174.03 [nil] = [0] 606.81/174.03 606.81/174.03 [ifmin](x1, x2) = [0] 606.81/174.03 606.81/174.03 [replace](x1, x2, x3) = [1] x3 + [0] 606.81/174.03 606.81/174.03 [ifrepl](x1, x2, x3, x4) = [1] x4 + [0] 606.81/174.03 606.81/174.03 [le^#](x1, x2) = [7] x1 + [7] x2 + [7] 606.81/174.03 606.81/174.03 [min^#](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [c_8](x1, x2) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [ifmin^#](x1, x2) = [1] x2 + [0] 606.81/174.03 606.81/174.03 [c_11](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [c_12](x1) = [1] x1 + [1] 606.81/174.03 606.81/174.03 [selsort^#](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [ifselsort^#](x1, x2) = [1] x2 + [0] 606.81/174.03 606.81/174.03 The order satisfies the following ordering constraints: 606.81/174.03 606.81/174.03 [eq(0(), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [eq(0(), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [eq(X, Y)] 606.81/174.03 606.81/174.03 [le(0(), Y)] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [le(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [le(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [le(X, Y)] 606.81/174.03 606.81/174.03 [min(cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.03 606.81/174.03 [min(cons(0(), nil()))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [0()] 606.81/174.03 606.81/174.03 [min(cons(s(N), nil()))] = [0] 606.81/174.03 ? [1] N + [0] 606.81/174.03 = [s(N)] 606.81/174.03 606.81/174.03 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [min(cons(N, L))] 606.81/174.03 606.81/174.03 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [min(cons(M, L))] 606.81/174.03 606.81/174.03 [replace(N, M, cons(K, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.03 606.81/174.03 [replace(N, M, nil())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [nil()] 606.81/174.03 606.81/174.03 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [cons(M, L)] 606.81/174.03 606.81/174.03 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [cons(K, replace(N, M, L))] 606.81/174.03 606.81/174.03 [min^#(cons(N, cons(M, L)))] = [1] L + [2] 606.81/174.03 >= [1] L + [2] 606.81/174.03 = [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))] 606.81/174.03 606.81/174.03 [ifmin^#(true(), cons(N, cons(M, L)))] = [1] L + [2] 606.81/174.03 > [1] L + [1] 606.81/174.03 = [c_11(min^#(cons(N, L)))] 606.81/174.03 606.81/174.03 [ifmin^#(false(), cons(N, cons(M, L)))] = [1] L + [2] 606.81/174.03 >= [1] L + [2] 606.81/174.03 = [c_12(min^#(cons(M, L)))] 606.81/174.03 606.81/174.03 [selsort^#(cons(N, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [min^#(cons(N, L))] 606.81/174.03 606.81/174.03 [selsort^#(cons(N, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))] 606.81/174.03 606.81/174.03 [ifselsort^#(true(), cons(N, L))] = [1] L + [1] 606.81/174.03 > [1] L + [0] 606.81/174.03 = [selsort^#(L)] 606.81/174.03 606.81/174.03 [ifselsort^#(false(), cons(N, L))] = [1] L + [1] 606.81/174.03 >= [1] L + [1] 606.81/174.03 = [min^#(cons(N, L))] 606.81/174.03 606.81/174.03 [ifselsort^#(false(), cons(N, L))] = [1] L + [1] 606.81/174.03 > [1] L + [0] 606.81/174.03 = [selsort^#(replace(min(cons(N, L)), N, L))] 606.81/174.03 606.81/174.03 606.81/174.03 We return to the main proof. Consider the set of all dependency 606.81/174.03 pairs 606.81/174.03 606.81/174.03 : 606.81/174.03 { 1: min^#(cons(N, cons(M, L))) -> 606.81/174.03 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.03 , 2: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.03 c_11(min^#(cons(N, L))) 606.81/174.03 , 3: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.03 c_12(min^#(cons(M, L))) 606.81/174.03 , 4: selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , 5: selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , 7: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , 8: ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 606.81/174.03 Processor 'matrix interpretation of dimension 1' induces the 606.81/174.03 complexity certificate YES(?,O(n^1)) on application of dependency 606.81/174.03 pairs {2,6,8}. These cover all (indirect) predecessors of 606.81/174.03 dependency pairs {2,4,5,6,7,8}, their number of application is 606.81/174.03 equally bounded. The dependency pairs are shifted into the weak 606.81/174.03 component. 606.81/174.03 606.81/174.03 We are left with following problem, upon which TcT provides the 606.81/174.03 certificate YES(O(1),O(n^1)). 606.81/174.03 606.81/174.03 Strict DPs: 606.81/174.03 { min^#(cons(N, cons(M, L))) -> 606.81/174.03 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.03 , ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.03 c_12(min^#(cons(M, L))) } 606.81/174.03 Weak DPs: 606.81/174.03 { ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.03 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 Weak Trs: 606.81/174.03 { eq(0(), 0()) -> true() 606.81/174.03 , eq(0(), s(Y)) -> false() 606.81/174.03 , eq(s(X), 0()) -> false() 606.81/174.03 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.03 , le(0(), Y) -> true() 606.81/174.03 , le(s(X), 0()) -> false() 606.81/174.03 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.03 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.03 , min(cons(0(), nil())) -> 0() 606.81/174.03 , min(cons(s(N), nil())) -> s(N) 606.81/174.03 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.03 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.03 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.03 , replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.03 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.03 Obligation: 606.81/174.03 innermost runtime complexity 606.81/174.03 Answer: 606.81/174.03 YES(O(1),O(n^1)) 606.81/174.03 606.81/174.03 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.03 orient following rules strictly. 606.81/174.03 606.81/174.03 DPs: 606.81/174.03 { 2: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.03 c_12(min^#(cons(M, L))) 606.81/174.03 , 3: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.03 c_11(min^#(cons(N, L))) 606.81/174.03 , 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) } 606.81/174.03 Trs: 606.81/174.03 { replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) } 606.81/174.03 606.81/174.03 Sub-proof: 606.81/174.03 ---------- 606.81/174.03 The following argument positions are usable: 606.81/174.03 Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1} 606.81/174.03 606.81/174.03 TcT has computed the following constructor-based matrix 606.81/174.03 interpretation satisfying not(EDA). 606.81/174.03 606.81/174.03 [eq](x1, x2) = [0] 606.81/174.03 606.81/174.03 [0] = [0] 606.81/174.03 606.81/174.03 [true] = [0] 606.81/174.03 606.81/174.03 [s](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [false] = [0] 606.81/174.03 606.81/174.03 [le](x1, x2) = [0] 606.81/174.03 606.81/174.03 [min](x1) = [0] 606.81/174.03 606.81/174.03 [cons](x1, x2) = [1] x2 + [2] 606.81/174.03 606.81/174.03 [nil] = [0] 606.81/174.03 606.81/174.03 [ifmin](x1, x2) = [0] 606.81/174.03 606.81/174.03 [replace](x1, x2, x3) = [1] x3 + [2] 606.81/174.03 606.81/174.03 [ifrepl](x1, x2, x3, x4) = [1] x4 + [2] 606.81/174.03 606.81/174.03 [le^#](x1, x2) = [7] x1 + [7] x2 + [7] 606.81/174.03 606.81/174.03 [min^#](x1) = [2] x1 + [0] 606.81/174.03 606.81/174.03 [c_8](x1, x2) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [ifmin^#](x1, x2) = [2] x2 + [0] 606.81/174.03 606.81/174.03 [c_11](x1) = [1] x1 + [3] 606.81/174.03 606.81/174.03 [c_12](x1) = [1] x1 + [1] 606.81/174.03 606.81/174.03 [selsort^#](x1) = [2] x1 + [0] 606.81/174.03 606.81/174.03 [ifselsort^#](x1, x2) = [2] x2 + [0] 606.81/174.03 606.81/174.03 The order satisfies the following ordering constraints: 606.81/174.03 606.81/174.03 [eq(0(), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [eq(0(), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [eq(X, Y)] 606.81/174.03 606.81/174.03 [le(0(), Y)] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [le(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [le(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [le(X, Y)] 606.81/174.03 606.81/174.03 [min(cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.03 606.81/174.03 [min(cons(0(), nil()))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [0()] 606.81/174.03 606.81/174.03 [min(cons(s(N), nil()))] = [0] 606.81/174.03 ? [1] N + [0] 606.81/174.03 = [s(N)] 606.81/174.03 606.81/174.03 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [min(cons(N, L))] 606.81/174.03 606.81/174.03 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [min(cons(M, L))] 606.81/174.03 606.81/174.03 [replace(N, M, cons(K, L))] = [1] L + [4] 606.81/174.03 >= [1] L + [4] 606.81/174.03 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.03 606.81/174.03 [replace(N, M, nil())] = [2] 606.81/174.03 > [0] 606.81/174.03 = [nil()] 606.81/174.03 606.81/174.03 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [4] 606.81/174.03 > [1] L + [2] 606.81/174.03 = [cons(M, L)] 606.81/174.03 606.81/174.03 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [4] 606.81/174.03 >= [1] L + [4] 606.81/174.03 = [cons(K, replace(N, M, L))] 606.81/174.03 606.81/174.03 [min^#(cons(N, cons(M, L)))] = [2] L + [8] 606.81/174.03 >= [2] L + [8] 606.81/174.03 = [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))] 606.81/174.03 606.81/174.03 [ifmin^#(true(), cons(N, cons(M, L)))] = [2] L + [8] 606.81/174.03 > [2] L + [7] 606.81/174.03 = [c_11(min^#(cons(N, L)))] 606.81/174.03 606.81/174.03 [ifmin^#(false(), cons(N, cons(M, L)))] = [2] L + [8] 606.81/174.03 > [2] L + [5] 606.81/174.03 = [c_12(min^#(cons(M, L)))] 606.81/174.03 606.81/174.03 [selsort^#(cons(N, L))] = [2] L + [4] 606.81/174.03 >= [2] L + [4] 606.81/174.03 = [min^#(cons(N, L))] 606.81/174.03 606.81/174.03 [selsort^#(cons(N, L))] = [2] L + [4] 606.81/174.03 >= [2] L + [4] 606.81/174.03 = [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))] 606.81/174.03 606.81/174.03 [ifselsort^#(true(), cons(N, L))] = [2] L + [4] 606.81/174.03 > [2] L + [0] 606.81/174.03 = [selsort^#(L)] 606.81/174.03 606.81/174.03 [ifselsort^#(false(), cons(N, L))] = [2] L + [4] 606.81/174.03 >= [2] L + [4] 606.81/174.03 = [min^#(cons(N, L))] 606.81/174.03 606.81/174.03 [ifselsort^#(false(), cons(N, L))] = [2] L + [4] 606.81/174.03 >= [2] L + [4] 606.81/174.03 = [selsort^#(replace(min(cons(N, L)), N, L))] 606.81/174.03 606.81/174.03 606.81/174.03 The strictly oriented rules are moved into the weak component. 606.81/174.03 606.81/174.03 We are left with following problem, upon which TcT provides the 606.81/174.03 certificate YES(O(1),O(n^1)). 606.81/174.03 606.81/174.03 Strict DPs: 606.81/174.03 { min^#(cons(N, cons(M, L))) -> 606.81/174.03 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) } 606.81/174.03 Weak DPs: 606.81/174.03 { ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.03 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.03 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , selsort^#(cons(N, L)) -> 606.81/174.03 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.03 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.03 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.03 Weak Trs: 606.81/174.03 { eq(0(), 0()) -> true() 606.81/174.03 , eq(0(), s(Y)) -> false() 606.81/174.03 , eq(s(X), 0()) -> false() 606.81/174.03 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.03 , le(0(), Y) -> true() 606.81/174.03 , le(s(X), 0()) -> false() 606.81/174.03 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.03 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.03 , min(cons(0(), nil())) -> 0() 606.81/174.03 , min(cons(s(N), nil())) -> s(N) 606.81/174.03 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.03 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.03 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.03 , replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.03 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.03 Obligation: 606.81/174.03 innermost runtime complexity 606.81/174.03 Answer: 606.81/174.03 YES(O(1),O(n^1)) 606.81/174.03 606.81/174.03 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.03 orient following rules strictly. 606.81/174.03 606.81/174.03 DPs: 606.81/174.03 { 2: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.03 c_11(min^#(cons(N, L))) 606.81/174.03 , 3: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.03 c_12(min^#(cons(M, L))) 606.81/174.03 , 4: selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.03 , 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.03 , 7: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) } 606.81/174.03 Trs: 606.81/174.03 { replace(N, M, nil()) -> nil() 606.81/174.03 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) } 606.81/174.03 606.81/174.03 Sub-proof: 606.81/174.03 ---------- 606.81/174.03 The following argument positions are usable: 606.81/174.03 Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1} 606.81/174.03 606.81/174.03 TcT has computed the following constructor-based matrix 606.81/174.03 interpretation satisfying not(EDA). 606.81/174.03 606.81/174.03 [eq](x1, x2) = [0] 606.81/174.03 606.81/174.03 [0] = [0] 606.81/174.03 606.81/174.03 [true] = [0] 606.81/174.03 606.81/174.03 [s](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [false] = [0] 606.81/174.03 606.81/174.03 [le](x1, x2) = [0] 606.81/174.03 606.81/174.03 [min](x1) = [0] 606.81/174.03 606.81/174.03 [cons](x1, x2) = [1] x2 + [4] 606.81/174.03 606.81/174.03 [nil] = [4] 606.81/174.03 606.81/174.03 [ifmin](x1, x2) = [0] 606.81/174.03 606.81/174.03 [replace](x1, x2, x3) = [1] x3 + [4] 606.81/174.03 606.81/174.03 [ifrepl](x1, x2, x3, x4) = [1] x4 + [4] 606.81/174.03 606.81/174.03 [le^#](x1, x2) = [7] x1 + [7] x2 + [7] 606.81/174.03 606.81/174.03 [min^#](x1) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [c_8](x1, x2) = [1] x1 + [0] 606.81/174.03 606.81/174.03 [ifmin^#](x1, x2) = [1] x2 + [0] 606.81/174.03 606.81/174.03 [c_11](x1) = [1] x1 + [3] 606.81/174.03 606.81/174.03 [c_12](x1) = [1] x1 + [3] 606.81/174.03 606.81/174.03 [selsort^#](x1) = [1] x1 + [2] 606.81/174.03 606.81/174.03 [ifselsort^#](x1, x2) = [1] x2 + [2] 606.81/174.03 606.81/174.03 The order satisfies the following ordering constraints: 606.81/174.03 606.81/174.03 [eq(0(), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [eq(0(), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [eq(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [eq(X, Y)] 606.81/174.03 606.81/174.03 [le(0(), Y)] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [true()] 606.81/174.03 606.81/174.03 [le(s(X), 0())] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [false()] 606.81/174.03 606.81/174.03 [le(s(X), s(Y))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [le(X, Y)] 606.81/174.03 606.81/174.03 [min(cons(N, cons(M, L)))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.03 606.81/174.03 [min(cons(0(), nil()))] = [0] 606.81/174.03 >= [0] 606.81/174.03 = [0()] 606.81/174.03 606.81/174.03 [min(cons(s(N), nil()))] = [0] 606.81/174.04 ? [1] N + [0] 606.81/174.04 = [s(N)] 606.81/174.04 606.81/174.04 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [min(cons(N, L))] 606.81/174.04 606.81/174.04 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [min(cons(M, L))] 606.81/174.04 606.81/174.04 [replace(N, M, cons(K, L))] = [1] L + [8] 606.81/174.04 >= [1] L + [8] 606.81/174.04 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.04 606.81/174.04 [replace(N, M, nil())] = [8] 606.81/174.04 > [4] 606.81/174.04 = [nil()] 606.81/174.04 606.81/174.04 [ifrepl(true(), N, M, cons(K, L))] = [1] L + [8] 606.81/174.04 > [1] L + [4] 606.81/174.04 = [cons(M, L)] 606.81/174.04 606.81/174.04 [ifrepl(false(), N, M, cons(K, L))] = [1] L + [8] 606.81/174.04 >= [1] L + [8] 606.81/174.04 = [cons(K, replace(N, M, L))] 606.81/174.04 606.81/174.04 [min^#(cons(N, cons(M, L)))] = [1] L + [8] 606.81/174.04 >= [1] L + [8] 606.81/174.04 = [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))] 606.81/174.04 606.81/174.04 [ifmin^#(true(), cons(N, cons(M, L)))] = [1] L + [8] 606.81/174.04 > [1] L + [7] 606.81/174.04 = [c_11(min^#(cons(N, L)))] 606.81/174.04 606.81/174.04 [ifmin^#(false(), cons(N, cons(M, L)))] = [1] L + [8] 606.81/174.04 > [1] L + [7] 606.81/174.04 = [c_12(min^#(cons(M, L)))] 606.81/174.04 606.81/174.04 [selsort^#(cons(N, L))] = [1] L + [6] 606.81/174.04 > [1] L + [4] 606.81/174.04 = [min^#(cons(N, L))] 606.81/174.04 606.81/174.04 [selsort^#(cons(N, L))] = [1] L + [6] 606.81/174.04 >= [1] L + [6] 606.81/174.04 = [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))] 606.81/174.04 606.81/174.04 [ifselsort^#(true(), cons(N, L))] = [1] L + [6] 606.81/174.04 > [1] L + [2] 606.81/174.04 = [selsort^#(L)] 606.81/174.04 606.81/174.04 [ifselsort^#(false(), cons(N, L))] = [1] L + [6] 606.81/174.04 > [1] L + [4] 606.81/174.04 = [min^#(cons(N, L))] 606.81/174.04 606.81/174.04 [ifselsort^#(false(), cons(N, L))] = [1] L + [6] 606.81/174.04 >= [1] L + [6] 606.81/174.04 = [selsort^#(replace(min(cons(N, L)), N, L))] 606.81/174.04 606.81/174.04 606.81/174.04 We return to the main proof. Consider the set of all dependency 606.81/174.04 pairs 606.81/174.04 606.81/174.04 : 606.81/174.04 { 1: min^#(cons(N, cons(M, L))) -> 606.81/174.04 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.04 , 2: ifmin^#(true(), cons(N, cons(M, L))) -> 606.81/174.04 c_11(min^#(cons(N, L))) 606.81/174.04 , 3: ifmin^#(false(), cons(N, cons(M, L))) -> 606.81/174.04 c_12(min^#(cons(M, L))) 606.81/174.04 , 4: selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , 5: selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , 7: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , 8: ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 606.81/174.04 Processor 'matrix interpretation of dimension 1' induces the 606.81/174.04 complexity certificate YES(?,O(n^1)) on application of dependency 606.81/174.04 pairs {2,3,4,6,7}. These cover all (indirect) predecessors of 606.81/174.04 dependency pairs {1,2,3,4,6,7}, their number of application is 606.81/174.04 equally bounded. The dependency pairs are shifted into the weak 606.81/174.04 component. 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Weak DPs: 606.81/174.04 { min^#(cons(N, cons(M, L))) -> 606.81/174.04 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.04 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.04 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.04 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 Weak Trs: 606.81/174.04 { eq(0(), 0()) -> true() 606.81/174.04 , eq(0(), s(Y)) -> false() 606.81/174.04 , eq(s(X), 0()) -> false() 606.81/174.04 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.04 , le(0(), Y) -> true() 606.81/174.04 , le(s(X), 0()) -> false() 606.81/174.04 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.04 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , min(cons(0(), nil())) -> 0() 606.81/174.04 , min(cons(s(N), nil())) -> s(N) 606.81/174.04 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.04 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.04 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.04 , replace(N, M, nil()) -> nil() 606.81/174.04 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.04 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 The following weak DPs constitute a sub-graph of the DG that is 606.81/174.04 closed under successors. The DPs are removed. 606.81/174.04 606.81/174.04 { min^#(cons(N, cons(M, L))) -> 606.81/174.04 c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M)) 606.81/174.04 , ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L))) 606.81/174.04 , ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L))) 606.81/174.04 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Weak Trs: 606.81/174.04 { eq(0(), 0()) -> true() 606.81/174.04 , eq(0(), s(Y)) -> false() 606.81/174.04 , eq(s(X), 0()) -> false() 606.81/174.04 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.04 , le(0(), Y) -> true() 606.81/174.04 , le(s(X), 0()) -> false() 606.81/174.04 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.04 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , min(cons(0(), nil())) -> 0() 606.81/174.04 , min(cons(s(N), nil())) -> s(N) 606.81/174.04 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.04 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.04 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.04 , replace(N, M, nil()) -> nil() 606.81/174.04 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.04 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 No rule is usable, rules are removed from the input problem. 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Rules: Empty 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 Empty rules are trivially bounded 606.81/174.04 606.81/174.04 We return to the main proof. 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(n^1)). 606.81/174.04 606.81/174.04 Strict DPs: { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) } 606.81/174.04 Weak DPs: 606.81/174.04 { min^#(cons(N, cons(M, L))) -> le^#(N, M) 606.81/174.04 , min^#(cons(N, cons(M, L))) -> 606.81/174.04 ifmin^#(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L)) 606.81/174.04 , ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 Weak Trs: 606.81/174.04 { eq(0(), 0()) -> true() 606.81/174.04 , eq(0(), s(Y)) -> false() 606.81/174.04 , eq(s(X), 0()) -> false() 606.81/174.04 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.04 , le(0(), Y) -> true() 606.81/174.04 , le(s(X), 0()) -> false() 606.81/174.04 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.04 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , min(cons(0(), nil())) -> 0() 606.81/174.04 , min(cons(s(N), nil())) -> s(N) 606.81/174.04 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.04 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.04 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.04 , replace(N, M, nil()) -> nil() 606.81/174.04 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.04 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(n^1)) 606.81/174.04 606.81/174.04 We use the processor 'matrix interpretation of dimension 1' to 606.81/174.04 orient following rules strictly. 606.81/174.04 606.81/174.04 DPs: 606.81/174.04 { 1: le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) } 606.81/174.04 606.81/174.04 Sub-proof: 606.81/174.04 ---------- 606.81/174.04 The following argument positions are usable: 606.81/174.04 Uargs(c_7) = {1} 606.81/174.04 606.81/174.04 TcT has computed the following constructor-based matrix 606.81/174.04 interpretation satisfying not(EDA). 606.81/174.04 606.81/174.04 [eq](x1, x2) = [0] 606.81/174.04 606.81/174.04 [0] = [0] 606.81/174.04 606.81/174.04 [true] = [0] 606.81/174.04 606.81/174.04 [s](x1) = [1] x1 + [4] 606.81/174.04 606.81/174.04 [false] = [0] 606.81/174.04 606.81/174.04 [le](x1, x2) = [0] 606.81/174.04 606.81/174.04 [min](x1) = [0] 606.81/174.04 606.81/174.04 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 606.81/174.04 606.81/174.04 [nil] = [0] 606.81/174.04 606.81/174.04 [ifmin](x1, x2) = [0] 606.81/174.04 606.81/174.04 [replace](x1, x2, x3) = [1] x2 + [1] x3 + [0] 606.81/174.04 606.81/174.04 [ifrepl](x1, x2, x3, x4) = [1] x3 + [1] x4 + [0] 606.81/174.04 606.81/174.04 [le^#](x1, x2) = [1] x1 + [1] x2 + [0] 606.81/174.04 606.81/174.04 [c_7](x1) = [1] x1 + [5] 606.81/174.04 606.81/174.04 [min^#](x1) = [4] x1 + [0] 606.81/174.04 606.81/174.04 [ifmin^#](x1, x2) = [4] x2 + [0] 606.81/174.04 606.81/174.04 [selsort^#](x1) = [4] x1 + [0] 606.81/174.04 606.81/174.04 [ifselsort^#](x1, x2) = [4] x2 + [0] 606.81/174.04 606.81/174.04 The order satisfies the following ordering constraints: 606.81/174.04 606.81/174.04 [eq(0(), 0())] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [true()] 606.81/174.04 606.81/174.04 [eq(0(), s(Y))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [false()] 606.81/174.04 606.81/174.04 [eq(s(X), 0())] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [false()] 606.81/174.04 606.81/174.04 [eq(s(X), s(Y))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [eq(X, Y)] 606.81/174.04 606.81/174.04 [le(0(), Y)] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [true()] 606.81/174.04 606.81/174.04 [le(s(X), 0())] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [false()] 606.81/174.04 606.81/174.04 [le(s(X), s(Y))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [le(X, Y)] 606.81/174.04 606.81/174.04 [min(cons(N, cons(M, L)))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [ifmin(le(N, M), cons(N, cons(M, L)))] 606.81/174.04 606.81/174.04 [min(cons(0(), nil()))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [0()] 606.81/174.04 606.81/174.04 [min(cons(s(N), nil()))] = [0] 606.81/174.04 ? [1] N + [4] 606.81/174.04 = [s(N)] 606.81/174.04 606.81/174.04 [ifmin(true(), cons(N, cons(M, L)))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [min(cons(N, L))] 606.81/174.04 606.81/174.04 [ifmin(false(), cons(N, cons(M, L)))] = [0] 606.81/174.04 >= [0] 606.81/174.04 = [min(cons(M, L))] 606.81/174.04 606.81/174.04 [replace(N, M, cons(K, L))] = [1] M + [1] L + [1] K + [0] 606.81/174.04 >= [1] M + [1] L + [1] K + [0] 606.81/174.04 = [ifrepl(eq(N, K), N, M, cons(K, L))] 606.81/174.04 606.81/174.04 [replace(N, M, nil())] = [1] M + [0] 606.81/174.04 >= [0] 606.81/174.04 = [nil()] 606.81/174.04 606.81/174.04 [ifrepl(true(), N, M, cons(K, L))] = [1] M + [1] L + [1] K + [0] 606.81/174.04 >= [1] M + [1] L + [0] 606.81/174.04 = [cons(M, L)] 606.81/174.04 606.81/174.04 [ifrepl(false(), N, M, cons(K, L))] = [1] M + [1] L + [1] K + [0] 606.81/174.04 >= [1] M + [1] L + [1] K + [0] 606.81/174.04 = [cons(K, replace(N, M, L))] 606.81/174.04 606.81/174.04 [le^#(s(X), s(Y))] = [1] Y + [1] X + [8] 606.81/174.04 > [1] Y + [1] X + [5] 606.81/174.04 = [c_7(le^#(X, Y))] 606.81/174.04 606.81/174.04 [min^#(cons(N, cons(M, L)))] = [4] N + [4] M + [4] L + [0] 606.81/174.04 >= [1] N + [1] M + [0] 606.81/174.04 = [le^#(N, M)] 606.81/174.04 606.81/174.04 [min^#(cons(N, cons(M, L)))] = [4] N + [4] M + [4] L + [0] 606.81/174.04 >= [4] N + [4] M + [4] L + [0] 606.81/174.04 = [ifmin^#(le(N, M), cons(N, cons(M, L)))] 606.81/174.04 606.81/174.04 [ifmin^#(true(), cons(N, cons(M, L)))] = [4] N + [4] M + [4] L + [0] 606.81/174.04 >= [4] N + [4] L + [0] 606.81/174.04 = [min^#(cons(N, L))] 606.81/174.04 606.81/174.04 [ifmin^#(false(), cons(N, cons(M, L)))] = [4] N + [4] M + [4] L + [0] 606.81/174.04 >= [4] M + [4] L + [0] 606.81/174.04 = [min^#(cons(M, L))] 606.81/174.04 606.81/174.04 [selsort^#(cons(N, L))] = [4] N + [4] L + [0] 606.81/174.04 >= [4] N + [4] L + [0] 606.81/174.04 = [min^#(cons(N, L))] 606.81/174.04 606.81/174.04 [selsort^#(cons(N, L))] = [4] N + [4] L + [0] 606.81/174.04 >= [4] N + [4] L + [0] 606.81/174.04 = [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))] 606.81/174.04 606.81/174.04 [ifselsort^#(true(), cons(N, L))] = [4] N + [4] L + [0] 606.81/174.04 >= [4] L + [0] 606.81/174.04 = [selsort^#(L)] 606.81/174.04 606.81/174.04 [ifselsort^#(false(), cons(N, L))] = [4] N + [4] L + [0] 606.81/174.04 >= [4] N + [4] L + [0] 606.81/174.04 = [min^#(cons(N, L))] 606.81/174.04 606.81/174.04 [ifselsort^#(false(), cons(N, L))] = [4] N + [4] L + [0] 606.81/174.04 >= [4] N + [4] L + [0] 606.81/174.04 = [selsort^#(replace(min(cons(N, L)), N, L))] 606.81/174.04 606.81/174.04 606.81/174.04 The strictly oriented rules are moved into the weak component. 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Weak DPs: 606.81/174.04 { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.04 , min^#(cons(N, cons(M, L))) -> le^#(N, M) 606.81/174.04 , min^#(cons(N, cons(M, L))) -> 606.81/174.04 ifmin^#(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L)) 606.81/174.04 , ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 Weak Trs: 606.81/174.04 { eq(0(), 0()) -> true() 606.81/174.04 , eq(0(), s(Y)) -> false() 606.81/174.04 , eq(s(X), 0()) -> false() 606.81/174.04 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.04 , le(0(), Y) -> true() 606.81/174.04 , le(s(X), 0()) -> false() 606.81/174.04 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.04 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , min(cons(0(), nil())) -> 0() 606.81/174.04 , min(cons(s(N), nil())) -> s(N) 606.81/174.04 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.04 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.04 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.04 , replace(N, M, nil()) -> nil() 606.81/174.04 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.04 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 The following weak DPs constitute a sub-graph of the DG that is 606.81/174.04 closed under successors. The DPs are removed. 606.81/174.04 606.81/174.04 { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) 606.81/174.04 , min^#(cons(N, cons(M, L))) -> le^#(N, M) 606.81/174.04 , min^#(cons(N, cons(M, L))) -> 606.81/174.04 ifmin^#(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L)) 606.81/174.04 , ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , selsort^#(cons(N, L)) -> 606.81/174.04 ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)) 606.81/174.04 , ifselsort^#(true(), cons(N, L)) -> selsort^#(L) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L)) 606.81/174.04 , ifselsort^#(false(), cons(N, L)) -> 606.81/174.04 selsort^#(replace(min(cons(N, L)), N, L)) } 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Weak Trs: 606.81/174.04 { eq(0(), 0()) -> true() 606.81/174.04 , eq(0(), s(Y)) -> false() 606.81/174.04 , eq(s(X), 0()) -> false() 606.81/174.04 , eq(s(X), s(Y)) -> eq(X, Y) 606.81/174.04 , le(0(), Y) -> true() 606.81/174.04 , le(s(X), 0()) -> false() 606.81/174.04 , le(s(X), s(Y)) -> le(X, Y) 606.81/174.04 , min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) 606.81/174.04 , min(cons(0(), nil())) -> 0() 606.81/174.04 , min(cons(s(N), nil())) -> s(N) 606.81/174.04 , ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L)) 606.81/174.04 , ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L)) 606.81/174.04 , replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 606.81/174.04 , replace(N, M, nil()) -> nil() 606.81/174.04 , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 606.81/174.04 , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) } 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 No rule is usable, rules are removed from the input problem. 606.81/174.04 606.81/174.04 We are left with following problem, upon which TcT provides the 606.81/174.04 certificate YES(O(1),O(1)). 606.81/174.04 606.81/174.04 Rules: Empty 606.81/174.04 Obligation: 606.81/174.04 innermost runtime complexity 606.81/174.04 Answer: 606.81/174.04 YES(O(1),O(1)) 606.81/174.04 606.81/174.04 Empty rules are trivially bounded 606.81/174.04 606.81/174.04 Hurray, we answered YES(O(1),O(n^3)) 607.07/174.23 EOF