Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex4_7_15_Bor03_GM)

The rewrite relation of the following TRS is considered.

a__f(0)	→	cons(0,f(s(0)))	(1)
a__f(s(0))	→	a__f(a__p(s(0)))	(2)
a__p(s(0))	→	0	(3)
mark(f(X))	→	a__f(mark(X))	(4)
mark(p(X))	→	a__p(mark(X))	(5)
mark(0)	→	0	(6)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(7)
mark(s(X))	→	s(mark(X))	(8)
a__f(X)	→	f(X)	(9)
a__p(X)	→	p(X)	(10)

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:

0₀	→	0
cons₀(0,0)	→	0
f₀(0)	→	0
s₀(0)	→	0
p₀(0)	→	0
a__f₀(0)	→	1
a__p₀(0)	→	2
mark₀(0)	→	3
0₁	→	4
0₁	→	7
s₁(7)	→	6
f₁(6)	→	5
cons₁(4,5)	→	1
s₁(7)	→	9
a__p₁(9)	→	8
a__f₁(8)	→	1
0₁	→	2
mark₁(0)	→	10
a__f₁(10)	→	3
mark₁(0)	→	11
a__p₁(11)	→	3
0₁	→	3
mark₁(0)	→	12
cons₁(12,0)	→	3
mark₁(0)	→	13
s₁(13)	→	3
f₁(0)	→	1
p₁(0)	→	2
0₂	→	8
a__f₁(10)	→	10
a__f₁(10)	→	11
a__f₁(10)	→	12
a__f₁(10)	→	13
a__p₁(11)	→	10
a__p₁(11)	→	11
a__p₁(11)	→	12
a__p₁(11)	→	13
0₁	→	10
0₁	→	11
0₁	→	12
0₁	→	13
cons₁(12,0)	→	10
cons₁(12,0)	→	11
cons₁(12,0)	→	12
cons₁(12,0)	→	13
s₁(13)	→	10
s₁(13)	→	11
s₁(13)	→	12
s₁(13)	→	13
f₂(8)	→	1
f₂(10)	→	3
p₂(11)	→	3
p₂(9)	→	8
0₂	→	14
0₂	→	17
s₂(17)	→	16
f₂(16)	→	15
cons₂(14,15)	→	3
cons₂(14,15)	→	10
cons₂(14,15)	→	11
cons₂(14,15)	→	12
cons₂(14,15)	→	13
s₂(17)	→	19
a__p₂(19)	→	18
a__f₂(18)	→	3
a__f₂(18)	→	10
a__f₂(18)	→	11
a__f₂(18)	→	12
a__f₂(18)	→	13
0₂	→	3
0₂	→	10
0₂	→	11
0₂	→	12
0₂	→	13
f₂(10)	→	10
f₂(10)	→	11
f₂(10)	→	12
f₂(10)	→	13
p₂(11)	→	10
p₂(11)	→	11
p₂(11)	→	12
p₂(11)	→	13
cons₂(14,15)	→	1
0₃	→	18
f₃(18)	→	3
f₃(18)	→	10
f₃(18)	→	11
f₃(18)	→	12
f₃(18)	→	13
p₃(19)	→	18
0₃	→	20
0₃	→	23
s₃(23)	→	22
f₃(22)	→	21
cons₃(20,21)	→	3
cons₃(20,21)	→	10
cons₃(20,21)	→	11
cons₃(20,21)	→	12
cons₃(20,21)	→	13