Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.12)

The rewrite relation of the following TRS is considered.

+(0,y)	→	y	(1)
+(s(x),0)	→	s(x)	(2)
+(s(x),s(y))	→	s(+(s(x),+(y,0)))	(3)

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}

transitions:

0₀	→	0
s₀(0)	→	0
+₀(0,0)	→	1
s₁(0)	→	1
s₁(0)	→	3
0₁	→	5
+₁(0,5)	→	4
+₁(3,4)	→	2
s₁(2)	→	1
s₁(0)	→	4
s₂(0)	→	2
s₂(0)	→	7
0₂	→	9
+₂(0,9)	→	8
+₂(7,8)	→	6
s₂(6)	→	2
s₁(0)	→	8
s₃(0)	→	6
s₂(6)	→	6
0	→	1
5	→	4
9	→	8