Certification Problem
Input (TPDB TRS_Standard/SK90/4.36)
The rewrite relation of the following TRS is considered.
a
(
a
(
x
))
→
a
(
b
(
a
(
x
)))
(1)
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}
transitions:
a
0
(0)
→
0
a
0
(1)
→
0
b
0
(0)
→
1
b
0
(1)
→
1
a
1
(0)
→
3
b
1
(3)
→
2
a
1
(2)
→
0
a
1
(1)
→
3
a
2
(2)
→
5
b
2
(5)
→
4
a
2
(4)
→
0
a
1
(4)
→
0
0
→
3
0
→
5