Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/ExProp7_Luc06_Z)

The rewrite relation of the following TRS is considered.

f(0)	→	cons(0,n__f(s(0)))	(1)
f(s(0))	→	f(p(s(0)))	(2)
p(s(X))	→	X	(3)
f(X)	→	n__f(X)	(4)
activate(n__f(X))	→	f(X)	(5)
activate(X)	→	X	(6)

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 Bounds

The given TRS is match-(raise)-bounded by 2. This is shown by the following automaton.

final states:

{0, 1, 2, 3}

transitions:

0₀	→	0
cons₀(0,0)	→	0
n__f₀(0)	→	0
s₀(0)	→	0
f₀(0)	→	1
p₀(0)	→	2
activate₀(0)	→	3
0₁	→	4
0₁	→	7
s₁(7)	→	6
n__f₁(6)	→	5
cons₁(4,5)	→	1
s₁(7)	→	9
p₁(9)	→	8
f₁(8)	→	1
n__f₁(0)	→	1
f₁(0)	→	3
cons₁(4,5)	→	3
f₁(8)	→	3
n__f₂(8)	→	1
n__f₂(0)	→	3
0₂	→	10
0₂	→	13
s₂(13)	→	12
n__f₂(12)	→	11
cons₂(10,11)	→	1
cons₂(10,11)	→	3
n__f₂(8)	→	3
0	→	2
0	→	3
7	→	8