Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/elimdupl)

The rewrite relation of the following TRS is considered.

eq(0,0) true (1)
eq(0,s(X)) false (2)
eq(s(X),0) false (3)
eq(s(X),s(Y)) eq(X,Y) (4)
rm(N,nil) nil (5)
rm(N,add(M,X)) ifrm(eq(N,M),N,add(M,X)) (6)
ifrm(true,N,add(M,X)) rm(N,X) (7)
ifrm(false,N,add(M,X)) add(M,rm(N,X)) (8)
purge(nil) nil (9)
purge(add(N,X)) add(N,purge(rm(N,X))) (10)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
eq#(0,0) c (11)
originates from
eq(0,0) true (1)
eq#(0,s(z0)) c1 (13)
originates from
eq(0,s(z0)) false (12)
eq#(s(z0),0) c2 (15)
originates from
eq(s(z0),0) false (14)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
originates from
eq(s(z0),s(z1)) eq(z0,z1) (16)
rm#(z0,nil) c4 (19)
originates from
rm(z0,nil) nil (18)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
originates from
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
originates from
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
originates from
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
purge#(nil) c8 (26)
originates from
purge(nil) nil (9)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
originates from
purge(add(z0,z1)) add(z0,purge(rm(z0,z1))) (27)
Moreover, we add the following terms to the innermost strategy.
eq#(0,0)
eq#(0,s(z0))
eq#(s(z0),0)
eq#(s(z0),s(z1))
rm#(z0,nil)
rm#(z0,add(z1,z2))
ifrm#(true,z0,add(z1,z2))
ifrm#(false,z0,add(z1,z2))
purge#(nil)
purge#(add(z0,z1))

1.1 Usable Rules

We remove the following rules since they are not usable.
purge(nil) nil (9)
purge(add(z0,z1)) add(z0,purge(rm(z0,z1))) (27)

1.1.1 Rule Shifting

The rules
purge#(nil) c8 (26)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[rm(x1, x2)] = 1 + 1 · x1
[ifrm(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[eq#(x1, x2)] = 0
[rm#(x1, x2)] = 0
[ifrm#(x1, x2, x3)] = 0
[purge#(x1)] = 1
[nil] = 1
[add(x1, x2)] = 1 · x1 + 0
[true] = 1
[false] = 1
[0] = 1
[s(x1)] = 1 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)

1.1.1.1 Rule Shifting

The rules
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[rm(x1, x2)] = 1 · x2 + 0
[ifrm(x1, x2, x3)] = 1 · x3 + 0
[eq#(x1, x2)] = 0
[rm#(x1, x2)] = 1 · x1 + 0
[ifrm#(x1, x2, x3)] = 1 · x2 + 0
[purge#(x1)] = 1 · x1 + 0
[nil] = 1
[add(x1, x2)] = 1 + 1 · x1 + 1 · x2
[true] = 1
[false] = 0
[0] = 1
[s(x1)] = 1 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1 Rule Shifting

The rules
rm#(z0,nil) c4 (19)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 1 + 1 · x1 + 1 · x2
[rm(x1, x2)] = 1 · x1 + 0 + 1 · x2
[ifrm(x1, x2, x3)] = 1 · x2 + 0 + 1 · x3
[eq#(x1, x2)] = 0
[rm#(x1, x2)] = 1
[ifrm#(x1, x2, x3)] = 1
[purge#(x1)] = 1 · x1 + 0
[nil] = 1
[add(x1, x2)] = 1 + 1 · x1 + 1 · x2
[true] = 1
[false] = 0
[0] = 1
[s(x1)] = 1 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1.1 Rule Shifting

The rules
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[rm(x1, x2)] = 1 · x2 + 0
[ifrm(x1, x2, x3)] = 1 · x3 + 0
[eq#(x1, x2)] = 1 · x1 + 0
[rm#(x1, x2)] = 2 · x1 + 0 + 1 · x1 · x2
[ifrm#(x1, x2, x3)] = 1 · x2 + 0 + 1 · x2 · x3
[purge#(x1)] = 1 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 2 + 1 · x1 + 1 · x2
[true] = 0
[false] = 0
[0] = 0
[s(x1)] = 2 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1.1.1 Rule Shifting

The rules
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[rm(x1, x2)] = 1 · x2 + 0
[ifrm(x1, x2, x3)] = 1 · x3 + 0
[eq#(x1, x2)] = 0
[rm#(x1, x2)] = 1 · x2 + 0
[ifrm#(x1, x2, x3)] = 1 · x3 + 0
[purge#(x1)] = 1 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 1 + 1 · x2
[true] = 0
[false] = 0
[0] = 0
[s(x1)] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[rm(x1, x2)] = 1 · x2 + 0
[ifrm(x1, x2, x3)] = 1 · x3 + 0
[eq#(x1, x2)] = 2
[rm#(x1, x2)] = 2 + 1 · x2
[ifrm#(x1, x2, x3)] = 1 · x3 + 0
[purge#(x1)] = 2 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 2 + 1 · x2
[true] = 0
[false] = 0
[0] = 0
[s(x1)] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1)] = 1 · x1 + 0
[c7(x1)] = 1 · x1 + 0
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[eq(x1, x2)] = 0
[rm(x1, x2)] = 1 · x2 + 0
[ifrm(x1, x2, x3)] = 1 · x3 + 0
[eq#(x1, x2)] = 0
[rm#(x1, x2)] = 2 + 2 · x2
[ifrm#(x1, x2, x3)] = 2 · x3 + 0
[purge#(x1)] = 1 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 2 + 1 · x2
[true] = 0
[false] = 0
[0] = 0
[s(x1)] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
eq#(0,0) c (11)
eq#(0,s(z0)) c1 (13)
eq#(s(z0),0) c2 (15)
eq#(s(z0),s(z1)) c3(eq#(z0,z1)) (17)
rm#(z0,nil) c4 (19)
rm#(z0,add(z1,z2)) c5(ifrm#(eq(z0,z1),z0,add(z1,z2)),eq#(z0,z1)) (21)
ifrm#(true,z0,add(z1,z2)) c6(rm#(z0,z2)) (23)
ifrm#(false,z0,add(z1,z2)) c7(rm#(z0,z2)) (25)
purge#(nil) c8 (26)
purge#(add(z0,z1)) c9(purge#(rm(z0,z1)),rm#(z0,z1)) (28)
rm(z0,add(z1,z2)) ifrm(eq(z0,z1),z0,add(z1,z2)) (20)
ifrm(false,z0,add(z1,z2)) add(z1,rm(z0,z2)) (24)
rm(z0,nil) nil (18)
ifrm(true,z0,add(z1,z2)) rm(z0,z2) (22)

1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).