Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/ExProp7_Luc06_L)

The rewrite relation of the following TRS is considered.

f(0)	→	cons(0)	(1)
f(s(0))	→	f(p(s(0)))	(2)
p(s(X))	→	X	(3)

The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

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, 2, 3, 4}

transitions:

f₀(0)	→	0
f₀(1)	→	0
f₀(2)	→	0
f₀(3)	→	0
f₀(4)	→	0
0₀	→	1
cons₀(0)	→	2
cons₀(1)	→	2
cons₀(2)	→	2
cons₀(3)	→	2
cons₀(4)	→	2
s₀(0)	→	3
s₀(1)	→	3
s₀(2)	→	3
s₀(3)	→	3
s₀(4)	→	3
p₀(0)	→	4
p₀(1)	→	4
p₀(2)	→	4
p₀(3)	→	4
p₀(4)	→	4
0₁	→	5
cons₁(5)	→	0
s₁(5)	→	7
p₁(7)	→	6
f₁(6)	→	0
0₂	→	8
cons₂(8)	→	0
0	→	4
1	→	4
2	→	4
3	→	4
5	→	6