Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/addlists)

The rewrite relation of the following TRS is considered.

addlist(Cons(x,xs'),Cons(S(0),xs))	→	Cons(S(x),addlist(xs',xs))	(1)
addlist(Cons(S(0),xs'),Cons(x,xs))	→	Cons(S(x),addlist(xs',xs))	(2)
addlist(Nil,ys)	→	Nil	(3)
notEmpty(Cons(x,xs))	→	True	(4)
notEmpty(Nil)	→	False	(5)
goal(xs,ys)	→	addlist(xs,ys)	(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
S₀(0)	→	0
0₀	→	0
Nil₀	→	0
True₀	→	0
False₀	→	0
addlist₀(0,0)	→	1
notEmpty₀(0)	→	2
goal₀(0,0)	→	3
S₁(0)	→	4
addlist₁(0,0)	→	5
Cons₁(4,5)	→	1
Nil₁	→	1
True₁	→	2
False₁	→	2
addlist₁(0,0)	→	3
Cons₁(4,5)	→	3
Cons₁(4,5)	→	5
Nil₁	→	3
Nil₁	→	5