Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/list)

The rewrite relation of the following TRS is considered.

list(Cons(x,xs))	→	list(xs)	(1)
list(Nil)	→	True	(2)
list(Nil)	→	isEmpty[Match](Nil)	(3)
notEmpty(Cons(x,xs))	→	True	(4)
notEmpty(Nil)	→	False	(5)
goal(x)	→	list(x)	(6)

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, 2, 3}

transitions:

Cons₀(0,0)	→	0
Nil₀	→	0
True₀	→	0
isEmpty[Match]₀(0)	→	0
False₀	→	0
list₀(0)	→	1
notEmpty₀(0)	→	2
goal₀(0)	→	3
list₁(0)	→	1
True₁	→	1
Nil₁	→	4
isEmpty[Match]₁(4)	→	1
True₁	→	2
False₁	→	2
list₁(0)	→	3
True₁	→	3
isEmpty[Match]₁(4)	→	3