```We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, selsort(nil()) -> nil()
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^3))

We add the following dependency tuples:

Strict DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(Y)) -> c_2()
, eq^#(s(X), 0()) -> c_3()
, eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(0(), Y) -> c_5()
, le^#(s(X), 0()) -> c_6()
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, min^#(cons(0(), nil())) -> c_9()
, min^#(cons(s(N), nil())) -> c_10()
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, replace^#(N, M, nil()) -> c_14()
, ifrepl^#(true(), N, M, cons(K, L)) -> c_15()
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, selsort^#(nil()) -> c_18()
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(Y)) -> c_2()
, eq^#(s(X), 0()) -> c_3()
, eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(0(), Y) -> c_5()
, le^#(s(X), 0()) -> c_6()
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, min^#(cons(0(), nil())) -> c_9()
, min^#(cons(s(N), nil())) -> c_10()
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, replace^#(N, M, nil()) -> c_14()
, ifrepl^#(true(), N, M, cons(K, L)) -> c_15()
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, selsort^#(nil()) -> c_18()
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, selsort(nil()) -> nil()
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^3))

We estimate the number of application of {1,2,3,5,6,9,10,14,15,18}
by applications of Pre({1,2,3,5,6,9,10,14,15,18}) =
{4,7,8,11,12,13,16,17,19,20}. Here rules are labeled as follows:

DPs:
{ 1: eq^#(0(), 0()) -> c_1()
, 2: eq^#(0(), s(Y)) -> c_2()
, 3: eq^#(s(X), 0()) -> c_3()
, 4: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, 5: le^#(0(), Y) -> c_5()
, 6: le^#(s(X), 0()) -> c_6()
, 7: le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, 8: min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, 9: min^#(cons(0(), nil())) -> c_9()
, 10: min^#(cons(s(N), nil())) -> c_10()
, 11: ifmin^#(true(), cons(N, cons(M, L))) ->
c_11(min^#(cons(N, L)))
, 12: ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L)))
, 13: replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, 14: replace^#(N, M, nil()) -> c_14()
, 15: ifrepl^#(true(), N, M, cons(K, L)) -> c_15()
, 16: ifrepl^#(false(), N, M, cons(K, L)) ->
c_16(replace^#(N, M, L))
, 17: selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, 18: selsort^#(nil()) -> c_18()
, 19: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, 20: ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(Y)) -> c_2()
, eq^#(s(X), 0()) -> c_3()
, le^#(0(), Y) -> c_5()
, le^#(s(X), 0()) -> c_6()
, min^#(cons(0(), nil())) -> c_9()
, min^#(cons(s(N), nil())) -> c_10()
, replace^#(N, M, nil()) -> c_14()
, ifrepl^#(true(), N, M, cons(K, L)) -> c_15()
, selsort^#(nil()) -> c_18() }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, selsort(nil()) -> nil()
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^3))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(Y)) -> c_2()
, eq^#(s(X), 0()) -> c_3()
, le^#(0(), Y) -> c_5()
, le^#(s(X), 0()) -> c_6()
, min^#(cons(0(), nil())) -> c_9()
, min^#(cons(s(N), nil())) -> c_10()
, replace^#(N, M, nil()) -> c_14()
, ifrepl^#(true(), N, M, cons(K, L)) -> c_15()
, selsort^#(nil()) -> c_18() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, selsort(nil()) -> nil()
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^3))

We replace rewrite rules by usable rules:

Weak Usable Rules:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).

Strict DPs:
{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^3))

We decompose the input problem according to the dependency graph
into the upper component

{ selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }

and lower component

{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) }

Further, following extension rules are added to the lower
component.

{ selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L)
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
{ selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
{ 2: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, 3: ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Trs:
{ min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N) }

Sub-proof:
----------
The following argument positions are usable:
Uargs(c_17) = {1, 2}, Uargs(c_19) = {1}, Uargs(c_20) = {2, 3}

TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).

[eq](x1, x2) = [0]

[0] = [1]

[true] = [0]

[s](x1) = [0]

[false] = [0]

[le](x1, x2) = [0]

[min](x1) = [6]

[cons](x1, x2) = [1] x2 + [3]

[nil] = [0]

[ifmin](x1, x2) = [6]

[replace](x1, x2, x3) = [1] x3 + [0]

[ifrepl](x1, x2, x3, x4) = [1] x4 + [0]

[eq^#](x1, x2) = [0]

[min^#](x1) = [1] x1 + [2]

[replace^#](x1, x2, x3) = [1] x1 + [0]

[selsort^#](x1) = [4] x1 + [0]

[c_17](x1, x2, x3) = [1] x1 + [1] x2 + [0]

[ifselsort^#](x1, x2) = [4] x1 + [4] x2 + [0]

[c_19](x1) = [1] x1 + [0]

[c_20](x1, x2, x3, x4) = [1] x2 + [1] x3 + [5]

The order satisfies the following ordering constraints:

[eq(0(), 0())] =  [0]
>= [0]
=  [true()]

[eq(0(), s(Y))] =  [0]
>= [0]
=  [false()]

[eq(s(X), 0())] =  [0]
>= [0]
=  [false()]

[eq(s(X), s(Y))] =  [0]
>= [0]
=  [eq(X, Y)]

[le(0(), Y)] =  [0]
>= [0]
=  [true()]

[le(s(X), 0())] =  [0]
>= [0]
=  [false()]

[le(s(X), s(Y))] =  [0]
>= [0]
=  [le(X, Y)]

[min(cons(N, cons(M, L)))] =  [6]
>= [6]
=  [ifmin(le(N, M), cons(N, cons(M, L)))]

[min(cons(0(), nil()))] =  [6]
>  [1]
=  [0()]

[min(cons(s(N), nil()))] =  [6]
>  [0]
=  [s(N)]

[ifmin(true(), cons(N, cons(M, L)))] =  [6]
>= [6]
=  [min(cons(N, L))]

[ifmin(false(), cons(N, cons(M, L)))] =  [6]
>= [6]
=  [min(cons(M, L))]

[replace(N, M, cons(K, L))] =  [1] L + [3]
>= [1] L + [3]
=  [ifrepl(eq(N, K), N, M, cons(K, L))]

[replace(N, M, nil())] =  [0]
>= [0]
=  [nil()]

[ifrepl(true(), N, M, cons(K, L))] =  [1] L + [3]
>= [1] L + [3]
=  [cons(M, L)]

[ifrepl(false(), N, M, cons(K, L))] =  [1] L + [3]
>= [1] L + [3]
=  [cons(K, replace(N, M, L))]

[selsort^#(cons(N, L))] =  [4] L + [12]
>= [4] L + [12]
=  [c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))]

[ifselsort^#(true(), cons(N, L))] =  [4] L + [12]
>  [4] L + [0]
=  [c_19(selsort^#(L))]

[ifselsort^#(false(), cons(N, L))] =  [4] L + [12]
>  [4] L + [11]
=  [c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L)))]

We return to the main proof. Consider the set of all dependency
pairs

:
{ 1: selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, 2: ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, 3: ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,3}. These cover all (indirect) predecessors of dependency
pairs {1,2,3}, their number of application is equally bounded. The
dependency pairs are shifted into the weak component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
{ selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ selsort^#(cons(N, L)) ->
c_17(ifselsort^#(eq(N, min(cons(N, L))), cons(N, L)),
eq^#(N, min(cons(N, L))),
min^#(cons(N, L)))
, ifselsort^#(true(), cons(N, L)) -> c_19(selsort^#(L))
, ifselsort^#(false(), cons(N, L)) ->
c_20(min^#(cons(N, L)),
selsort^#(replace(min(cons(N, L)), N, L)),
replace^#(min(cons(N, L)), N, L),
min^#(cons(N, L))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
innermost runtime complexity
YES(O(1),O(1))

Empty rules are trivially bounded

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L)) }
Weak DPs:
{ selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L)
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^2))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

DPs:
{ 1: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, 6: replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, 7: ifrepl^#(false(), N, M, cons(K, L)) ->
c_16(replace^#(N, M, L))
, 8: selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, 9: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 11: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 12: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 13: ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L)
, 14: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }

Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1, 2},
Uargs(c_11) = {1}, Uargs(c_12) = {1}, Uargs(c_13) = {1, 2},
Uargs(c_16) = {1}

TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).

[eq](x1, x2) = [1 0] x2 + [0]
[0 0]      [2]

[0] = [1]
[1]

[true] = [1]
[2]

[s](x1) = [1 0] x1 + [1]
[0 0]      [0]

[false] = [1]
[2]

[le](x1, x2) = [1]
[2]

[min](x1) = [0 3] x1 + [0]
[0 0]      [2]

[cons](x1, x2) = [0 0] x1 + [0 1] x2 + [1]
[1 0]      [0 1]      [2]

[nil] = [5]
[0]

[ifmin](x1, x2) = [0 0] x1 + [0 3] x2 + [0]
[2 0]      [0 0]      [0]

[replace](x1, x2, x3) = [1 1] x2 + [1 4] x3 + [0]
[1 0]      [0 1]      [0]

[ifrepl](x1, x2, x3, x4) = [1 0] x1 + [1 1] x3 + [1 0] x4 + [0]
[0 0]      [1 0]      [0 1]      [0]

[eq^#](x1, x2) = [2 0] x2 + [2]
[0 0]      [0]

[c_4](x1) = [1 0] x1 + [0]
[0 0]      [0]

[le^#](x1, x2) = [0 0] x1 + [0]
[0 1]      [2]

[c_7](x1) = [3 0] x1 + [0]
[0 0]      [0]

[min^#](x1) = [4]
[0]

[c_8](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0]      [0 0]      [0]

[ifmin^#](x1, x2) = [4 0] x1 + [0]
[0 0]      [0]

[c_11](x1) = [1 0] x1 + [0]
[0 0]      [0]

[c_12](x1) = [1 0] x1 + [0]
[0 0]      [0]

[replace^#](x1, x2, x3) = [0 5] x3 + [5]
[0 0]      [0]

[c_13](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0]      [0 0]      [0]

[ifrepl^#](x1, x2, x3, x4) = [0 0] x1 + [3 2] x4 + [0]
[1 0]      [0 0]      [0]

[c_16](x1) = [1 0] x1 + [0]
[0 0]      [0]

[selsort^#](x1) = [0 7] x1 + [1]
[0 3]      [5]

[ifselsort^#](x1, x2) = [0 0] x1 + [0 7] x2 + [1]
[0 1]      [0 3]      [1]

The order satisfies the following ordering constraints:

[eq(0(), 0())] =  [1]
[2]
>= [1]
[2]
=  [true()]

[eq(0(), s(Y))] =  [1 0] Y + [1]
[0 0]     [2]
>= [1]
[2]
=  [false()]

[eq(s(X), 0())] =  [1]
[2]
>= [1]
[2]
=  [false()]

[eq(s(X), s(Y))] =  [1 0] Y + [1]
[0 0]     [2]
>  [1 0] Y + [0]
[0 0]     [2]
=  [eq(X, Y)]

[le(0(), Y)] =  [1]
[2]
>= [1]
[2]
=  [true()]

[le(s(X), 0())] =  [1]
[2]
>= [1]
[2]
=  [false()]

[le(s(X), s(Y))] =  [1]
[2]
>= [1]
[2]
=  [le(X, Y)]

[min(cons(N, cons(M, L)))] =  [3 0] N + [3 0] M + [0 3] L + [12]
[0 0]     [0 0]     [0 0]     [2]
>= [3 0] N + [3 0] M + [0 3] L + [12]
[0 0]     [0 0]     [0 0]     [2]
=  [ifmin(le(N, M), cons(N, cons(M, L)))]

[min(cons(0(), nil()))] =  [9]
[2]
>  [1]
[1]
=  [0()]

[min(cons(s(N), nil()))] =  [3 0] N + [9]
[0 0]     [2]
>  [1 0] N + [1]
[0 0]     [0]
=  [s(N)]

[ifmin(true(), cons(N, cons(M, L)))] =  [3 0] N + [3 0] M + [0 3] L + [12]
[0 0]     [0 0]     [0 0]     [2]
>  [3 0] N + [0 3] L + [6]
[0 0]     [0 0]     [2]
=  [min(cons(N, L))]

[ifmin(false(), cons(N, cons(M, L)))] =  [3 0] N + [3 0] M + [0 3] L + [12]
[0 0]     [0 0]     [0 0]     [2]
>  [3 0] M + [0 3] L + [6]
[0 0]     [0 0]     [2]
=  [min(cons(M, L))]

[replace(N, M, cons(K, L))] =  [1 1] M + [0 5] L + [4 0] K + [9]
[1 0]     [0 1]     [1 0]     [2]
>  [1 1] M + [0 1] L + [1 0] K + [1]
[1 0]     [0 1]     [1 0]     [2]
=  [ifrepl(eq(N, K), N, M, cons(K, L))]

[replace(N, M, nil())] =  [1 1] M + [5]
[1 0]     [0]
>= [5]
[0]
=  [nil()]

[ifrepl(true(), N, M, cons(K, L))] =  [1 1] M + [0 1] L + [0 0] K + [2]
[1 0]     [0 1]     [1 0]     [2]
>  [0 0] M + [0 1] L + [1]
[1 0]     [0 1]     [2]
=  [cons(M, L)]

[ifrepl(false(), N, M, cons(K, L))] =  [1 1] M + [0 1] L + [0 0] K + [2]
[1 0]     [0 1]     [1 0]     [2]
>  [1 0] M + [0 1] L + [0 0] K + [1]
[1 0]     [0 1]     [1 0]     [2]
=  [cons(K, replace(N, M, L))]

[eq^#(s(X), s(Y))] =  [2 0] Y + [4]
[0 0]     [0]
>  [2 0] Y + [2]
[0 0]     [0]
=  [c_4(eq^#(X, Y))]

[le^#(s(X), s(Y))] =  [0]
[2]
>= [0]
[0]
=  [c_7(le^#(X, Y))]

[min^#(cons(N, cons(M, L)))] =  [4]
[0]
>= [4]
[0]
=  [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))]

[ifmin^#(true(), cons(N, cons(M, L)))] =  [4]
[0]
>= [4]
[0]
=  [c_11(min^#(cons(N, L)))]

[ifmin^#(false(), cons(N, cons(M, L)))] =  [4]
[0]
>= [4]
[0]
=  [c_12(min^#(cons(M, L)))]

[replace^#(N, M, cons(K, L))] =  [0 5] L + [5 0] K + [15]
[0 0]     [0 0]     [0]
>  [0 5] L + [5 0] K + [10]
[0 0]     [0 0]     [0]
=  [c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))]

[ifrepl^#(false(), N, M, cons(K, L))] =  [0 5] L + [2 0] K + [7]
[0 0]     [0 0]     [1]
>  [0 5] L + [5]
[0 0]     [0]
=  [c_16(replace^#(N, M, L))]

[selsort^#(cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [11]
>  [6 0] N + [0 6] L + [14]
[0 0]     [0 0]     [0]
=  [eq^#(N, min(cons(N, L)))]

[selsort^#(cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [11]
>  [4]
[0]
=  [min^#(cons(N, L))]

[selsort^#(cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [11]
>= [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [9]
=  [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))]

[ifselsort^#(true(), cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [9]
>  [0 7] L + [1]
[0 3]     [5]
=  [selsort^#(L)]

[ifselsort^#(false(), cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [9]
>  [4]
[0]
=  [min^#(cons(N, L))]

[ifselsort^#(false(), cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [9]
>  [0 5] L + [5]
[0 0]     [0]
=  [replace^#(min(cons(N, L)), N, L)]

[ifselsort^#(false(), cons(N, L))] =  [7 0] N + [0 7] L + [15]
[3 0]     [0 3]     [9]
>  [7 0] N + [0 7] L + [1]
[3 0]     [0 3]     [5]
=  [selsort^#(replace(min(cons(N, L)), N, L))]

We return to the main proof. Consider the set of all dependency
pairs

:
{ 1: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, 2: le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, 3: min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, 4: ifmin^#(true(), cons(N, cons(M, L))) ->
c_11(min^#(cons(N, L)))
, 5: ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L)))
, 6: replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, 7: ifrepl^#(false(), N, M, cons(K, L)) ->
c_16(replace^#(N, M, L))
, 8: selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, 9: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 10: selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, 11: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 12: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 13: ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L)
, 14: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,6,7,8,9,11,12,13,14}. These cover all (indirect)
predecessors of dependency pairs {1,6,7,8,9,10,11,12,13,14}, their
number of application is equally bounded. The dependency pairs are
shifted into the weak component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
{ le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L))) }
Weak DPs:
{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L)
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^2))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y))
, replace^#(N, M, cons(K, L)) ->
c_13(ifrepl^#(eq(N, K), N, M, cons(K, L)), eq^#(N, K))
, ifrepl^#(false(), N, M, cons(K, L)) -> c_16(replace^#(N, M, L))
, selsort^#(cons(N, L)) -> eq^#(N, min(cons(N, L)))
, ifselsort^#(false(), cons(N, L)) ->
replace^#(min(cons(N, L)), N, L) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
{ le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L))) }
Weak DPs:
{ selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^2))

We decompose the input problem according to the dependency graph
into the upper component

{ min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

and lower component

{ le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) }

Further, following extension rules are added to the lower
component.

{ min^#(cons(N, cons(M, L))) -> le^#(N, M)
, min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L))
, ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
{ min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L))) }
Weak DPs:
{ selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
{ 2: ifmin^#(true(), cons(N, cons(M, L))) ->
c_11(min^#(cons(N, L)))
, 3: ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L)))
, 4: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 5: selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 7: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 8: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Trs:
{ le(0(), Y) -> true()
, le(s(X), 0()) -> false() }

Sub-proof:
----------
The following argument positions are usable:
Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1}

TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).

[eq](x1, x2) = [0]

[0] = [1]

[true] = [1]

[s](x1) = [1] x1 + [0]

[false] = [0]

[le](x1, x2) = [2]

[min](x1) = [0]

[cons](x1, x2) = [1] x2 + [2]

[nil] = [0]

[ifmin](x1, x2) = [0]

[replace](x1, x2, x3) = [1] x3 + [0]

[ifrepl](x1, x2, x3, x4) = [1] x4 + [0]

[le^#](x1, x2) = [0]

[min^#](x1) = [2] x1 + [3]

[c_8](x1, x2) = [1] x1 + [1] x2 + [0]

[ifmin^#](x1, x2) = [1] x1 + [2] x2 + [1]

[c_11](x1) = [1] x1 + [0]

[c_12](x1) = [1] x1 + [0]

[selsort^#](x1) = [2] x1 + [7]

[ifselsort^#](x1, x2) = [2] x2 + [5]

The order satisfies the following ordering constraints:

[eq(0(), 0())] =  [0]
?  [1]
=  [true()]

[eq(0(), s(Y))] =  [0]
>= [0]
=  [false()]

[eq(s(X), 0())] =  [0]
>= [0]
=  [false()]

[eq(s(X), s(Y))] =  [0]
>= [0]
=  [eq(X, Y)]

[le(0(), Y)] =  [2]
>  [1]
=  [true()]

[le(s(X), 0())] =  [2]
>  [0]
=  [false()]

[le(s(X), s(Y))] =  [2]
>= [2]
=  [le(X, Y)]

[min(cons(N, cons(M, L)))] =  [0]
>= [0]
=  [ifmin(le(N, M), cons(N, cons(M, L)))]

[min(cons(0(), nil()))] =  [0]
?  [1]
=  [0()]

[min(cons(s(N), nil()))] =  [0]
?  [1] N + [0]
=  [s(N)]

[ifmin(true(), cons(N, cons(M, L)))] =  [0]
>= [0]
=  [min(cons(N, L))]

[ifmin(false(), cons(N, cons(M, L)))] =  [0]
>= [0]
=  [min(cons(M, L))]

[replace(N, M, cons(K, L))] =  [1] L + [2]
>= [1] L + [2]
=  [ifrepl(eq(N, K), N, M, cons(K, L))]

[replace(N, M, nil())] =  [0]
>= [0]
=  [nil()]

[ifrepl(true(), N, M, cons(K, L))] =  [1] L + [2]
>= [1] L + [2]
=  [cons(M, L)]

[ifrepl(false(), N, M, cons(K, L))] =  [1] L + [2]
>= [1] L + [2]
=  [cons(K, replace(N, M, L))]

[min^#(cons(N, cons(M, L)))] =  [2] L + [11]
>= [2] L + [11]
=  [c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))]

[ifmin^#(true(), cons(N, cons(M, L)))] =  [2] L + [10]
>  [2] L + [7]
=  [c_11(min^#(cons(N, L)))]

[ifmin^#(false(), cons(N, cons(M, L)))] =  [2] L + [9]
>  [2] L + [7]
=  [c_12(min^#(cons(M, L)))]

[selsort^#(cons(N, L))] =  [2] L + [11]
>  [2] L + [7]
=  [min^#(cons(N, L))]

[selsort^#(cons(N, L))] =  [2] L + [11]
>  [2] L + [9]
=  [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))]

[ifselsort^#(true(), cons(N, L))] =  [2] L + [9]
>  [2] L + [7]
=  [selsort^#(L)]

[ifselsort^#(false(), cons(N, L))] =  [2] L + [9]
>  [2] L + [7]
=  [min^#(cons(N, L))]

[ifselsort^#(false(), cons(N, L))] =  [2] L + [9]
>  [2] L + [7]
=  [selsort^#(replace(min(cons(N, L)), N, L))]

We return to the main proof. Consider the set of all dependency
pairs

:
{ 1: min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, 2: ifmin^#(true(), cons(N, cons(M, L))) ->
c_11(min^#(cons(N, L)))
, 3: ifmin^#(false(), cons(N, cons(M, L))) ->
c_12(min^#(cons(M, L)))
, 4: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 5: selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, 6: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 7: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 8: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,3,4,5,6,7,8}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4,5,6,7,8}, their number of application is
equally bounded. The dependency pairs are shifted into the weak
component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
{ min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ min^#(cons(N, cons(M, L))) ->
c_8(ifmin^#(le(N, M), cons(N, cons(M, L))), le^#(N, M))
, ifmin^#(true(), cons(N, cons(M, L))) -> c_11(min^#(cons(N, L)))
, ifmin^#(false(), cons(N, cons(M, L))) -> c_12(min^#(cons(M, L)))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
innermost runtime complexity
YES(O(1),O(1))

Empty rules are trivially bounded

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs: { le^#(s(X), s(Y)) -> c_7(le^#(X, Y)) }
Weak DPs:
{ min^#(cons(N, cons(M, L))) -> le^#(N, M)
, min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L))
, ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
{ 1: le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, 2: min^#(cons(N, cons(M, L))) -> le^#(N, M)
, 3: min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, 6: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 8: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 9: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 10: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

Sub-proof:
----------
The following argument positions are usable:
Uargs(c_7) = {1}

TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).

[eq](x1, x2) = [0]

[0] = [0]

[true] = [0]

[s](x1) = [1] x1 + [4]

[false] = [0]

[le](x1, x2) = [0]

[min](x1) = [0]

[cons](x1, x2) = [1] x1 + [1] x2 + [1]

[nil] = [0]

[ifmin](x1, x2) = [0]

[replace](x1, x2, x3) = [1] x2 + [1] x3 + [0]

[ifrepl](x1, x2, x3, x4) = [1] x3 + [1] x4 + [0]

[le^#](x1, x2) = [1] x1 + [1] x2 + [2]

[c_7](x1) = [1] x1 + [0]

[min^#](x1) = [1] x1 + [7]

[ifmin^#](x1, x2) = [1] x2 + [6]

[selsort^#](x1) = [2] x1 + [7]

[ifselsort^#](x1, x2) = [2] x2 + [7]

The order satisfies the following ordering constraints:

[eq(0(), 0())] =  [0]
>= [0]
=  [true()]

[eq(0(), s(Y))] =  [0]
>= [0]
=  [false()]

[eq(s(X), 0())] =  [0]
>= [0]
=  [false()]

[eq(s(X), s(Y))] =  [0]
>= [0]
=  [eq(X, Y)]

[le(0(), Y)] =  [0]
>= [0]
=  [true()]

[le(s(X), 0())] =  [0]
>= [0]
=  [false()]

[le(s(X), s(Y))] =  [0]
>= [0]
=  [le(X, Y)]

[min(cons(N, cons(M, L)))] =  [0]
>= [0]
=  [ifmin(le(N, M), cons(N, cons(M, L)))]

[min(cons(0(), nil()))] =  [0]
>= [0]
=  [0()]

[min(cons(s(N), nil()))] =  [0]
?  [1] N + [4]
=  [s(N)]

[ifmin(true(), cons(N, cons(M, L)))] =  [0]
>= [0]
=  [min(cons(N, L))]

[ifmin(false(), cons(N, cons(M, L)))] =  [0]
>= [0]
=  [min(cons(M, L))]

[replace(N, M, cons(K, L))] =  [1] M + [1] L + [1] K + [1]
>= [1] M + [1] L + [1] K + [1]
=  [ifrepl(eq(N, K), N, M, cons(K, L))]

[replace(N, M, nil())] =  [1] M + [0]
>= [0]
=  [nil()]

[ifrepl(true(), N, M, cons(K, L))] =  [1] M + [1] L + [1] K + [1]
>= [1] M + [1] L + [1]
=  [cons(M, L)]

[ifrepl(false(), N, M, cons(K, L))] =  [1] M + [1] L + [1] K + [1]
>= [1] M + [1] L + [1] K + [1]
=  [cons(K, replace(N, M, L))]

[le^#(s(X), s(Y))] =  [1] Y + [1] X + [10]
>  [1] Y + [1] X + [2]
=  [c_7(le^#(X, Y))]

[min^#(cons(N, cons(M, L)))] =  [1] N + [1] M + [1] L + [9]
>  [1] N + [1] M + [2]
=  [le^#(N, M)]

[min^#(cons(N, cons(M, L)))] =  [1] N + [1] M + [1] L + [9]
>  [1] N + [1] M + [1] L + [8]
=  [ifmin^#(le(N, M), cons(N, cons(M, L)))]

[ifmin^#(true(), cons(N, cons(M, L)))] =  [1] N + [1] M + [1] L + [8]
>= [1] N + [1] L + [8]
=  [min^#(cons(N, L))]

[ifmin^#(false(), cons(N, cons(M, L)))] =  [1] N + [1] M + [1] L + [8]
>= [1] M + [1] L + [8]
=  [min^#(cons(M, L))]

[selsort^#(cons(N, L))] =  [2] N + [2] L + [9]
>  [1] N + [1] L + [8]
=  [min^#(cons(N, L))]

[selsort^#(cons(N, L))] =  [2] N + [2] L + [9]
>= [2] N + [2] L + [9]
=  [ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))]

[ifselsort^#(true(), cons(N, L))] =  [2] N + [2] L + [9]
>  [2] L + [7]
=  [selsort^#(L)]

[ifselsort^#(false(), cons(N, L))] =  [2] N + [2] L + [9]
>  [1] N + [1] L + [8]
=  [min^#(cons(N, L))]

[ifselsort^#(false(), cons(N, L))] =  [2] N + [2] L + [9]
>  [2] N + [2] L + [7]
=  [selsort^#(replace(min(cons(N, L)), N, L))]

We return to the main proof. Consider the set of all dependency
pairs

:
{ 1: le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, 2: min^#(cons(N, cons(M, L))) -> le^#(N, M)
, 3: min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, 4: ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L))
, 5: ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L))
, 6: selsort^#(cons(N, L)) -> min^#(cons(N, L))
, 7: selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, 8: ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, 9: ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, 10: ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,2,3,6,8,9,10}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4,5,6,7,8,9,10}, their number of
application is equally bounded. The dependency pairs are shifted
into the weak component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
{ le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) -> le^#(N, M)
, min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L))
, ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ le^#(s(X), s(Y)) -> c_7(le^#(X, Y))
, min^#(cons(N, cons(M, L))) -> le^#(N, M)
, min^#(cons(N, cons(M, L))) ->
ifmin^#(le(N, M), cons(N, cons(M, L)))
, ifmin^#(true(), cons(N, cons(M, L))) -> min^#(cons(N, L))
, ifmin^#(false(), cons(N, cons(M, L))) -> min^#(cons(M, L))
, selsort^#(cons(N, L)) -> min^#(cons(N, L))
, selsort^#(cons(N, L)) ->
ifselsort^#(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort^#(true(), cons(N, L)) -> selsort^#(L)
, ifselsort^#(false(), cons(N, L)) -> min^#(cons(N, L))
, ifselsort^#(false(), cons(N, L)) ->
selsort^#(replace(min(cons(N, L)), N, L)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) }
Obligation:
innermost runtime complexity
YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
innermost runtime complexity