Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/ex6)

The rewrite relation of the following TRS is considered.

g(S(x),y)	→	g(x,S(y))	(1)
f(y,S(x))	→	f(S(y),x)	(2)
g(0,x2)	→	x2	(3)
f(x1,0)	→	g(x1,0)	(4)

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:

S₀(0)	→	0
0₀	→	0
g₀(0,0)	→	1
f₀(0,0)	→	2
S₁(0)	→	3
g₁(0,3)	→	1
S₁(0)	→	4
f₁(4,0)	→	2
0₁	→	5
g₁(0,5)	→	2
S₁(3)	→	3
S₁(5)	→	3
g₁(0,3)	→	2
S₁(4)	→	4
g₁(4,5)	→	2
S₂(5)	→	6
g₂(0,6)	→	2
g₂(4,6)	→	2
S₁(6)	→	3
S₂(6)	→	6
0	→	1
3	→	1
3	→	2
5	→	2
6	→	2