Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/54532)

The rewrite relation of the following TRS is considered.

0(x1)	→	1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(1)
2(x1)	→	3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(2)
0(1(2(3(4(5(4(5(x1))))))))	→	0(1(2(3(4(4(5(5(x1))))))))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

0(x1)	→	1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(1)
2(x1)	→	3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(3(...display limit reached...)))))))))))))))))))))))))))))))))))))))))))))))))))	(2)
5(4(5(4(3(2(1(0(x1))))))))	→	5(5(4(4(3(2(1(0(x1))))))))	(4)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

5^#(4(5(4(3(2(1(0(x1))))))))	→	5^#(4(4(3(2(1(0(x1)))))))	(5)
5^#(4(5(4(3(2(1(0(x1))))))))	→	5^#(5(4(4(3(2(1(0(x1))))))))	(6)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.