Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/ExConc_Zan97_FR)

The rewrite relation of the following TRS is considered.

f(X)	→	g(n__h(n__f(X)))	(1)
h(X)	→	n__h(X)	(2)
f(X)	→	n__f(X)	(3)
activate(n__h(X))	→	h(activate(X))	(4)
activate(n__f(X))	→	f(activate(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:

g₀(0)	→	0
n__h₀(0)	→	0
n__f₀(0)	→	0
f₀(0)	→	1
h₀(0)	→	2
activate₀(0)	→	3
n__f₁(0)	→	5
n__h₁(5)	→	4
g₁(4)	→	1
n__h₁(0)	→	2
n__f₁(0)	→	1
activate₁(0)	→	6
h₁(6)	→	3
activate₁(0)	→	7
f₁(7)	→	3
n__f₂(7)	→	9
n__h₂(9)	→	8
g₂(8)	→	3
n__h₂(6)	→	3
n__f₂(7)	→	3
h₁(6)	→	6
h₁(6)	→	7
f₁(7)	→	6
f₁(7)	→	7
g₂(8)	→	6
g₂(8)	→	7
n__h₂(6)	→	6
n__h₂(6)	→	7
n__f₂(7)	→	6
n__f₂(7)	→	7
0	→	3
0	→	6
0	→	7