Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex18_Luc06_Z)

The rewrite relation of the following TRS is considered.

f(f(a))	→	f(g(n__f(a)))	(1)
f(X)	→	n__f(X)	(2)
activate(n__f(X))	→	f(X)	(3)
activate(X)	→	X	(4)

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
a₀	→	1
g₀(0)	→	2
g₀(1)	→	2
g₀(2)	→	2
g₀(3)	→	2
g₀(4)	→	2
n__f₀(0)	→	3
n__f₀(1)	→	3
n__f₀(2)	→	3
n__f₀(3)	→	3
n__f₀(4)	→	3
activate₀(0)	→	4
activate₀(1)	→	4
activate₀(2)	→	4
activate₀(3)	→	4
activate₀(4)	→	4
a₁	→	7
n__f₁(7)	→	6
g₁(6)	→	5
f₁(5)	→	0
n__f₁(0)	→	0
n__f₁(1)	→	0
n__f₁(2)	→	0
n__f₁(3)	→	0
n__f₁(4)	→	0
f₁(0)	→	4
f₁(1)	→	4
f₁(2)	→	4
f₁(3)	→	4
f₁(4)	→	4
n__f₂(5)	→	0
n__f₂(0)	→	0
n__f₂(1)	→	0
n__f₂(2)	→	0
n__f₂(3)	→	0
n__f₂(4)	→	0
0	→	4
1	→	4
2	→	4
3	→	4