Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex26_Luc03b_L)

The rewrite relation of the following TRS is considered.

terms(N)	→	cons(recip(sqr(N)))	(1)
sqr(0)	→	0	(2)
sqr(s)	→	s	(3)
dbl(0)	→	0	(4)
dbl(s)	→	s	(5)
add(0,X)	→	X	(6)
add(s,Y)	→	s	(7)
first(0,X)	→	nil	(8)
first(s,cons(Y))	→	cons(Y)	(9)

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

transitions:

cons₀(0)	→	0
recip₀(0)	→	0
0₀	→	0
s₀	→	0
nil₀	→	0
terms₀(0)	→	1
sqr₀(0)	→	2
dbl₀(0)	→	3
add₀(0,0)	→	4
first₀(0,0)	→	5
sqr₁(0)	→	7
recip₁(7)	→	6
cons₁(6)	→	1
0₁	→	2
s₁	→	2
0₁	→	3
s₁	→	3
s₁	→	4
nil₁	→	5
cons₁(0)	→	5
0₁	→	7
s₁	→	7
0	→	4