Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex6_9_Luc02c_FR)

The rewrite relation of the following TRS is considered.

2nd(cons1(X,cons(Y,Z)))	→	Y	(1)
2nd(cons(X,X1))	→	2nd(cons1(X,activate(X1)))	(2)
from(X)	→	cons(X,n__from(n__s(X)))	(3)
from(X)	→	n__from(X)	(4)
s(X)	→	n__s(X)	(5)
activate(n__from(X))	→	from(activate(X))	(6)
activate(n__s(X))	→	s(activate(X))	(7)
activate(X)	→	X	(8)

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:

2nd^#(cons1(z0,cons(z1,z2)))

→

(10)

originates from

2nd(cons1(z0,cons(z1,z2)))

→

(9)

2nd^#(cons(z0,z1))

→

c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))

(12)

originates from

2nd(cons(z0,z1))

→

2nd(cons1(z0,activate(z1)))

(11)

from^#(z0)

→

(14)

originates from

from(z0)

→

cons(z0,n__from(n__s(z0)))

(13)

from^#(z0)

→

(16)

originates from

from(z0)

→

n__from(z0)

(15)

s^#(z0)

→

(18)

originates from

s(z0)

→

n__s(z0)

(17)

activate^#(n__from(z0))

→

c5(from^#(activate(z0)),activate^#(z0))

(20)

originates from

activate(n__from(z0))

→

from(activate(z0))

(19)

activate^#(n__s(z0))

→

c6(s^#(activate(z0)),activate^#(z0))

(22)

originates from

activate(n__s(z0))

→

s(activate(z0))

(21)

activate^#(z0)

→

(24)

originates from

activate(z0)

→

(23)

Moreover, we add the following terms to the innermost strategy.

2nd^#(cons1(z0,cons(z1,z2)))

2nd^#(cons(z0,z1))

from^#(z0)

s^#(z0)

activate^#(n__from(z0))

activate^#(n__s(z0))

activate^#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

2nd(cons1(z0,cons(z1,z2)))	→	z1	(9)
2nd(cons(z0,z1))	→	2nd(cons1(z0,activate(z1)))	(11)

1.1.1 Rule Shifting

The rules

2nd^#(cons1(z0,cons(z1,z2)))

→

(10)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c7]	=	0
[activate(x₁)]	=	1 + 1 · x₁ + 1 · x₁ · x₁ + 1 · x₁ · x₁ · x₁
[from(x₁)]	=	0
[s(x₁)]	=	1 + 1 · x₁
[2nd^#(x₁)]	=	1
[from^#(x₁)]	=	0
[s^#(x₁)]	=	0
[activate^#(x₁)]	=	0
[n__from(x₁)]	=	0
[n__s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	0
[cons1(x₁, x₂)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

2nd^#(cons1(z0,cons(z1,z2)))	→	c	(10)
2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)
s^#(z0)	→	c4	(18)
activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)
activate^#(z0)	→	c7	(24)

1.1.1.1 Rule Shifting

The rules

2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c7]	=	0
[activate(x₁)]	=	0
[from(x₁)]	=	3
[s(x₁)]	=	3
[2nd^#(x₁)]	=	1 · x₁ + 0
[from^#(x₁)]	=	0
[s^#(x₁)]	=	0
[activate^#(x₁)]	=	1 · x₁ + 0
[n__from(x₁)]	=	1 · x₁ + 0
[n__s(x₁)]	=	2 + 1 · x₁
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[cons1(x₁, x₂)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

2nd^#(cons1(z0,cons(z1,z2)))	→	c	(10)
2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)
s^#(z0)	→	c4	(18)
activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)
activate^#(z0)	→	c7	(24)

1.1.1.1.1 Rule Shifting

The rules

from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c7]	=	0
[activate(x₁)]	=	1 + 1 · x₁
[from(x₁)]	=	1 + 1 · x₁
[s(x₁)]	=	1 · x₁ + 0
[2nd^#(x₁)]	=	1 · x₁ + 0
[from^#(x₁)]	=	1
[s^#(x₁)]	=	0
[activate^#(x₁)]	=	1 · x₁ + 0
[n__from(x₁)]	=	1 + 1 · x₁
[n__s(x₁)]	=	1 · x₁ + 0
[cons(x₁, x₂)]	=	1 · x₂ + 0
[cons1(x₁, x₂)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

2nd^#(cons1(z0,cons(z1,z2)))	→	c	(10)
2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)
s^#(z0)	→	c4	(18)
activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)
activate^#(z0)	→	c7	(24)

1.1.1.1.1.1 Rule Shifting

The rules

activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(z0)	→	c7	(24)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c7]	=	0
[activate(x₁)]	=	0
[from(x₁)]	=	3
[s(x₁)]	=	3
[2nd^#(x₁)]	=	2 · x₁ + 0
[from^#(x₁)]	=	0
[s^#(x₁)]	=	0
[activate^#(x₁)]	=	2 + 2 · x₁
[n__from(x₁)]	=	2 + 1 · x₁
[n__s(x₁)]	=	1 · x₁ + 0
[cons(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[cons1(x₁, x₂)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

2nd^#(cons1(z0,cons(z1,z2)))	→	c	(10)
2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)
s^#(z0)	→	c4	(18)
activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)
activate^#(z0)	→	c7	(24)

1.1.1.1.1.1.1 Rule Shifting

The rules

s^#(z0)

→

(18)

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

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c7]	=	0
[activate(x₁)]	=	1 + 1 · x₁
[from(x₁)]	=	1 + 1 · x₁
[s(x₁)]	=	1 + 1 · x₁
[2nd^#(x₁)]	=	1 · x₁ + 0
[from^#(x₁)]	=	1
[s^#(x₁)]	=	1
[activate^#(x₁)]	=	1 + 1 · x₁
[n__from(x₁)]	=	1 + 1 · x₁
[n__s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[cons1(x₁, x₂)]	=	1 · x₁ + 0

which has the intended complexity. Here, only the following usable rules have been considered:

2nd^#(cons1(z0,cons(z1,z2)))	→	c	(10)
2nd^#(cons(z0,z1))	→	c1(2nd^#(cons1(z0,activate(z1))),activate^#(z1))	(12)
from^#(z0)	→	c2	(14)
from^#(z0)	→	c3	(16)
s^#(z0)	→	c4	(18)
activate^#(n__from(z0))	→	c5(from^#(activate(z0)),activate^#(z0))	(20)
activate^#(n__s(z0))	→	c6(s^#(activate(z0)),activate^#(z0))	(22)
activate^#(z0)	→	c7	(24)

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