MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. 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 Answer: MAYBE We add 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 MAYBE. 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 Answer: MAYBE 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 MAYBE. 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 Answer: MAYBE 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 MAYBE. 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 Answer: MAYBE 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 MAYBE. 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 Answer: MAYBE The input cannot be shown compatible Arrrr..