Certification Problem

Input (TPDB TRS_Standard/AProVE_04/improved_usable)

The rewrite relation of the following TRS is considered.

f(a,h(x))	→	f(g(x),h(x))	(1)
h(g(x))	→	h(a)	(2)
g(h(x))	→	g(x)	(3)
h(h(x))	→	x	(4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

The given TRS is roof-(raise)-bounded by 2. This is shown by the following automaton.

final states:

{5}

transitions:

10	→	5
10	→	8
5	→	8
a₁	→	10
f₁(9,8)	→	5
f₁(15,5)	→	5
h₁(5)	→	8
h₁(10)	→	5
h₁(10)	→	8
f₀(5,5)	→	5
a₀	→	5
g₂(10)	→	5
g₂(10)	→	9
h₂(19)	→	8
g₀(5)	→	5
g₁(10)	→	15
g₁(10)	→	5
g₁(5)	→	9
g₁(5)	→	5
a₂	→	19
h₀(5)	→	5

The automaton is closed under rewriting as it is compatible.