YES(?,O(n^3)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^3)). Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) , purge(nil()) -> nil() , purge(add(N, X)) -> add(N, purge(rm(N, X))) } Obligation: innermost runtime complexity Answer: YES(?,O(n^3)) We add following dependency tuples: Strict DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(X)) -> c_2() , eq^#(s(X), 0()) -> c_3() , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , rm^#(N, nil()) -> c_5() , rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , purge^#(nil()) -> c_9() , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^3)). Strict DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(X)) -> c_2() , eq^#(s(X), 0()) -> c_3() , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , rm^#(N, nil()) -> c_5() , rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , purge^#(nil()) -> c_9() , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } Weak Trs: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) , purge(nil()) -> nil() , purge(add(N, X)) -> add(N, purge(rm(N, X))) } Obligation: innermost runtime complexity Answer: YES(?,O(n^3)) We estimate the number of application of {1,2,3,5,9} by applications of Pre({1,2,3,5,9}) = {4,6,7,8,10}. Here rules are labeled as follows: DPs: { 1: eq^#(0(), 0()) -> c_1() , 2: eq^#(0(), s(X)) -> c_2() , 3: eq^#(s(X), 0()) -> c_3() , 4: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , 5: rm^#(N, nil()) -> c_5() , 6: rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , 7: ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , 8: ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , 9: purge^#(nil()) -> c_9() , 10: purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^3)). Strict DPs: { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } Weak DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(X)) -> c_2() , eq^#(s(X), 0()) -> c_3() , rm^#(N, nil()) -> c_5() , purge^#(nil()) -> c_9() } Weak Trs: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) , purge(nil()) -> nil() , purge(add(N, X)) -> add(N, purge(rm(N, X))) } Obligation: innermost runtime complexity Answer: YES(?,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(X)) -> c_2() , eq^#(s(X), 0()) -> c_3() , rm^#(N, nil()) -> c_5() , purge^#(nil()) -> c_9() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^3)). Strict DPs: { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } Weak Trs: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) , purge(nil()) -> nil() , purge(add(N, X)) -> add(N, purge(rm(N, X))) } Obligation: innermost runtime complexity Answer: YES(?,O(n^3)) We replace rewrite rules by usable rules: Weak Usable Rules: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^3)). Strict DPs: { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) , rm^#(N, add(M, X)) -> c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } Weak Trs: { eq(0(), 0()) -> true() , eq(0(), s(X)) -> false() , eq(s(X), 0()) -> false() , eq(s(X), s(Y)) -> eq(X, Y) , rm(N, nil()) -> nil() , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) , ifrm(true(), N, add(M, X)) -> rm(N, X) , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } Obligation: innermost runtime complexity Answer: YES(?,O(n^3)) The following argument positions are usable: Uargs(c_4) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_10) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [0] [eq](x1, x2) = [0] [0] [0] [0] = [0] [0] [0] [true] = [0] [0] [1 0 1] [0] [s](x1) = [0 1 0] x1 + [1] [0 0 0] [0] [0] [false] = [0] [0] [1 0 0] [0] [rm](x1, x2) = [0 1 0] x2 + [0] [0 0 1] [0] [0] [nil] = [0] [0] [0 0 0] [1 0 1] [0] [add](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [1] [0 1 0] [0 1 1] [1] [1 0 0] [0] [ifrm](x1, x2, x3) = [0 1 0] x3 + [0] [0 0 1] [0] [0 1 0] [0] [eq^#](x1, x2) = [0 0 0] x2 + [0] [0 0 0] [0] [1 0 0] [0] [c_4](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [0 1 1] [0] [rm^#](x1, x2) = [0 0 0] x2 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_6](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [0 0 1] [0] [ifrm^#](x1, x2, x3) = [0 0 0] x3 + [0] [0 0 0] [0] [1 0 0] [0] [c_7](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_8](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 1] [0] [purge^#](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_10](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] This order satisfies following ordering constraints: [rm(N, nil())] = [0] [0] [0] >= [0] [0] [0] = [nil()] [rm(N, add(M, X))] = [1 0 1] [0 0 0] [0] [0 1 0] X + [0 1 0] M + [1] [0 1 1] [0 1 0] [1] >= [1 0 1] [0 0 0] [0] [0 1 0] X + [0 1 0] M + [1] [0 1 1] [0 1 0] [1] = [ifrm(eq(N, M), N, add(M, X))] [ifrm(true(), N, add(M, X))] = [1 0 1] [0 0 0] [0] [0 1 0] X + [0 1 0] M + [1] [0 1 1] [0 1 0] [1] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = [rm(N, X)] [ifrm(false(), N, add(M, X))] = [1 0 1] [0 0 0] [0] [0 1 0] X + [0 1 0] M + [1] [0 1 1] [0 1 0] [1] >= [1 0 1] [0 0 0] [0] [0 1 0] X + [0 1 0] M + [1] [0 1 1] [0 1 0] [1] = [add(M, rm(N, X))] [eq^#(s(X), s(Y))] = [0 1 0] [1] [0 0 0] Y + [0] [0 0 0] [0] > [0 1 0] [0] [0 0 0] Y + [0] [0 0 0] [0] = [c_4(eq^#(X, Y))] [rm^#(N, add(M, X))] = [0 2 1] [0 2 0] [2] [0 0 0] X + [0 0 0] M + [0] [0 0 0] [0 0 0] [0] > [0 1 1] [0 2 0] [1] [0 0 0] X + [0 0 0] M + [0] [0 0 0] [0 0 0] [0] = [c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M))] [ifrm^#(true(), N, add(M, X))] = [0 1 1] [0 1 0] [1] [0 0 0] X + [0 0 0] M + [0] [0 0 0] [0 0 0] [0] > [0 1 1] [0] [0 0 0] X + [0] [0 0 0] [0] = [c_7(rm^#(N, X))] [ifrm^#(false(), N, add(M, X))] = [0 1 1] [0 1 0] [1] [0 0 0] X + [0 0 0] M + [0] [0 0 0] [0 0 0] [0] > [0 1 1] [0] [0 0 0] X + [0] [0 0 0] [0] = [c_8(rm^#(N, X))] [purge^#(add(N, X))] = [1 1 2] [0 1 0] [1] [0 0 0] X + [0 0 0] N + [0] [0 0 0] [0 0 0] [0] > [1 1 2] [0] [0 0 0] X + [0] [0 0 0] [0] = [c_10(purge^#(rm(N, X)), rm^#(N, X))] Hurray, we answered YES(?,O(n^3))