Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.29)

The rewrite relation of the following TRS is considered.

merge(x,nil)	→	x	(1)
merge(nil,y)	→	y	(2)
merge(++(x,y),++(u,v))	→	++(x,merge(y,++(u,v)))	(3)
merge(++(x,y),++(u,v))	→	++(u,merge(++(x,y),v))	(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:

nil₀	→	0
++₀(0,0)	→	0
u₀	→	0
v₀	→	0
merge₀(0,0)	→	1
u₁	→	4
v₁	→	5
++₁(4,5)	→	3
merge₁(0,3)	→	2
++₁(0,2)	→	1
++₁(0,0)	→	7
v₁	→	8
merge₁(7,8)	→	6
++₁(4,6)	→	1
++₁(0,2)	→	2
++₁(4,6)	→	2
0	→	1
3	→	2