Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/rev-fletf)

The rewrite relation of the following TRS is considered.

rev_l#2(x8,x10)	→	Cons(x10,x8)	(1)
step_x_f#1(rev_l,x5,step_x_f(x2,x3,x4),x1)	→	step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))	(2)
step_x_f#1(rev_l,x5,fleft_op_e_xs_1,x3)	→	rev_l#2(x3,x5)	(3)
foldr#3(Nil)	→	fleft_op_e_xs_1	(4)
foldr#3(Cons(x16,x6))	→	step_x_f(rev_l,x16,foldr#3(x6))	(5)
main(Nil)	→	Nil	(6)
main(Cons(x8,x9))	→	step_x_f#1(rev_l,x8,foldr#3(x9),Nil)	(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 3. This is shown by the following automaton.

final states:

{0, 1, 2, 3, 4}

transitions:

Cons₀(0,0)	→	0
rev_l₀	→	0
step_x_f₀(0,0,0)	→	0
fleft_op_e_xs_1₀	→	0
Nil₀	→	0
rev_l#2₀(0,0)	→	1
step_x_f#1₀(0,0,0,0)	→	2
foldr#3₀(0)	→	3
main₀(0)	→	4
Cons₁(0,0)	→	1
rev_l#2₁(0,0)	→	5
step_x_f#1₁(0,0,0,5)	→	2
rev_l#2₁(0,0)	→	2
fleft_op_e_xs_1₁	→	3
rev_l₁	→	6
foldr#3₁(0)	→	7
step_x_f₁(6,0,7)	→	3
Nil₁	→	4
rev_l₁	→	8
foldr#3₁(0)	→	9
Nil₁	→	10
step_x_f#1₁(8,0,9,10)	→	4
Cons₂(0,0)	→	2
Cons₂(0,0)	→	5
rev_l#2₁(5,0)	→	5
rev_l#2₁(5,0)	→	2
fleft_op_e_xs_1₁	→	7
fleft_op_e_xs_1₁	→	9
step_x_f₁(6,0,7)	→	7
step_x_f₁(6,0,7)	→	9
Cons₂(0,5)	→	2
Cons₂(0,5)	→	5
rev_l#2₂(10,0)	→	11
step_x_f#1₂(6,0,7,11)	→	4
rev_l#2₂(10,0)	→	4
Cons₃(0,10)	→	4
Cons₃(0,10)	→	11
rev_l#2₂(11,0)	→	11
rev_l#2₂(11,0)	→	4
Cons₃(0,11)	→	4
Cons₃(0,11)	→	11