Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Various_04/24)

The rewrite relation of the following TRS is considered.

max(L(x))	→	x	(1)
max(N(L(0),L(y)))	→	y	(2)
max(N(L(s(x)),L(s(y))))	→	s(max(N(L(x),L(y))))	(3)
max(N(L(x),N(y,z)))	→	max(N(L(x),L(max(N(y,z)))))	(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 1. This is shown by the following automaton.

final states:

{0, 1}

transitions:

L₀(0)	→	0
N₀(0,0)	→	0
0₀	→	0
s₀(0)	→	0
max₀(0)	→	1
L₁(0)	→	4
L₁(0)	→	5
N₁(4,5)	→	3
max₁(3)	→	2
s₁(2)	→	1
N₁(0,0)	→	8
max₁(8)	→	7
L₁(7)	→	6
N₁(4,6)	→	3
max₁(3)	→	1
s₁(2)	→	7
max₁(3)	→	7
L₁(2)	→	5
0	→	1
0	→	7
0	→	2
7	→	1
7	→	2
2	→	1
2	→	7