Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/264370)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(5(4(1(3(2(x1)))))) 0#(5(4(3(1(2(x1)))))) (6)
0#(5(3(1(2(4(x1)))))) 0#(1(5(3(2(4(x1)))))) (7)
0#(5(2(4(1(3(x1)))))) 0#(1(5(2(4(3(x1)))))) (8)
0#(5(1(2(4(3(x1)))))) 0#(5(2(1(4(3(x1)))))) (9)
0#(1(2(3(4(x1))))) 0#(2(1(3(4(x1))))) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.