Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/214091)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0#(1(2(x1))) → 0#(x1) (51)
0#(1(2(x1))) → 2#(1(0(x1))) (52)
0#(1(2(x1))) → 0#(2(1(0(x1)))) (53)
0#(1(2(x1))) → 2#(3(x1)) (54)
0#(1(2(x1))) → 0#(2(3(x1))) (55)
0#(1(2(x1))) → 2#(4(1(5(x1)))) (56)
0#(1(2(x1))) → 0#(2(4(1(5(x1))))) (57)
0#(1(2(x1))) → 0#(3(2(1(0(x1))))) (58)
0#(1(2(x1))) → 0#(3(2(3(x1)))) (59)
0#(1(2(x1))) → 0#(1(3(4(2(3(x1)))))) (60)
0#(5(2(x1))) → 2#(4(5(3(x1)))) (61)
0#(5(2(x1))) → 0#(2(4(5(3(x1))))) (62)
0#(5(2(x1))) → 0#(4(x1)) (63)
0#(5(2(x1))) → 2#(3(0(4(x1)))) (64)
2#(0(1(x1))) → 2#(1(x1)) (65)
2#(0(1(x1))) → 0#(2(1(x1))) (66)
2#(0(1(x1))) → 2#(1(1(4(x1)))) (67)
2#(0(1(x1))) → 0#(2(1(1(4(x1))))) (68)
2#(0(1(x1))) → 2#(4(1(x1))) (69)
2#(0(1(x1))) → 0#(3(2(4(1(x1))))) (70)
2#(0(1(x1))) → 2#(1(4(x1))) (71)
2#(0(1(x1))) → 0#(2(1(4(x1)))) (72)
2#(0(1(x1))) → 2#(3(4(1(x1)))) (73)
2#(0(1(x1))) → 2#(2(3(4(1(x1))))) (74)
2#(0(1(x1))) → 0#(2(2(3(4(1(x1)))))) (75)
2#(0(1(x1))) → 2#(3(1(1(x1)))) (76)
2#(0(1(x1))) → 0#(3(2(3(1(1(x1)))))) (77)
2#(0(1(x1))) → 0#(4(2(1(4(x1))))) (78)
2#(5(1(x1))) → 2#(1(5(1(x1)))) (79)
2#(5(1(x1))) → 0#(2(1(5(1(x1))))) (80)
2#(5(1(x1))) → 2#(x1) (81)
2#(5(1(x1))) → 2#(1(4(x1))) (82)
2#(5(1(x1))) → 0#(2(1(4(x1)))) (83)
2#(5(1(x1))) → 2#(1(4(1(x1)))) (84)
2#(5(1(x1))) → 2#(4(1(x1))) (85)
2#(5(1(x1))) → 0#(2(4(1(x1)))) (86)
2#(5(1(x1))) → 2#(1(1(1(1(x1))))) (87)
0#(1(2(1(x1)))) → 0#(2(1(x1))) (88)
0#(1(3(1(x1)))) → 0#(3(1(1(x1)))) (89)
0#(1(3(1(x1)))) → 2#(1(x1)) (90)
0#(1(3(1(x1)))) → 0#(3(4(2(1(x1))))) (91)
0#(1(5(1(x1)))) → 0#(3(1(1(x1)))) (92)
0#(2(1(2(x1)))) → 2#(1(5(x1))) (93)
0#(2(1(2(x1)))) → 2#(2(1(5(x1)))) (94)
0#(2(1(2(x1)))) → 0#(2(2(1(5(x1))))) (95)
0#(2(5(1(x1)))) → 2#(1(x1)) (96)
0#(2(5(1(x1)))) → 0#(2(1(x1))) (97)
0#(5(3(1(x1)))) → 0#(1(4(4(3(5(x1)))))) (98)
0#(5(5(2(x1)))) → 0#(x1) (99)
0#(5(5(2(x1)))) → 2#(3(5(0(x1)))) (100)
2#(0(1(2(x1)))) → 2#(1(1(x1))) (101)
2#(0(1(2(x1)))) → 2#(3(2(1(1(x1))))) (102)
2#(0(1(2(x1)))) → 0#(2(3(2(1(1(x1)))))) (103)
2#(0(1(2(x1)))) → 2#(1(1(2(x1)))) (104)
2#(0(1(2(x1)))) → 0#(2(1(1(2(x1))))) (105)
2#(0(4(1(x1)))) → 2#(4(1(x1))) (106)
2#(0(4(1(x1)))) → 0#(2(4(1(x1)))) (107)
2#(0(5(1(x1)))) → 0#(x1) (108)
2#(0(5(1(x1)))) → 2#(1(0(x1))) (109)
2#(2(5(1(x1)))) → 2#(4(5(1(x1)))) (110)
2#(2(5(1(x1)))) → 2#(2(4(5(1(x1))))) (111)
2#(4(0(1(x1)))) → 2#(4(4(x1))) (112)
2#(4(0(1(x1)))) → 0#(2(4(4(x1)))) (113)
2#(4(0(1(x1)))) → 2#(4(1(x1))) (114)
2#(4(0(1(x1)))) → 0#(2(4(1(x1)))) (115)
2#(4(0(1(x1)))) → 0#(0(2(4(1(x1))))) (116)
2#(4(0(1(x1)))) → 2#(1(1(x1))) (117)
2#(4(0(1(x1)))) → 0#(2(1(1(x1)))) (118)
2#(5(2(1(x1)))) → 2#(3(1(x1))) (119)
2#(5(2(1(x1)))) → 2#(2(3(1(x1)))) (120)
2#(5(4(1(x1)))) → 2#(1(4(4(x1)))) (121)
2#(5(5(1(x1)))) → 2#(4(5(x1))) (122)
2#(5(5(2(x1)))) → 2#(3(2(x1))) (123)
0#(1(3(0(1(x1))))) → 0#(1(1(x1))) (124)
0#(1(3(0(1(x1))))) → 0#(3(1(0(1(1(x1)))))) (125)
0#(2(4(3(1(x1))))) → 0#(x1) (126)
0#(2(4(3(1(x1))))) → 2#(3(0(x1))) (127)
0#(2(4(3(1(x1))))) → 2#(1(0(x1))) (128)
0#(2(4(3(1(x1))))) → 0#(3(2(1(0(x1))))) (129)
0#(2(5(3(1(x1))))) → 2#(3(5(1(x1)))) (130)
0#(2(5(3(1(x1))))) → 0#(2(3(5(1(x1))))) (131)
2#(0(5(4(1(x1))))) → 2#(1(x1)) (132)
2#(0(5(4(1(x1))))) → 0#(4(5(3(2(1(x1)))))) (133)
2#(2(0(1(2(x1))))) → 2#(1(x1)) (134)
2#(2(0(1(2(x1))))) → 2#(2(1(x1))) (135)
2#(2(0(1(2(x1))))) → 0#(2(2(1(x1)))) (136)
2#(2(0(1(2(x1))))) → 2#(4(0(2(2(1(x1)))))) (137)
2#(4(0(5(1(x1))))) → 2#(x1) (138)
2#(4(0(5(1(x1))))) → 0#(4(2(x1))) (139)
2#(4(2(3(1(x1))))) → 2#(3(3(1(x1)))) (140)
2#(4(2(3(1(x1))))) → 2#(2(3(3(1(x1))))) (141)
2#(5(2(0(1(x1))))) → 2#(x1) (142)
2#(5(2(0(1(x1))))) → 2#(4(1(5(2(x1))))) (143)
2#(5(2(0(1(x1))))) → 0#(2(4(1(5(2(x1)))))) (144)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.