Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/flatten)

The rewrite relation of the following TRS is considered.

walk#1(Leaf(x2))	→	cons_x(x2)	(1)
walk#1(Node(x5,x3))	→	comp_f_g(walk#1(x5),walk#1(x3))	(2)
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1)	→	comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))	(3)
comp_f_g#1(comp_f_g(x7,x9),cons_x(x2),x4)	→	comp_f_g#1(x7,x9,Cons(x2,x4))	(4)
comp_f_g#1(cons_x(x2),comp_f_g(x5,x7),x3)	→	Cons(x2,comp_f_g#1(x5,x7,x3))	(5)
comp_f_g#1(cons_x(x5),cons_x(x2),x4)	→	Cons(x5,Cons(x2,x4))	(6)
main(Leaf(x4))	→	Cons(x4,Nil)	(7)
main(Node(x9,x5))	→	comp_f_g#1(walk#1(x9),walk#1(x5),Nil)	(8)

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:

Leaf₀(0)	→	0
cons_x₀(0)	→	0
Node₀(0,0)	→	0
comp_f_g₀(0,0)	→	0
Cons₀(0,0)	→	0
Nil₀	→	0
walk#1₀(0)	→	1
comp_f_g#1₀(0,0,0)	→	2
main₀(0)	→	3
cons_x₁(0)	→	1
walk#1₁(0)	→	4
walk#1₁(0)	→	5
comp_f_g₁(4,5)	→	1
comp_f_g#1₁(0,0,0)	→	6
comp_f_g#1₁(0,0,6)	→	2
Cons₁(0,0)	→	7
comp_f_g#1₁(0,0,7)	→	2
comp_f_g#1₁(0,0,0)	→	8
Cons₁(0,8)	→	2
Cons₁(0,0)	→	9
Cons₁(0,9)	→	2
Nil₁	→	10
Cons₁(0,10)	→	3
walk#1₁(0)	→	11
walk#1₁(0)	→	12
Nil₁	→	13
comp_f_g#1₁(11,12,13)	→	3
cons_x₁(0)	→	4
cons_x₁(0)	→	5
cons_x₁(0)	→	11
cons_x₁(0)	→	12
comp_f_g₁(4,5)	→	4
comp_f_g₁(4,5)	→	5
comp_f_g₁(4,5)	→	11
comp_f_g₁(4,5)	→	12
comp_f_g#1₁(0,0,6)	→	6
comp_f_g#1₁(0,0,7)	→	6
comp_f_g#1₁(0,0,6)	→	8
Cons₁(0,6)	→	7
Cons₁(0,7)	→	7
comp_f_g#1₁(0,0,7)	→	8
Cons₁(0,8)	→	6
Cons₁(0,8)	→	8
Cons₁(0,6)	→	9
Cons₁(0,7)	→	9
Cons₁(0,9)	→	6
Cons₁(0,9)	→	8
comp_f_g#1₂(4,5,13)	→	14
comp_f_g#1₂(4,5,14)	→	3
Cons₂(0,13)	→	15
comp_f_g#1₂(4,5,15)	→	3
comp_f_g#1₂(4,5,13)	→	16
Cons₂(0,16)	→	3
Cons₂(0,13)	→	17
Cons₂(0,17)	→	3
comp_f_g#1₂(4,5,14)	→	14
comp_f_g#1₂(4,5,15)	→	14
comp_f_g#1₂(4,5,14)	→	16
Cons₂(0,14)	→	15
Cons₂(0,15)	→	15
comp_f_g#1₂(4,5,15)	→	16
Cons₂(0,16)	→	14
Cons₂(0,16)	→	16
Cons₂(0,14)	→	17
Cons₂(0,15)	→	17
Cons₂(0,17)	→	14
Cons₂(0,17)	→	16