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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

0^#(5(2(3(1(4(x1))))))	→	0^#(1(5(2(3(4(x1))))))	(6)
0^#(5(1(2(3(4(x1))))))	→	0^#(2(3(1(4(x1)))))	(7)
0^#(5(1(2(3(4(x1))))))	→	0^#(5(2(1(3(4(x1))))))	(8)
0^#(5(1(2(3(4(x1))))))	→	0^#(1(2(5(3(4(x1))))))	(9)
0^#(1(2(3(4(x1)))))	→	0^#(2(3(1(4(x1)))))	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.