Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/264405)

The rewrite relation of the following TRS is considered.

0(1(2(3(4(x1))))) 0(2(3(1(4(x1))))) (1)
0(5(1(2(3(4(x1)))))) 0(1(2(5(3(4(x1)))))) (2)
0(5(1(2(3(4(x1)))))) 0(5(2(1(3(4(x1)))))) (3)
0(5(1(2(3(4(x1)))))) 5(0(2(3(1(4(x1)))))) (4)
0(5(2(3(1(4(x1)))))) 0(1(5(2(3(4(x1)))))) (5)

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.