Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212062)

The rewrite relation of the following TRS is considered.

0(0(x1)) 0(1(0(2(x1)))) (1)
0(0(x1)) 1(0(2(0(x1)))) (2)
0(0(x1)) 1(0(1(0(1(x1))))) (3)
0(0(x1)) 1(0(1(2(0(x1))))) (4)
0(0(x1)) 1(0(2(0(3(x1))))) (5)
0(0(x1)) 1(0(2(2(0(x1))))) (6)
0(0(x1)) 2(1(0(2(0(x1))))) (7)
0(0(x1)) 0(1(0(2(1(2(x1)))))) (8)
0(0(x1)) 1(0(1(0(2(2(x1)))))) (9)
0(0(x1)) 1(0(1(3(0(1(x1)))))) (10)
0(0(x1)) 1(0(4(1(0(2(x1)))))) (11)
0(0(x1)) 1(1(1(0(2(0(x1)))))) (12)
0(0(x1)) 3(0(4(0(2(2(x1)))))) (13)
0(0(x1)) 3(1(0(1(0(4(x1)))))) (14)
0(0(0(x1))) 0(1(0(4(0(4(x1)))))) (15)
0(0(0(x1))) 3(0(0(1(0(2(x1)))))) (16)
3(0(0(x1))) 3(0(2(0(3(x1))))) (17)
3(0(0(x1))) 3(0(2(4(0(2(x1)))))) (18)
5(2(0(x1))) 0(2(3(5(x1)))) (19)
5(2(0(x1))) 3(5(0(2(x1)))) (20)
5(2(0(x1))) 0(2(3(3(5(x1))))) (21)
5(2(0(x1))) 1(0(2(3(5(x1))))) (22)
5(2(0(x1))) 5(1(0(2(4(x1))))) (23)
5(2(0(x1))) 5(0(1(2(2(2(x1)))))) (24)
5(2(0(x1))) 5(3(5(1(0(2(x1)))))) (25)
0(5(2(0(x1)))) 0(5(0(2(2(x1))))) (26)
3(4(0(0(x1)))) 0(3(3(0(4(5(x1)))))) (27)
3(4(0(0(x1)))) 3(0(4(5(3(0(x1)))))) (28)
5(1(0(0(x1)))) 0(3(1(0(1(5(x1)))))) (29)
5(1(4(0(x1)))) 0(1(5(2(4(x1))))) (30)
5(1(5(0(x1)))) 5(1(0(3(5(x1))))) (31)
5(2(2(0(x1)))) 0(2(1(2(4(5(x1)))))) (32)
5(3(2(0(x1)))) 5(3(0(1(2(x1))))) (33)
5(3(2(0(x1)))) 3(3(5(3(0(2(x1)))))) (34)
5(4(0(0(x1)))) 0(4(5(5(0(2(x1)))))) (35)
5(4(2(0(x1)))) 2(4(3(5(0(x1))))) (36)
5(4(2(0(x1)))) 5(0(2(2(4(x1))))) (37)
5(4(2(0(x1)))) 5(4(5(0(2(x1))))) (38)
0(3(5(2(0(x1))))) 3(0(2(5(3(0(x1)))))) (39)
3(3(5(2(0(x1))))) 3(5(2(3(0(2(x1)))))) (40)
3(3(5(2(0(x1))))) 4(3(3(5(0(2(x1)))))) (41)
5(0(5(2(0(x1))))) 0(3(5(5(0(2(x1)))))) (42)
5(1(4(0(0(x1))))) 0(2(5(0(1(4(x1)))))) (43)
5(3(3(2(0(x1))))) 5(2(3(3(0(2(x1)))))) (44)
5(4(3(0(0(x1))))) 1(0(4(0(3(5(x1)))))) (45)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
0(0(x1)) 2(0(1(0(x1)))) (46)
0(0(x1)) 0(2(0(1(x1)))) (47)
0(0(x1)) 1(0(1(0(1(x1))))) (3)
0(0(x1)) 0(2(1(0(1(x1))))) (48)
0(0(x1)) 3(0(2(0(1(x1))))) (49)
0(0(x1)) 0(2(2(0(1(x1))))) (50)
0(0(x1)) 0(2(0(1(2(x1))))) (51)
0(0(x1)) 2(1(2(0(1(0(x1)))))) (52)
0(0(x1)) 2(2(0(1(0(1(x1)))))) (53)
0(0(x1)) 1(0(3(1(0(1(x1)))))) (54)
0(0(x1)) 2(0(1(4(0(1(x1)))))) (55)
0(0(x1)) 0(2(0(1(1(1(x1)))))) (56)
0(0(x1)) 2(2(0(4(0(3(x1)))))) (57)
0(0(x1)) 4(0(1(0(1(3(x1)))))) (58)
0(0(0(x1))) 4(0(4(0(1(0(x1)))))) (59)
0(0(0(x1))) 2(0(1(0(0(3(x1)))))) (60)
0(0(3(x1))) 3(0(2(0(3(x1))))) (61)
0(0(3(x1))) 2(0(4(2(0(3(x1)))))) (62)
0(2(5(x1))) 5(3(2(0(x1)))) (63)
0(2(5(x1))) 2(0(5(3(x1)))) (64)
0(2(5(x1))) 5(3(3(2(0(x1))))) (65)
0(2(5(x1))) 5(3(2(0(1(x1))))) (66)
0(2(5(x1))) 4(2(0(1(5(x1))))) (67)
0(2(5(x1))) 2(2(2(1(0(5(x1)))))) (68)
0(2(5(x1))) 2(0(1(5(3(5(x1)))))) (69)
0(2(5(0(x1)))) 2(2(0(5(0(x1))))) (70)
0(0(4(3(x1)))) 5(4(0(3(3(0(x1)))))) (71)
0(0(4(3(x1)))) 0(3(5(4(0(3(x1)))))) (72)
0(0(1(5(x1)))) 5(1(0(1(3(0(x1)))))) (73)
0(4(1(5(x1)))) 4(2(5(1(0(x1))))) (74)
0(5(1(5(x1)))) 5(3(0(1(5(x1))))) (75)
0(2(2(5(x1)))) 5(4(2(1(2(0(x1)))))) (76)
0(2(3(5(x1)))) 2(1(0(3(5(x1))))) (77)
0(2(3(5(x1)))) 2(0(3(5(3(3(x1)))))) (78)
0(0(4(5(x1)))) 2(0(5(5(4(0(x1)))))) (79)
0(2(4(5(x1)))) 0(5(3(4(2(x1))))) (80)
0(2(4(5(x1)))) 4(2(2(0(5(x1))))) (81)
0(2(4(5(x1)))) 2(0(5(4(5(x1))))) (82)
0(2(5(3(0(x1))))) 0(3(5(2(0(3(x1)))))) (83)
0(2(5(3(3(x1))))) 2(0(3(2(5(3(x1)))))) (84)
0(2(5(3(3(x1))))) 2(0(5(3(3(4(x1)))))) (85)
0(2(5(0(5(x1))))) 2(0(5(5(3(0(x1)))))) (86)
0(0(4(1(5(x1))))) 4(1(0(5(2(0(x1)))))) (87)
0(2(3(3(5(x1))))) 2(0(3(3(2(5(x1)))))) (88)
0(0(3(4(5(x1))))) 5(3(0(4(0(1(x1)))))) (89)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(5(1(5(x1)))) 0#(1(5(x1))) (90)
0#(4(1(5(x1)))) 0#(x1) (91)
0#(2(5(x1))) 0#(x1) (92)
0#(2(5(x1))) 0#(5(x1)) (93)
0#(2(5(x1))) 0#(5(3(x1))) (94)
0#(2(5(x1))) 0#(1(x1)) (95)
0#(2(5(x1))) 0#(1(5(x1))) (96)
0#(2(5(x1))) 0#(1(5(3(5(x1))))) (97)
0#(2(5(3(3(x1))))) 0#(5(3(3(4(x1))))) (98)
0#(2(5(3(3(x1))))) 0#(3(2(5(3(x1))))) (99)
0#(2(5(3(0(x1))))) 0#(3(x1)) (100)
0#(2(5(3(0(x1))))) 0#(3(5(2(0(3(x1)))))) (101)
0#(2(5(0(x1)))) 0#(5(0(x1))) (102)
0#(2(5(0(5(x1))))) 0#(x1) (103)
0#(2(5(0(5(x1))))) 0#(5(5(3(0(x1))))) (104)
0#(2(4(5(x1)))) 0#(5(x1)) (105)
0#(2(4(5(x1)))) 0#(5(4(5(x1)))) (106)
0#(2(4(5(x1)))) 0#(5(3(4(2(x1))))) (107)
0#(2(3(5(x1)))) 0#(3(5(x1))) (108)
0#(2(3(5(x1)))) 0#(3(5(3(3(x1))))) (109)
0#(2(3(3(5(x1))))) 0#(3(3(2(5(x1))))) (110)
0#(2(2(5(x1)))) 0#(x1) (111)
0#(0(x1)) 0#(4(0(3(x1)))) (112)
0#(0(x1)) 0#(3(x1)) (113)
0#(0(x1)) 0#(3(1(0(1(x1))))) (114)
0#(0(x1)) 0#(2(2(0(1(x1))))) (115)
0#(0(x1)) 0#(2(1(0(1(x1))))) (116)
0#(0(x1)) 0#(2(0(1(x1)))) (117)
0#(0(x1)) 0#(2(0(1(2(x1))))) (118)
0#(0(x1)) 0#(2(0(1(1(1(x1)))))) (119)
0#(0(x1)) 0#(1(x1)) (120)
0#(0(x1)) 0#(1(4(0(1(x1))))) (121)
0#(0(x1)) 0#(1(3(x1))) (122)
0#(0(x1)) 0#(1(2(x1))) (123)
0#(0(x1)) 0#(1(1(1(x1)))) (124)
0#(0(x1)) 0#(1(0(x1))) (125)
0#(0(x1)) 0#(1(0(1(x1)))) (126)
0#(0(x1)) 0#(1(0(1(3(x1))))) (127)
0#(0(4(5(x1)))) 0#(x1) (128)
0#(0(4(5(x1)))) 0#(5(5(4(0(x1))))) (129)
0#(0(4(3(x1)))) 0#(x1) (130)
0#(0(4(3(x1)))) 0#(3(x1)) (131)
0#(0(4(3(x1)))) 0#(3(5(4(0(3(x1)))))) (132)
0#(0(4(3(x1)))) 0#(3(3(0(x1)))) (133)
0#(0(4(1(5(x1))))) 0#(x1) (134)
0#(0(4(1(5(x1))))) 0#(5(2(0(x1)))) (135)
0#(0(3(x1))) 0#(4(2(0(3(x1))))) (136)
0#(0(3(x1))) 0#(2(0(3(x1)))) (137)
0#(0(3(4(5(x1))))) 0#(4(0(1(x1)))) (138)
0#(0(3(4(5(x1))))) 0#(1(x1)) (139)
0#(0(1(5(x1)))) 0#(x1) (140)
0#(0(1(5(x1)))) 0#(1(3(0(x1)))) (141)
0#(0(0(x1))) 0#(4(0(1(0(x1))))) (142)
0#(0(0(x1))) 0#(3(x1)) (143)
0#(0(0(x1))) 0#(1(0(x1))) (144)
0#(0(0(x1))) 0#(1(0(0(3(x1))))) (145)
0#(0(0(x1))) 0#(0(3(x1))) (146)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

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 +
0
[1(x1)] = x1 +
0
[0(x1)] = x1 +
1
[0#(x1)] = x1 +
0
together with the usable rules
0(0(x1)) 2(0(1(0(x1)))) (46)
0(0(x1)) 0(2(0(1(x1)))) (47)
0(0(x1)) 1(0(1(0(1(x1))))) (3)
0(0(x1)) 0(2(1(0(1(x1))))) (48)
0(0(x1)) 3(0(2(0(1(x1))))) (49)
0(0(x1)) 0(2(2(0(1(x1))))) (50)
0(0(x1)) 0(2(0(1(2(x1))))) (51)
0(0(x1)) 2(1(2(0(1(0(x1)))))) (52)
0(0(x1)) 2(2(0(1(0(1(x1)))))) (53)
0(0(x1)) 1(0(3(1(0(1(x1)))))) (54)
0(0(x1)) 2(0(1(4(0(1(x1)))))) (55)
0(0(x1)) 0(2(0(1(1(1(x1)))))) (56)
0(0(x1)) 2(2(0(4(0(3(x1)))))) (57)
0(0(x1)) 4(0(1(0(1(3(x1)))))) (58)
0(0(0(x1))) 4(0(4(0(1(0(x1)))))) (59)
0(0(0(x1))) 2(0(1(0(0(3(x1)))))) (60)
0(0(3(x1))) 3(0(2(0(3(x1))))) (61)
0(0(3(x1))) 2(0(4(2(0(3(x1)))))) (62)
0(2(5(x1))) 5(3(2(0(x1)))) (63)
0(2(5(x1))) 2(0(5(3(x1)))) (64)
0(2(5(x1))) 5(3(3(2(0(x1))))) (65)
0(2(5(x1))) 5(3(2(0(1(x1))))) (66)
0(2(5(x1))) 4(2(0(1(5(x1))))) (67)
0(2(5(x1))) 2(2(2(1(0(5(x1)))))) (68)
0(2(5(x1))) 2(0(1(5(3(5(x1)))))) (69)
0(2(5(0(x1)))) 2(2(0(5(0(x1))))) (70)
0(0(4(3(x1)))) 5(4(0(3(3(0(x1)))))) (71)
0(0(4(3(x1)))) 0(3(5(4(0(3(x1)))))) (72)
0(0(1(5(x1)))) 5(1(0(1(3(0(x1)))))) (73)
0(4(1(5(x1)))) 4(2(5(1(0(x1))))) (74)
0(5(1(5(x1)))) 5(3(0(1(5(x1))))) (75)
0(2(2(5(x1)))) 5(4(2(1(2(0(x1)))))) (76)
0(2(3(5(x1)))) 2(1(0(3(5(x1))))) (77)
0(2(3(5(x1)))) 2(0(3(5(3(3(x1)))))) (78)
0(0(4(5(x1)))) 2(0(5(5(4(0(x1)))))) (79)
0(2(4(5(x1)))) 0(5(3(4(2(x1))))) (80)
0(2(4(5(x1)))) 4(2(2(0(5(x1))))) (81)
0(2(4(5(x1)))) 2(0(5(4(5(x1))))) (82)
0(2(5(3(0(x1))))) 0(3(5(2(0(3(x1)))))) (83)
0(2(5(3(3(x1))))) 2(0(3(2(5(3(x1)))))) (84)
0(2(5(3(3(x1))))) 2(0(5(3(3(4(x1)))))) (85)
0(2(5(0(5(x1))))) 2(0(5(5(3(0(x1)))))) (86)
0(0(4(1(5(x1))))) 4(1(0(5(2(0(x1)))))) (87)
0(2(3(3(5(x1))))) 2(0(3(3(2(5(x1)))))) (88)
0(0(3(4(5(x1))))) 5(3(0(4(0(1(x1)))))) (89)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
0#(2(5(3(0(x1))))) 0#(3(x1)) (100)
0#(2(5(0(5(x1))))) 0#(x1) (103)
0#(0(x1)) 0#(3(x1)) (113)
0#(0(x1)) 0#(1(x1)) (120)
0#(0(x1)) 0#(1(3(x1))) (122)
0#(0(x1)) 0#(1(2(x1))) (123)
0#(0(x1)) 0#(1(1(1(x1)))) (124)
0#(0(4(5(x1)))) 0#(x1) (128)
0#(0(4(3(x1)))) 0#(x1) (130)
0#(0(4(3(x1)))) 0#(3(x1)) (131)
0#(0(4(1(5(x1))))) 0#(x1) (134)
0#(0(3(4(5(x1))))) 0#(1(x1)) (139)
0#(0(1(5(x1)))) 0#(x1) (140)
0#(0(0(x1))) 0#(3(x1)) (143)
0#(0(0(x1))) 0#(1(0(x1))) (144)
0#(0(0(x1))) 0#(0(3(x1))) (146)
and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.