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(n²).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

eq^#(0,0)

→

(11)

originates from

eq(0,0)

→

true

(1)

eq^#(0,s(z0))

→

(13)

originates from

eq(0,s(z0))

→

false

(12)

eq^#(s(z0),0)

→

(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)

→

(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)

→

(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)

→

(26)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[rm(x₁, x₂)]	=	1 + 1 · x₁
[ifrm(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[eq^#(x₁, x₂)]	=	0
[rm^#(x₁, x₂)]	=	0
[ifrm^#(x₁, x₂, x₃)]	=	0
[purge^#(x₁)]	=	1
[nil]	=	1
[add(x₁, x₂)]	=	1 · x₁ + 0
[true]	=	1
[false]	=	1
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁

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(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[rm(x₁, x₂)]	=	1 · x₂ + 0
[ifrm(x₁, x₂, x₃)]	=	1 · x₃ + 0
[eq^#(x₁, x₂)]	=	0
[rm^#(x₁, x₂)]	=	1 · x₁ + 0
[ifrm^#(x₁, x₂, x₃)]	=	1 · x₂ + 0
[purge^#(x₁)]	=	1 · x₁ + 0
[nil]	=	1
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[true]	=	1
[false]	=	0
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁

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)

→

(19)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[rm(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[ifrm(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[eq^#(x₁, x₂)]	=	0
[rm^#(x₁, x₂)]	=	1
[ifrm^#(x₁, x₂, x₃)]	=	1
[purge^#(x₁)]	=	1 · x₁ + 0
[nil]	=	1
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[true]	=	1
[false]	=	0
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁

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(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	1 · x₂ + 0
[ifrm(x₁, x₂, x₃)]	=	1 · x₃ + 0
[eq^#(x₁, x₂)]	=	1 · x₁ + 0
[rm^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₁ · x₂
[ifrm^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₂ · x₃
[purge^#(x₁)]	=	1 · x₁ · x₁ + 0
[nil]	=	0
[add(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	2 + 1 · x₁

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(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	1 · x₂ + 0
[ifrm(x₁, x₂, x₃)]	=	1 · x₃ + 0
[eq^#(x₁, x₂)]	=	0
[rm^#(x₁, x₂)]	=	1 · x₂ + 0
[ifrm^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[purge^#(x₁)]	=	1 · x₁ · x₁ + 0
[nil]	=	0
[add(x₁, x₂)]	=	1 + 1 · x₂
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	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(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	1 · x₂ + 0
[ifrm(x₁, x₂, x₃)]	=	1 · x₃ + 0
[eq^#(x₁, x₂)]	=	2
[rm^#(x₁, x₂)]	=	2 + 1 · x₂
[ifrm^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[purge^#(x₁)]	=	2 · x₁ · x₁ + 0
[nil]	=	0
[add(x₁, x₂)]	=	2 + 1 · x₂
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	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(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁)]	=	1 · x₁ + 0
[c7(x₁)]	=	1 · x₁ + 0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[eq(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	1 · x₂ + 0
[ifrm(x₁, x₂, x₃)]	=	1 · x₃ + 0
[eq^#(x₁, x₂)]	=	0
[rm^#(x₁, x₂)]	=	2 + 2 · x₂
[ifrm^#(x₁, x₂, x₃)]	=	2 · x₃ + 0
[purge^#(x₁)]	=	1 · x₁ · x₁ + 0
[nil]	=	0
[add(x₁, x₂)]	=	2 + 1 · x₂
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	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).