Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z113)

The rewrite relation of the following TRS is considered.

1(1(x1)) → 4(3(x1)) (1)
1(2(x1)) → 2(1(x1)) (2)
2(2(x1)) → 1(1(1(x1))) (3)
3(3(x1)) → 5(6(x1)) (4)
3(4(x1)) → 1(1(x1)) (5)
4(4(x1)) → 3(x1) (6)
5(5(x1)) → 6(2(x1)) (7)
5(6(x1)) → 1(2(x1)) (8)
6(6(x1)) → 2(1(x1)) (9)

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.
1#(2(x1)) → 1#(x1) (10)
5#(5(x1)) → 6#(2(x1)) (11)
1#(1(x1)) → 4#(3(x1)) (12)
3#(4(x1)) → 1#(x1) (13)
2#(2(x1)) → 1#(1(x1)) (14)
2#(2(x1)) → 1#(x1) (15)
1#(1(x1)) → 3#(x1) (16)
5#(5(x1)) → 2#(x1) (17)
2#(2(x1)) → 1#(1(1(x1))) (18)
6#(6(x1)) → 1#(x1) (19)
3#(3(x1)) → 5#(6(x1)) (20)
5#(6(x1)) → 2#(x1) (21)
4#(4(x1)) → 3#(x1) (22)
1#(2(x1)) → 2#(1(x1)) (23)
3#(4(x1)) → 1#(1(x1)) (24)
5#(6(x1)) → 1#(2(x1)) (25)
6#(6(x1)) → 2#(1(x1)) (26)
3#(3(x1)) → 6#(x1) (27)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.