Certification Problem

Input (TPDB TRS_Standard/AProVE_10/ex5)

The rewrite relation of the following TRS is considered.

g(0)	→	0	(1)
g(s(x))	→	f(g(x))	(2)
f(0)	→	0	(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 2. This is shown by the following automaton.

final states:

{0, 1, 2, 3}

transitions:

g₀(0)	→	0
g₀(1)	→	0
g₀(2)	→	0
g₀(3)	→	0
0₀	→	1
s₀(0)	→	2
s₀(1)	→	2
s₀(2)	→	2
s₀(3)	→	2
f₀(0)	→	3
f₀(1)	→	3
f₀(2)	→	3
f₀(3)	→	3
0₁	→	0
g₁(0)	→	4
f₁(4)	→	0
g₁(1)	→	4
g₁(2)	→	4
g₁(3)	→	4
0₂	→	0
0	→	3
0	→	4