Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/ExConc_Zan97_GM)

The rewrite relation of the following TRS is considered.

a__f(X)	→	g(h(f(X)))	(1)
mark(f(X))	→	a__f(mark(X))	(2)
mark(g(X))	→	g(X)	(3)
mark(h(X))	→	h(mark(X))	(4)
a__f(X)	→	f(X)	(5)

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:

{1, 2}

transitions:

a__f₀(2)	→	1
mark₀(2)	→	1
f₁(2)	→	1
g₁(2)	→	1
g₁(8)	→	1
a__f₁(10)	→	1
f₂(10)	→	1
h₁(11)	→	1
g₂(12)	→	1
g₀(2)	→	2
h₀(2)	→	2
f₀(2)	→	2
h₁(9)	→	8
f₁(2)	→	9
mark₁(2)	→	10
g₁(2)	→	10
a__f₁(10)	→	10
f₂(10)	→	10
h₁(11)	→	10
g₂(12)	→	10
mark₁(2)	→	11
g₁(2)	→	11
a__f₁(10)	→	11
f₂(10)	→	11
h₁(11)	→	11
g₂(12)	→	11
h₂(13)	→	12
f₂(10)	→	13