Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex2_Luc03b_L)

The rewrite relation of the following TRS is considered.

fst(0,Z)	→	nil	(1)
fst(s,cons(Y))	→	cons(Y)	(2)
from(X)	→	cons(X)	(3)
add(0,X)	→	X	(4)
add(s,Y)	→	s	(5)
len(nil)	→	0	(6)
len(cons(X))	→	s	(7)

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, 4}

transitions:

0₀	→	0
nil₀	→	0
s₀	→	0
cons₀(0)	→	0
fst₀(0,0)	→	1
from₀(0)	→	2
add₀(0,0)	→	3
len₀(0)	→	4
nil₁	→	1
cons₁(0)	→	1
cons₁(0)	→	2
s₁	→	3
0₁	→	4
s₁	→	4
0	→	3