Certification Problem

Input (TPDB TRS_Standard/SK90/4.44)

The rewrite relation of the following TRS is considered.

f(h(x))	→	f(i(x))	(1)
g(i(x))	→	g(h(x))	(2)
h(a)	→	b	(3)
i(a)	→	b	(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 1. This is shown by the following automaton.

final states:

{0, 1, 2, 3, 4, 5}

transitions:

f₀(0)	→	0
f₀(1)	→	0
f₀(2)	→	0
f₀(3)	→	0
f₀(4)	→	0
f₀(5)	→	0
h₀(0)	→	1
h₀(1)	→	1
h₀(2)	→	1
h₀(3)	→	1
h₀(4)	→	1
h₀(5)	→	1
i₀(0)	→	2
i₀(1)	→	2
i₀(2)	→	2
i₀(3)	→	2
i₀(4)	→	2
i₀(5)	→	2
g₀(0)	→	3
g₀(1)	→	3
g₀(2)	→	3
g₀(3)	→	3
g₀(4)	→	3
g₀(5)	→	3
a₀	→	4
b₀	→	5
i₁(0)	→	6
f₁(6)	→	0
i₁(1)	→	6
i₁(2)	→	6
i₁(3)	→	6
i₁(4)	→	6
i₁(5)	→	6
h₁(0)	→	7
g₁(7)	→	3
h₁(1)	→	7
h₁(2)	→	7
h₁(3)	→	7
h₁(4)	→	7
h₁(5)	→	7
b₁	→	1
1	→	2
1	→	7
1	→	6