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

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[5(x1)] = x1 +
0
[4(x1)] = x1 +
0
[3(x1)] = x1 +
0
[2(x1)] = x1 +
1
[1(x1)] = x1 +
0
[0(x1)] = x1 +
1
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 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(1(2(3(4(5(4(5(x1)))))))) → 0#(1(2(3(4(4(5(5(x1)))))))) (4)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.