Certification Problem

Input (TPDB TRS_Standard/Rubio_04/p266)

The rewrite relation of the following TRS is considered.

f(f(X))	→	f(a(b(f(X))))	(1)
f(a(g(X)))	→	b(X)	(2)
b(X)	→	a(X)	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

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:

f₀(0)	→	0
f₀(1)	→	0
f₀(2)	→	0
f₀(3)	→	0
a₀(0)	→	1
a₀(1)	→	1
a₀(2)	→	1
a₀(3)	→	1
b₀(0)	→	2
b₀(1)	→	2
b₀(2)	→	2
b₀(3)	→	2
g₀(0)	→	3
g₀(1)	→	3
g₀(2)	→	3
g₀(3)	→	3
f₁(0)	→	6
b₁(6)	→	5
a₁(5)	→	4
f₁(4)	→	0
f₁(1)	→	6
f₁(2)	→	6
f₁(3)	→	6
b₁(0)	→	0
b₁(1)	→	0
b₁(2)	→	0
b₁(3)	→	0
a₁(0)	→	2
a₁(1)	→	2
a₁(2)	→	2
a₁(3)	→	2
f₂(4)	→	9
b₂(9)	→	8
a₂(8)	→	7
f₂(7)	→	6
a₂(0)	→	0
a₂(1)	→	0
a₂(3)	→	0
a₂(6)	→	5
a₃(9)	→	8
2	→	4
4	→	0
0	→	6
0	→	5
5	→	9