Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.16)

The rewrite relation of the following TRS is considered.

f(0)	→	s(0)	(1)
f(s(0))	→	s(s(0))	(2)
f(s(0))	→	*(s(s(0)),f(0))	(3)
f(+(x,s(0)))	→	+(s(s(0)),f(x))	(4)
f(+(x,y))	→	*(f(x),f(y))	(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}

transitions:

0₀	→	0
s₀(0)	→	0
*₀(0,0)	→	0
+₀(0,0)	→	0
f₀(0)	→	1
0₁	→	2
s₁(2)	→	1
s₁(2)	→	3
s₁(3)	→	1
s₁(3)	→	4
0₁	→	6
f₁(6)	→	5
*₁(4,5)	→	1
s₁(3)	→	7
f₁(0)	→	8
+₁(7,8)	→	1
f₁(0)	→	9
f₁(0)	→	10
*₁(9,10)	→	1
s₁(2)	→	8
s₁(2)	→	9
s₁(2)	→	10
0₂	→	11
s₂(11)	→	5
s₁(3)	→	8
s₁(3)	→	9
s₁(3)	→	10
*₁(4,5)	→	8
*₁(4,5)	→	9
*₁(4,5)	→	10
+₁(7,8)	→	8
+₁(7,8)	→	9
+₁(7,8)	→	10
*₁(9,10)	→	8
*₁(9,10)	→	9
*₁(9,10)	→	10