Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/213281)

The rewrite relation of the following TRS is considered.

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

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.