Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex15_Luc06_Z)

The rewrite relation of the following TRS is considered.

f(n__f(n__a))	→	f(n__g(f(n__a)))	(1)
f(X)	→	n__f(X)	(2)
a	→	n__a	(3)
g(X)	→	n__g(X)	(4)
activate(n__f(X))	→	f(X)	(5)
activate(n__a)	→	a	(6)
activate(n__g(X))	→	g(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 Bounds

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

final states:

{0, 1, 2, 3, 4}

transitions:

n__f₀(0)	→	0
n__a₀	→	0
n__g₀(0)	→	0
f₀(0)	→	1
a₀	→	2
g₀(0)	→	3
activate₀(0)	→	4
n__a₁	→	7
f₁(7)	→	6
n__g₁(6)	→	5
f₁(5)	→	1
n__f₁(0)	→	1
n__a₁	→	2
n__g₁(0)	→	3
f₁(0)	→	4
a₁	→	4
g₁(0)	→	4
f₁(5)	→	4
n__f₂(5)	→	1
n__f₂(0)	→	4
n__f₂(7)	→	6
n__a₂	→	4
n__g₂(0)	→	4
n__f₂(5)	→	4
0	→	4