Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/PEANO_nosorts-noand_FR)

The rewrite relation of the following TRS is considered.

U11(tt,M,N)	→	U12(tt,activate(M),activate(N))	(1)
U12(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
plus(N,0)	→	N	(3)
plus(N,s(M))	→	U11(tt,M,N)	(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 3. This is shown by the following automaton.

final states:

{0, 1, 2, 3, 4}

transitions:

tt₀	→	0
s₀(0)	→	0
0₀	→	0
U11₀(0,0,0)	→	1
U12₀(0,0,0)	→	2
plus₀(0,0)	→	3
activate₀(0)	→	4
tt₁	→	5
activate₁(0)	→	6
activate₁(0)	→	7
U12₁(5,6,7)	→	1
activate₁(0)	→	9
activate₁(0)	→	10
plus₁(9,10)	→	8
s₁(8)	→	2
tt₁	→	11
U11₁(11,0,0)	→	3
tt₂	→	12
activate₂(0)	→	13
activate₂(0)	→	14
U12₂(12,13,14)	→	3
activate₂(7)	→	16
activate₂(6)	→	17
plus₂(16,17)	→	15
s₂(15)	→	1
U11₁(11,0,9)	→	8
activate₃(14)	→	19
activate₃(13)	→	20
plus₃(19,20)	→	18
s₃(18)	→	3
activate₂(9)	→	14
U12₂(12,13,14)	→	8
U11₁(11,0,16)	→	15
activate₂(16)	→	14
U12₂(12,13,14)	→	15
s₃(18)	→	8
U11₁(11,0,19)	→	18
activate₂(19)	→	14
U12₂(12,13,14)	→	18
s₃(18)	→	15
s₃(18)	→	18
0	→	3
0	→	4
0	→	6
0	→	7
0	→	9
0	→	10
0	→	13
0	→	14
9	→	8
9	→	14
7	→	16
6	→	17
16	→	15
16	→	14
14	→	19
13	→	20
19	→	18
19	→	14