Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/rev-dl)

The rewrite relation of the following TRS is considered.

walk#1(Nil)	→	walk_xs	(1)
walk#1(Cons(x4,x3))	→	comp_f_g(walk#1(x3),walk_xs_3(x4))	(2)
comp_f_g#1(comp_f_g(x7,x9),walk_xs_3(x8),x12)	→	comp_f_g#1(x7,x9,Cons(x8,x12))	(3)
comp_f_g#1(walk_xs,walk_xs_3(x8),x12)	→	Cons(x8,x12)	(4)
main(Nil)	→	Nil	(5)
main(Cons(x4,x5))	→	comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil)	(6)

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 2. This is shown by the following automaton.

final states:

{0, 1, 2, 3}

transitions:

Nil₀	→	0
walk_xs₀	→	0
Cons₀(0,0)	→	0
comp_f_g₀(0,0)	→	0
walk_xs_3₀(0)	→	0
walk#1₀(0)	→	1
comp_f_g#1₀(0,0,0)	→	2
main₀(0)	→	3
walk_xs₁	→	1
walk#1₁(0)	→	4
walk_xs_3₁(0)	→	5
comp_f_g₁(4,5)	→	1
Cons₁(0,0)	→	6
comp_f_g#1₁(0,0,6)	→	2
Cons₁(0,0)	→	2
Nil₁	→	3
walk#1₁(0)	→	7
walk_xs_3₁(0)	→	8
Nil₁	→	9
comp_f_g#1₁(7,8,9)	→	3
walk_xs₁	→	4
walk_xs₁	→	7
comp_f_g₁(4,5)	→	4
comp_f_g₁(4,5)	→	7
Cons₁(0,6)	→	6
Cons₁(0,6)	→	2
Cons₂(0,9)	→	10
comp_f_g#1₂(4,5,10)	→	3
Cons₂(0,9)	→	3
Cons₂(0,10)	→	10
Cons₂(0,10)	→	3