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 AProVE @ 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 Rule Removal

Using the linear polynomial interpretation over the naturals
[0(x1)] = 1 · x1 + 1
[1(x1)] = 1 · x1
[2(x1)] = 1 · x1 + 1
[3(x1)] = 1 · x1
[5(x1)] = 1 · x1
[4(x1)] = 1 · x1
all of the following rules can be deleted.
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)

1.1.1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1.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#(5(4(4(3(2(1(0(x1)))))))) (5)
5#(4(5(4(3(2(1(0(x1)))))))) 5#(4(4(3(2(1(0(x1))))))) (6)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.