Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/211857)

The rewrite relation of the following TRS is considered.

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

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#(0(1(x1))) → 0#(x1) (47)
0#(5(1(x1))) → 0#(4(5(1(x1)))) (48)
0#(5(1(x1))) → 0#(3(1(5(x1)))) (49)
0#(0(1(x1))) → 0#(0(2(2(1(2(x1)))))) (50)
0#(1(1(x1))) → 0#(3(1(2(4(x1))))) (51)
0#(0(1(x1))) → 0#(1(2(x1))) (52)
5#(0(1(x1))) → 0#(2(1(2(4(x1))))) (53)
5#(0(1(x1))) → 5#(0(2(1(2(4(x1)))))) (54)
5#(0(1(x1))) → 5#(1(2(3(0(4(x1)))))) (55)
0#(0(1(x1))) → 0#(x1) (47)
5#(3(1(5(x1)))) → 5#(3(1(2(5(x1))))) (56)
0#(5(3(4(1(x1))))) → 0#(3(5(4(5(x1))))) (57)
0#(1(1(x1))) → 0#(3(1(1(x1)))) (58)
0#(0(1(x1))) → 0#(2(0(x1))) (59)
0#(0(1(x1))) → 0#(x1) (47)
0#(0(1(x1))) → 0#(1(2(0(x1)))) (60)
0#(1(1(x1))) → 0#(4(4(x1))) (61)
0#(5(1(x1))) → 0#(3(1(5(2(x1))))) (62)
5#(0(1(x1))) → 0#(4(x1)) (63)
5#(0(1(x1))) → 5#(1(2(4(0(x1))))) (64)
0#(0(2(1(x1)))) → 0#(2(0(1(x1)))) (65)
0#(5(3(4(1(x1))))) → 5#(x1) (66)
0#(5(1(x1))) → 0#(2(3(1(5(x1))))) (67)
0#(0(1(x1))) → 0#(4(x1)) (68)
0#(0(1(x1))) → 0#(1(3(0(4(x1))))) (69)
0#(0(5(1(5(x1))))) → 0#(x1) (70)
5#(4(2(1(1(x1))))) → 5#(4(1(2(1(2(x1)))))) (71)
0#(0(5(1(5(x1))))) → 5#(0(0(x1))) (72)
0#(5(1(x1))) → 5#(2(x1)) (73)
0#(0(1(x1))) → 0#(3(0(3(1(x1))))) (74)
0#(0(1(x1))) → 0#(x1) (47)
0#(1(1(x1))) → 0#(x1) (75)
0#(0(1(x1))) → 0#(1(2(4(2(0(x1)))))) (76)
0#(1(1(x1))) → 0#(2(1(x1))) (77)
0#(1(1(x1))) → 0#(2(1(1(x1)))) (78)
0#(0(1(x1))) → 0#(3(0(1(2(x1))))) (79)
0#(1(1(1(x1)))) → 0#(x1) (80)
0#(0(5(1(5(x1))))) → 0#(0(x1)) (81)
0#(1(1(x1))) → 0#(x1) (75)
0#(0(1(x1))) → 0#(1(3(0(2(x1))))) (82)
0#(5(1(x1))) → 0#(3(1(2(5(2(x1)))))) (83)
5#(4(0(1(x1)))) → 5#(0(4(x1))) (84)
0#(5(1(x1))) → 5#(2(x1)) (73)
0#(5(1(x1))) → 5#(x1) (85)
0#(0(1(x1))) → 0#(4(x1)) (68)
0#(0(1(x1))) → 0#(x1) (47)
0#(0(1(x1))) → 0#(4(0(4(1(x1))))) (86)
0#(0(1(x1))) → 0#(2(0(1(2(x1))))) (87)
5#(0(1(x1))) → 0#(x1) (88)
0#(0(1(x1))) → 0#(3(0(4(x1)))) (89)
0#(0(5(1(5(x1))))) → 5#(5(0(0(x1)))) (90)
0#(0(1(5(x1)))) → 0#(4(1(0(5(x1))))) (91)
0#(5(4(0(1(x1))))) → 0#(4(5(x1))) (92)
0#(0(1(x1))) → 0#(4(0(x1))) (93)
0#(5(3(0(1(x1))))) → 0#(4(x1)) (94)
0#(1(1(x1))) → 0#(4(2(1(2(x1))))) (95)
0#(0(1(5(x1)))) → 0#(5(x1)) (96)
0#(0(1(x1))) → 0#(x1) (47)
5#(3(2(1(x1)))) → 5#(2(x1)) (97)
0#(5(4(0(1(x1))))) → 5#(x1) (98)
0#(0(1(x1))) → 0#(0(x1)) (99)
0#(0(2(1(x1)))) → 0#(1(x1)) (100)
5#(0(1(1(x1)))) → 0#(x1) (101)
0#(5(4(0(1(x1))))) → 0#(1(3(0(4(5(x1)))))) (102)
5#(3(0(1(x1)))) → 0#(x1) (103)
0#(1(1(x1))) → 0#(4(x1)) (104)
0#(0(1(x1))) → 0#(4(1(x1))) (105)
0#(5(1(x1))) → 5#(x1) (85)
0#(0(1(x1))) → 0#(2(2(1(2(x1))))) (106)
0#(0(1(x1))) → 0#(1(2(x1))) (52)
5#(0(1(1(x1)))) → 5#(1(2(0(x1)))) (107)
0#(5(3(0(1(x1))))) → 0#(5(3(0(4(x1))))) (108)
0#(0(1(x1))) → 0#(3(1(x1))) (109)
0#(0(1(x1))) → 0#(3(1(0(x1)))) (110)
0#(5(3(4(1(x1))))) → 5#(4(5(x1))) (111)
0#(1(0(1(x1)))) → 0#(2(0(1(x1)))) (112)
5#(4(0(1(x1)))) → 0#(4(x1)) (113)
0#(5(3(0(1(x1))))) → 5#(3(0(4(x1)))) (114)
0#(0(1(x1))) → 0#(2(x1)) (115)
0#(0(2(1(x1)))) → 0#(3(0(2(1(x1))))) (116)
5#(3(0(1(x1)))) → 5#(1(2(3(0(x1))))) (117)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.