Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex5_Zan97_Z)

The rewrite relation of the following TRS is considered.

f(X)	→	if(X,c,n__f(true))	(1)
if(true,X,Y)	→	X	(2)
if(false,X,Y)	→	activate(Y)	(3)
f(X)	→	n__f(X)	(4)
activate(n__f(X))	→	f(X)	(5)
activate(X)	→	X	(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 3. This is shown by the following automaton.

final states:

{0, 1, 2, 3}

transitions:

c₀	→	0
n__f₀(0)	→	0
true₀	→	0
false₀	→	0
f₀(0)	→	1
if₀(0,0,0)	→	2
activate₀(0)	→	3
c₁	→	4
true₁	→	6
n__f₁(6)	→	5
if₁(0,4,5)	→	1
activate₁(0)	→	2
n__f₁(0)	→	1
f₁(0)	→	3
c₂	→	7
true₂	→	9
n__f₂(9)	→	8
if₂(0,7,8)	→	3
activate₁(5)	→	1
n__f₂(0)	→	3
f₁(0)	→	2
if₂(0,7,8)	→	2
n__f₂(0)	→	2
f₂(6)	→	1
activate₁(8)	→	3
activate₁(8)	→	2
f₂(9)	→	3
c₃	→	10
true₃	→	12
n__f₃(12)	→	11
if₃(6,10,11)	→	1
n__f₃(6)	→	1
f₂(9)	→	2
if₃(9,10,11)	→	3
n__f₃(9)	→	3
if₃(9,10,11)	→	2
n__f₃(9)	→	2
0	→	2
0	→	3
4	→	1
5	→	1
7	→	3
7	→	2
8	→	3
8	→	2
10	→	1
10	→	3
10	→	2