Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/gmnp)

The rewrite relation of the following TRS is considered.

f(a)	→	f(c(a))	(1)
f(c(X))	→	X	(2)
f(c(a))	→	f(d(b))	(3)
f(a)	→	f(d(a))	(4)
f(d(X))	→	X	(5)
f(c(b))	→	f(d(a))	(6)
e(g(X))	→	e(X)	(7)

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}

transitions:

a₀	→	0
c₀(0)	→	0
d₀(0)	→	0
b₀	→	0
g₀(0)	→	0
f₀(0)	→	1
e₀(0)	→	2
a₁	→	4
c₁(4)	→	3
f₁(3)	→	1
b₁	→	6
d₁(6)	→	5
f₁(5)	→	1
a₁	→	8
d₁(8)	→	7
f₁(7)	→	1
e₁(0)	→	2
b₂	→	10
d₂(10)	→	9
f₂(9)	→	1
0	→	1
4	→	1
6	→	1
8	→	1
10	→	1