Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex4_7_77_Bor03_FR)

The rewrite relation of the following TRS is considered.

zeros	→	cons(0,n__zeros)	(1)
tail(cons(X,XS))	→	activate(XS)	(2)
zeros	→	n__zeros	(3)
activate(n__zeros)	→	zeros	(4)
activate(X)	→	X	(5)

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:

cons₀(0,0)	→	0
0₀	→	0
n__zeros₀	→	0
zeros₀	→	1
tail₀(0)	→	2
activate₀(0)	→	3
0₁	→	4
n__zeros₁	→	5
cons₁(4,5)	→	1
activate₁(0)	→	2
n__zeros₁	→	1
zeros₁	→	3
0₂	→	6
n__zeros₂	→	7
cons₂(6,7)	→	3
n__zeros₂	→	3
zeros₁	→	2
cons₂(6,7)	→	2
n__zeros₂	→	2
0	→	3
0	→	2