Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/158152)

The rewrite relation of the following TRS is considered.

0(1(1(2(x1)))) → 1(0(1(3(2(x1))))) (1)
0(1(1(2(x1)))) → 4(1(0(1(2(x1))))) (2)
0(1(1(2(x1)))) → 0(1(4(1(3(2(x1)))))) (3)
0(1(1(2(x1)))) → 0(4(1(4(1(2(x1)))))) (4)
0(1(1(2(x1)))) → 4(1(0(3(1(2(x1)))))) (5)
0(1(1(2(x1)))) → 4(1(3(1(0(2(x1)))))) (6)
0(1(1(5(x1)))) → 4(1(0(1(5(x1))))) (7)
0(1(1(5(x1)))) → 5(4(1(0(1(x1))))) (8)
0(1(1(5(x1)))) → 0(4(1(0(1(5(x1)))))) (9)
0(1(1(5(x1)))) → 0(5(4(1(0(1(x1)))))) (10)
0(1(1(5(x1)))) → 1(0(1(3(1(5(x1)))))) (11)
0(1(1(5(x1)))) → 1(4(4(0(1(5(x1)))))) (12)
0(1(1(5(x1)))) → 3(0(1(5(4(1(x1)))))) (13)
0(1(1(5(x1)))) → 3(4(1(0(1(5(x1)))))) (14)
0(1(1(5(x1)))) → 3(4(1(5(0(1(x1)))))) (15)
0(1(1(5(x1)))) → 3(5(4(1(0(1(x1)))))) (16)
0(1(1(5(x1)))) → 4(1(0(1(5(3(x1)))))) (17)
0(1(1(5(x1)))) → 4(1(0(1(5(4(x1)))))) (18)
0(1(1(5(x1)))) → 4(1(3(1(0(5(x1)))))) (19)
0(1(1(5(x1)))) → 4(1(4(1(0(5(x1)))))) (20)
0(1(1(5(x1)))) → 4(4(1(5(0(1(x1)))))) (21)
0(1(1(5(x1)))) → 5(4(1(3(1(0(x1)))))) (22)
0(1(2(0(x1)))) → 0(2(4(1(0(3(x1)))))) (23)
0(1(3(5(x1)))) → 0(3(5(4(1(x1))))) (24)
0(1(4(5(x1)))) → 0(3(5(4(1(x1))))) (25)
0(1(4(5(x1)))) → 4(4(0(1(5(3(x1)))))) (26)
0(2(4(5(x1)))) → 4(0(2(3(5(x1))))) (27)
0(2(4(5(x1)))) → 4(4(0(2(5(x1))))) (28)
0(2(4(5(x1)))) → 4(0(3(2(3(5(x1)))))) (29)
0(0(2(1(5(x1))))) → 0(0(2(5(4(1(x1)))))) (30)
0(0(2(4(5(x1))))) → 0(0(4(4(2(5(x1)))))) (31)
0(1(0(4(5(x1))))) → 0(4(0(0(1(5(x1)))))) (32)
0(1(0(5(0(x1))))) → 4(1(5(0(0(0(x1)))))) (33)
0(1(1(0(5(x1))))) → 1(0(4(0(1(5(x1)))))) (34)
0(1(1(2(0(x1))))) → 0(4(1(2(1(0(x1)))))) (35)
0(1(1(2(0(x1))))) → 4(1(2(1(0(0(x1)))))) (36)
0(1(1(3(5(x1))))) → 4(1(0(1(3(5(x1)))))) (37)
0(1(1(3(5(x1))))) → 5(4(1(0(3(1(x1)))))) (38)
0(1(1(4(2(x1))))) → 0(4(1(4(1(2(x1)))))) (39)
0(1(1(4(2(x1))))) → 4(1(3(1(2(0(x1)))))) (40)
0(1(1(4(2(x1))))) → 4(2(4(1(0(1(x1)))))) (41)
0(1(1(4(5(x1))))) → 0(5(4(1(3(1(x1)))))) (42)
0(1(1(4(5(x1))))) → 0(5(4(1(4(1(x1)))))) (43)
0(1(1(4(5(x1))))) → 2(4(1(0(1(5(x1)))))) (44)
0(1(2(0(2(x1))))) → 0(4(0(1(2(2(x1)))))) (45)
0(1(2(1(5(x1))))) → 0(1(4(1(2(5(x1)))))) (46)
0(1(4(5(0(x1))))) → 0(5(4(1(0(3(x1)))))) (47)
0(1(5(1(5(x1))))) → 5(4(1(0(1(5(x1)))))) (48)
0(2(0(1(5(x1))))) → 1(0(0(2(3(5(x1)))))) (49)
0(2(0(4(5(x1))))) → 0(0(2(4(1(5(x1)))))) (50)
0(2(0(5(0(x1))))) → 0(2(5(0(3(0(x1)))))) (51)
0(2(3(1(5(x1))))) → 0(0(1(2(3(5(x1)))))) (52)
0(2(3(1(5(x1))))) → 0(2(5(3(4(1(x1)))))) (53)
0(2(3(1(5(x1))))) → 0(3(5(2(4(1(x1)))))) (54)
0(2(3(1(5(x1))))) → 2(0(4(1(3(5(x1)))))) (55)
0(2(3(1(5(x1))))) → 2(0(4(1(5(3(x1)))))) (56)
0(2(3(1(5(x1))))) → 2(3(5(3(0(1(x1)))))) (57)
0(2(3(1(5(x1))))) → 2(5(3(4(1(0(x1)))))) (58)
0(2(3(1(5(x1))))) → 4(1(0(5(2(3(x1)))))) (59)
0(2(3(1(5(x1))))) → 4(1(3(0(2(5(x1)))))) (60)
0(2(3(1(5(x1))))) → 4(1(5(2(0(3(x1)))))) (61)
0(2(5(1(2(x1))))) → 0(2(3(2(1(5(x1)))))) (62)
0(2(5(1(5(x1))))) → 0(3(5(2(1(5(x1)))))) (63)
0(2(5(1(5(x1))))) → 0(4(1(5(2(5(x1)))))) (64)
0(2(5(1(5(x1))))) → 2(4(1(5(0(5(x1)))))) (65)
0(2(5(1(5(x1))))) → 4(1(0(5(2(5(x1)))))) (66)
0(2(5(1(5(x1))))) → 4(1(5(5(2(0(x1)))))) (67)
0(3(5(1(5(x1))))) → 5(0(3(5(4(1(x1)))))) (68)
0(4(2(0(2(x1))))) → 0(0(4(3(2(2(x1)))))) (69)
0(4(2(1(5(x1))))) → 0(2(5(4(4(1(x1)))))) (70)
0(4(2(1(5(x1))))) → 0(4(1(5(3(2(x1)))))) (71)
0(4(2(1(5(x1))))) → 2(4(1(0(0(5(x1)))))) (72)
0(4(2(1(5(x1))))) → 2(4(1(3(0(5(x1)))))) (73)
0(4(2(1(5(x1))))) → 2(4(1(5(4(0(x1)))))) (74)
0(4(2(1(5(x1))))) → 3(0(1(5(2(4(x1)))))) (75)
0(4(2(1(5(x1))))) → 3(0(5(2(4(1(x1)))))) (76)
0(4(2(1(5(x1))))) → 4(1(3(2(5(0(x1)))))) (77)
0(4(2(1(5(x1))))) → 4(4(0(1(5(2(x1)))))) (78)
0(4(5(1(5(x1))))) → 5(4(1(5(0(4(x1)))))) (79)

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.
0#(1(1(4(5(x1))))) → 0#(5(4(1(4(1(x1)))))) (80)
0#(1(1(5(x1)))) → 0#(1(x1)) (81)
0#(1(1(5(x1)))) → 0#(1(5(x1))) (82)
0#(1(1(5(x1)))) → 0#(4(1(0(1(5(x1)))))) (83)
0#(4(2(1(5(x1))))) → 0#(2(5(4(4(1(x1)))))) (84)
0#(3(5(1(5(x1))))) → 0#(3(5(4(1(x1))))) (85)
0#(4(2(1(5(x1))))) → 0#(5(x1)) (86)
0#(4(5(1(5(x1))))) → 0#(4(x1)) (87)
0#(4(2(0(2(x1))))) → 0#(4(3(2(2(x1))))) (88)
0#(2(0(4(5(x1))))) → 0#(2(4(1(5(x1))))) (89)
0#(4(2(0(2(x1))))) → 0#(0(4(3(2(2(x1)))))) (90)
0#(1(2(0(x1)))) → 0#(3(x1)) (91)
0#(1(1(5(x1)))) → 0#(1(x1)) (81)
0#(1(1(0(5(x1))))) → 0#(1(5(x1))) (92)
0#(2(3(1(5(x1))))) → 0#(4(1(5(3(x1))))) (93)
0#(2(3(1(5(x1))))) → 0#(1(2(3(5(x1))))) (94)
0#(1(1(5(x1)))) → 0#(x1) (95)
0#(1(1(5(x1)))) → 0#(1(5(x1))) (82)
0#(2(3(1(5(x1))))) → 0#(2(5(x1))) (96)
0#(2(4(5(x1)))) → 0#(2(3(5(x1)))) (97)
0#(1(1(5(x1)))) → 0#(1(5(x1))) (82)
0#(1(1(5(x1)))) → 0#(1(x1)) (81)
0#(4(2(1(5(x1))))) → 0#(1(5(2(x1)))) (98)
0#(1(2(1(5(x1))))) → 0#(1(4(1(2(5(x1)))))) (99)
0#(1(1(4(2(x1))))) → 0#(4(1(4(1(2(x1)))))) (100)
0#(2(0(1(5(x1))))) → 0#(2(3(5(x1)))) (101)
0#(1(1(2(x1)))) → 0#(3(1(2(x1)))) (102)
0#(1(2(0(2(x1))))) → 0#(1(2(2(x1)))) (103)
0#(2(3(1(5(x1))))) → 0#(3(5(2(4(1(x1)))))) (104)
0#(0(2(1(5(x1))))) → 0#(2(5(4(1(x1))))) (105)
0#(2(3(1(5(x1))))) → 0#(2(5(3(4(1(x1)))))) (106)
0#(1(1(3(5(x1))))) → 0#(1(3(5(x1)))) (107)
0#(1(4(5(0(x1))))) → 0#(5(4(1(0(3(x1)))))) (108)
0#(1(1(5(x1)))) → 0#(5(x1)) (109)
0#(1(1(5(x1)))) → 0#(1(5(3(x1)))) (110)
0#(2(0(4(5(x1))))) → 0#(0(2(4(1(5(x1)))))) (111)
0#(2(5(1(5(x1))))) → 0#(x1) (112)
0#(2(4(5(x1)))) → 0#(2(5(x1))) (113)
0#(2(3(1(5(x1))))) → 0#(4(1(3(5(x1))))) (114)
0#(2(5(1(5(x1))))) → 0#(3(5(2(1(5(x1)))))) (115)
0#(1(0(4(5(x1))))) → 0#(0(1(5(x1)))) (116)
0#(0(2(4(5(x1))))) → 0#(4(4(2(5(x1))))) (117)
0#(1(1(5(x1)))) → 0#(1(5(4(x1)))) (118)
0#(2(5(1(5(x1))))) → 0#(5(x1)) (119)
0#(1(4(5(0(x1))))) → 0#(3(x1)) (120)
0#(1(1(5(x1)))) → 0#(1(3(1(5(x1))))) (121)
0#(1(0(4(5(x1))))) → 0#(1(5(x1))) (122)
0#(1(4(5(x1)))) → 0#(3(5(4(1(x1))))) (123)
0#(1(1(2(x1)))) → 0#(1(3(2(x1)))) (124)
0#(1(4(5(x1)))) → 0#(1(5(3(x1)))) (125)
0#(4(2(1(5(x1))))) → 0#(4(1(5(3(2(x1)))))) (126)
0#(2(5(1(5(x1))))) → 0#(4(1(5(2(5(x1)))))) (127)
0#(1(1(5(x1)))) → 0#(1(5(x1))) (82)
0#(2(3(1(5(x1))))) → 0#(0(1(2(3(5(x1)))))) (128)
0#(2(5(1(2(x1))))) → 0#(2(3(2(1(5(x1)))))) (129)
0#(1(1(4(2(x1))))) → 0#(x1) (130)
0#(1(1(3(5(x1))))) → 0#(3(1(x1))) (131)
0#(4(2(1(5(x1))))) → 0#(x1) (132)
0#(1(1(4(5(x1))))) → 0#(5(4(1(3(1(x1)))))) (133)
0#(1(2(0(2(x1))))) → 0#(4(0(1(2(2(x1)))))) (134)
0#(4(2(1(5(x1))))) → 0#(5(x1)) (86)
0#(1(1(5(x1)))) → 0#(1(x1)) (81)
0#(1(1(2(x1)))) → 0#(4(1(4(1(2(x1)))))) (135)
0#(1(0(5(0(x1))))) → 0#(0(x1)) (136)
0#(4(2(1(5(x1))))) → 0#(5(2(4(1(x1))))) (137)
0#(1(1(0(5(x1))))) → 0#(4(0(1(5(x1))))) (138)
0#(2(5(1(5(x1))))) → 0#(5(2(5(x1)))) (139)
0#(0(2(4(5(x1))))) → 0#(0(4(4(2(5(x1)))))) (140)
0#(4(2(1(5(x1))))) → 0#(0(5(x1))) (141)
0#(1(1(5(x1)))) → 0#(1(5(4(1(x1))))) (142)
0#(2(3(1(5(x1))))) → 0#(5(2(3(x1)))) (143)
0#(1(3(5(x1)))) → 0#(3(5(4(1(x1))))) (144)
0#(1(1(2(0(x1))))) → 0#(0(x1)) (145)
0#(1(1(2(x1)))) → 0#(1(4(1(3(2(x1)))))) (146)
0#(2(0(5(0(x1))))) → 0#(3(0(x1))) (147)
0#(1(1(5(x1)))) → 0#(5(4(1(0(1(x1)))))) (148)
0#(4(2(1(5(x1))))) → 0#(x1) (132)
0#(2(3(1(5(x1))))) → 0#(1(x1)) (149)
0#(2(3(1(5(x1))))) → 0#(3(x1)) (150)
0#(1(0(5(0(x1))))) → 0#(0(0(x1))) (151)
0#(2(0(5(0(x1))))) → 0#(2(5(0(3(0(x1)))))) (152)
0#(1(1(5(x1)))) → 0#(1(x1)) (81)
0#(1(1(4(5(x1))))) → 0#(1(5(x1))) (153)
0#(1(2(0(x1)))) → 0#(2(4(1(0(3(x1)))))) (154)
0#(1(1(2(x1)))) → 0#(2(x1)) (155)
0#(4(2(1(5(x1))))) → 0#(1(5(2(4(x1))))) (156)
0#(2(4(5(x1)))) → 0#(3(2(3(5(x1))))) (157)
0#(1(0(4(5(x1))))) → 0#(4(0(0(1(5(x1)))))) (158)
0#(1(1(2(x1)))) → 0#(1(2(x1))) (159)
0#(2(0(1(5(x1))))) → 0#(0(2(3(5(x1))))) (160)
0#(1(1(4(2(x1))))) → 0#(1(x1)) (161)
0#(1(5(1(5(x1))))) → 0#(1(5(x1))) (162)
0#(1(1(2(0(x1))))) → 0#(4(1(2(1(0(x1)))))) (163)
0#(1(1(5(x1)))) → 0#(5(x1)) (109)
0#(0(2(1(5(x1))))) → 0#(0(2(5(4(1(x1)))))) (164)
0#(2(3(1(5(x1))))) → 0#(x1) (165)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.