Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t000)

The rewrite relation of the following TRS is considered.

There are 104 ruless (increase limit for explicit display).

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.
+#(2,8) → c#(1,0) (105)
+#(8,4) → c#(1,2) (106)
+#(5,5) → c#(1,0) (107)
+#(3,8) → c#(1,1) (108)
+#(c(x,y),z) → c#(x,+(y,z)) (109)
+#(9,9) → c#(1,8) (110)
+#(5,9) → c#(1,4) (111)
+#(9,2) → c#(1,1) (112)
+#(c(x,y),z) → +#(y,z) (113)
c#(x,c(y,z)) → c#(+(x,y),z) (114)
+#(6,4) → c#(1,0) (115)
+#(9,8) → c#(1,7) (116)
+#(8,6) → c#(1,4) (117)
+#(4,9) → c#(1,3) (118)
+#(3,7) → c#(1,0) (119)
+#(4,7) → c#(1,1) (120)
+#(7,3) → c#(1,0) (121)
+#(9,5) → c#(1,4) (122)
+#(7,7) → c#(1,4) (123)
+#(7,6) → c#(1,3) (124)
+#(5,7) → c#(1,2) (125)
+#(2,9) → c#(1,1) (126)
+#(5,8) → c#(1,3) (127)
+#(8,8) → c#(1,6) (128)
c#(x,c(y,z)) → +#(x,y) (129)
+#(6,8) → c#(1,4) (130)
+#(7,5) → c#(1,2) (131)
+#(9,6) → c#(1,5) (132)
+#(8,3) → c#(1,1) (133)
+#(7,4) → c#(1,1) (134)
+#(1,9) → c#(1,0) (135)
+#(9,4) → c#(1,3) (136)
+#(6,7) → c#(1,3) (137)
+#(7,8) → c#(1,5) (138)
+#(6,9) → c#(1,5) (139)
+#(8,7) → c#(1,5) (140)
+#(x,c(y,z)) → +#(x,z) (141)
+#(8,9) → c#(1,7) (142)
+#(4,8) → c#(1,2) (143)
+#(5,6) → c#(1,1) (144)
+#(x,c(y,z)) → c#(y,+(x,z)) (145)
+#(9,1) → c#(1,0) (146)
+#(9,3) → c#(1,2) (147)
+#(3,9) → c#(1,2) (148)
+#(8,2) → c#(1,0) (149)
+#(8,5) → c#(1,3) (150)
+#(4,6) → c#(1,0) (151)
+#(6,6) → c#(1,2) (152)
+#(6,5) → c#(1,1) (153)
+#(7,9) → c#(1,6) (154)
+#(9,7) → c#(1,6) (155)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.