Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/40976)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

There are 297 ruless (increase limit for explicit display).

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1 + 1
[12(x1)] = 1 · x1 + 1
[20(x1)] = 1 · x1
[02(x1)] = 1 · x1 + 1
[22(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1
[11(x1)] = 1 · x1 + 2
[10(x1)] = 1 · x1
all of the following rules can be deleted.

There are 263 ruless (increase limit for explicit display).

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

There are 229 ruless (increase limit for explicit display).

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.