Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/rev-foldl)

The rewrite relation of the following TRS is considered.

foldl#3(x2,Nil)	→	x2	(1)
foldl#3(x16,Cons(x24,x6))	→	foldl#3(Cons(x24,x16),x6)	(2)
main(x1)	→	foldl#3(Nil,x1)	(3)

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}

transitions:

Nil₀	→	0
Cons₀(0,0)	→	0
foldl#3₀(0,0)	→	1
main₀(0)	→	2
Cons₁(0,0)	→	3
foldl#3₁(3,0)	→	1
Nil₁	→	4
foldl#3₁(4,0)	→	2
Cons₁(0,3)	→	3
Cons₁(0,4)	→	3
foldl#3₁(3,0)	→	2
0	→	1
3	→	1
3	→	2
4	→	2