Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/add)

The rewrite relation of the following TRS is considered.

add0(x',Cons(x,xs))	→	add0(Cons(Cons(Nil,Nil),x'),xs)	(1)
notEmpty(Cons(x,xs))	→	True	(2)
notEmpty(Nil)	→	False	(3)
add0(x,Nil)	→	x	(4)
goal(x,y)	→	add0(x,y)	(5)

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
False₀	→	0
add0₀(0,0)	→	1
notEmpty₀(0)	→	2
goal₀(0,0)	→	3
Nil₁	→	6
Nil₁	→	7
Cons₁(6,7)	→	5
Cons₁(5,0)	→	4
add0₁(4,0)	→	1
True₁	→	2
False₁	→	2
add0₁(0,0)	→	3
Cons₁(5,4)	→	4
add0₁(4,0)	→	3
0	→	1
0	→	3
4	→	1
4	→	3