Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.38)

The rewrite relation of the following TRS is considered.

g(f(x,y),z)	→	f(x,g(y,z))	(1)
g(h(x,y),z)	→	g(x,f(y,z))	(2)
g(x,h(y,z))	→	h(g(x,y),z)	(3)

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 1. This is shown by the following automaton.

final states:

{0, 1}

transitions:

f₀(0,0)	→	0
h₀(0,0)	→	0
g₀(0,0)	→	1
g₁(0,0)	→	2
f₁(0,2)	→	1
f₁(0,0)	→	3
g₁(0,3)	→	1
g₁(0,0)	→	4
h₁(4,0)	→	1
g₁(0,3)	→	2
f₁(0,2)	→	2
f₁(0,2)	→	4
f₁(0,3)	→	3
g₁(0,3)	→	4
h₁(4,0)	→	2
h₁(4,0)	→	4