Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/138468)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
0(1(1(1(2(2(0(1(0(x1))))))))) → 2(0(0(0(2(2(1(0(0(0(x1)))))))))) (101)
0(1(0(2(1(2(1(1(1(0(x1)))))))))) → 2(2(0(0(2(0(2(1(2(2(1(x1))))))))))) (102)
1(0(2(0(1(0(1(1(1(1(x1)))))))))) → 0(2(1(2(2(1(2(2(2(0(1(x1))))))))))) (103)
0(2(1(0(1(0(1(2(2(1(1(0(x1)))))))))))) → 0(2(1(2(2(2(2(0(0(2(2(0(0(x1))))))))))))) (104)
0(2(1(2(0(0(1(1(1(1(0(1(x1)))))))))))) → 2(1(2(0(2(2(2(1(2(0(2(2(1(x1))))))))))))) (105)
1(1(0(2(1(1(1(0(0(1(1(0(0(x1))))))))))))) → 1(0(2(2(2(2(1(2(2(0(2(2(0(1(x1)))))))))))))) (106)
1(1(1(1(0(0(1(0(1(1(1(1(0(x1))))))))))))) → 1(2(2(1(2(0(0(0(2(0(0(1(2(0(x1)))))))))))))) (107)
0(1(2(1(1(1(1(1(1(0(1(2(0(x1))))))))))))) → 0(0(0(2(1(1(2(2(0(2(2(1(2(2(x1)))))))))))))) (108)
0(1(1(0(0(0(0(2(0(1(0(1(1(x1))))))))))))) → 0(2(0(2(2(2(0(0(2(1(0(0(0(0(x1)))))))))))))) (109)
1(1(1(2(0(0(1(1(1(1(2(1(1(x1))))))))))))) → 0(2(2(1(2(2(2(2(1(2(0(2(0(1(x1)))))))))))))) (110)
0(1(1(0(0(1(1(0(1(0(1(0(2(0(x1)))))))))))))) → 0(0(0(2(2(0(2(1(0(0(2(2(0(1(2(x1))))))))))))))) (111)
0(2(2(2(2(0(1(2(0(0(1(0(2(1(x1)))))))))))))) → 0(2(2(2(2(2(2(0(2(2(0(2(0(2(1(x1))))))))))))))) (112)
0(0(0(1(1(0(1(1(0(1(0(1(2(1(x1)))))))))))))) → 0(1(1(1(0(2(2(2(2(1(2(0(2(2(1(x1))))))))))))))) (113)
1(0(0(1(1(1(2(1(1(1(0(0(1(0(0(x1))))))))))))))) → 0(1(1(0(0(0(2(2(0(1(1(2(2(2(1(0(x1)))))))))))))))) (114)
1(0(1(2(1(2(1(0(0(0(1(2(1(0(1(x1))))))))))))))) → 0(1(2(2(2(1(2(2(2(2(1(0(0(1(2(1(x1)))))))))))))))) (115)
0(1(0(0(0(1(0(0(0(0(1(0(2(1(1(x1))))))))))))))) → 0(2(0(2(0(0(2(0(2(1(2(0(2(2(2(2(x1)))))))))))))))) (116)
1(0(1(1(2(0(0(1(0(1(1(1(1(1(2(x1))))))))))))))) → 0(1(0(2(2(0(2(2(0(2(0(2(2(2(2(2(2(x1))))))))))))))))) (117)
2(2(2(1(2(0(0(1(2(0(0(0(2(0(1(0(x1)))))))))))))))) → 2(2(1(0(0(0(0(0(2(1(0(2(2(1(2(0(x1)))))))))))))))) (118)
0(2(0(0(2(2(0(0(0(0(0(1(1(1(1(0(x1)))))))))))))))) → 2(0(2(2(1(2(1(1(0(2(0(2(2(1(2(2(1(x1))))))))))))))))) (119)
1(0(1(2(0(1(2(1(1(1(0(0(2(1(0(1(x1)))))))))))))))) → 2(1(2(0(2(1(2(2(2(0(1(0(2(1(2(2(1(x1))))))))))))))))) (120)
0(1(0(1(0(0(1(0(2(0(2(1(1(1(2(1(x1)))))))))))))))) → 0(1(2(0(1(2(2(1(2(2(2(1(0(0(0(2(1(x1))))))))))))))))) (121)
1(2(0(1(0(1(1(1(1(1(1(1(0(0(1(1(0(x1))))))))))))))))) → 2(2(0(0(1(0(2(0(2(0(2(2(0(1(0(1(0(2(x1)))))))))))))))))) (122)
1(0(0(1(1(2(1(1(2(0(0(0(2(0(1(1(0(x1))))))))))))))))) → 1(0(0(2(0(1(0(0(1(2(2(2(2(0(0(2(2(2(x1)))))))))))))))))) (123)
2(0(2(1(2(1(2(2(1(0(0(0(0(1(1(0(1(x1))))))))))))))))) → 2(2(2(0(0(0(2(2(0(2(2(1(0(2(2(2(0(1(x1)))))))))))))))))) (124)
1(1(2(0(1(1(1(0(1(0(0(1(2(1(0(1(1(x1))))))))))))))))) → 1(2(0(1(1(2(1(2(0(2(0(0(2(0(2(0(0(0(x1)))))))))))))))))) (125)
1(0(1(0(0(1(1(1(1(1(2(2(0(0(0(1(2(x1))))))))))))))))) → 1(0(2(0(1(0(2(2(1(0(2(0(2(0(0(1(0(2(x1)))))))))))))))))) (126)
0(0(0(0(1(2(1(0(0(2(1(1(0(0(1(2(2(x1))))))))))))))))) → 2(0(2(2(1(1(2(1(2(2(2(1(1(0(2(2(2(2(x1)))))))))))))))))) (127)
2(0(0(1(2(2(0(1(1(0(1(1(2(1(0(2(1(0(x1)))))))))))))))))) → 2(1(0(0(0(2(2(2(0(2(0(2(0(2(2(2(1(0(0(x1))))))))))))))))))) (128)
0(2(2(0(0(2(2(0(0(2(0(0(2(0(1(0(2(0(x1)))))))))))))))))) → 0(2(2(0(0(0(2(0(0(0(2(2(2(0(1(0(2(0(x1)))))))))))))))))) (129)
1(0(2(2(0(1(0(1(1(0(1(2(2(1(0(0(0(1(x1)))))))))))))))))) → 2(0(1(1(2(0(2(2(2(2(0(0(2(2(2(2(0(2(1(x1))))))))))))))))))) (130)
0(0(1(2(2(0(1(1(1(1(0(0(0(2(2(0(0(1(x1)))))))))))))))))) → 2(0(2(2(0(2(1(0(2(2(2(1(2(2(2(0(2(0(0(x1))))))))))))))))))) (131)
1(1(2(1(1(2(1(1(2(1(1(0(2(1(0(0(1(1(x1)))))))))))))))))) → 2(0(2(2(0(2(1(2(0(2(0(1(0(1(0(1(2(0(1(x1))))))))))))))))))) (132)
0(0(1(1(2(0(0(2(1(0(1(0(0(2(0(1(1(2(x1)))))))))))))))))) → 0(2(2(1(2(0(1(2(2(2(1(2(1(0(2(0(1(1(2(x1))))))))))))))))))) (133)
1(0(1(2(2(2(2(0(1(2(0(0(1(1(1(1(1(2(x1)))))))))))))))))) → 1(0(1(1(1(2(1(2(2(1(0(2(2(0(2(0(2(2(2(x1))))))))))))))))))) (134)
0(0(2(1(0(0(1(1(2(0(1(0(1(2(1(0(1(0(1(x1))))))))))))))))))) → 0(2(1(0(2(0(2(0(2(0(0(2(1(0(2(2(1(1(0(0(1(x1))))))))))))))))))))) (135)
0(2(1(1(1(2(1(2(1(0(1(0(1(1(2(2(1(0(1(x1))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(2(2(0(2(1(2(0(0(1(1(1(x1)))))))))))))))))))) (136)
0(2(1(1(2(0(0(1(2(1(1(0(1(0(1(0(0(1(1(x1))))))))))))))))))) → 0(0(1(0(2(0(1(0(2(0(1(0(2(2(2(2(1(2(1(1(x1)))))))))))))))))))) (137)
0(0(1(2(1(2(2(2(0(1(1(2(1(2(1(1(1(1(1(x1))))))))))))))))))) → 0(1(2(2(0(2(0(2(0(0(2(0(0(1(0(2(2(0(1(1(x1)))))))))))))))))))) (138)
1(2(0(1(1(1(1(0(2(0(2(0(1(1(0(1(2(1(1(x1))))))))))))))))))) → 2(0(0(0(0(2(2(2(2(1(0(1(0(2(2(2(2(2(2(2(0(x1))))))))))))))))))))) (139)
1(0(1(2(1(1(0(1(0(1(2(1(2(0(0(0(1(2(1(x1))))))))))))))))))) → 1(1(2(0(2(2(2(1(2(0(0(2(2(1(2(2(1(2(1(1(2(x1))))))))))))))))))))) (140)
2(0(0(0(1(0(1(1(0(0(1(1(2(1(1(1(1(2(2(x1))))))))))))))))))) → 2(2(1(2(0(2(2(1(0(0(2(0(2(0(2(2(2(0(2(1(x1)))))))))))))))))))) (141)
0(1(1(0(1(2(0(0(2(0(1(0(0(1(1(1(1(1(0(0(x1)))))))))))))))))))) → 2(2(0(2(0(2(0(0(0(1(2(0(2(1(2(2(2(2(2(2(2(1(x1)))))))))))))))))))))) (142)
0(1(2(1(2(2(2(0(2(1(0(2(1(1(0(1(2(2(0(1(x1)))))))))))))))))))) → 2(2(2(1(0(0(2(1(0(2(2(1(2(2(2(1(0(2(1(0(1(x1))))))))))))))))))))) (143)
1(1(0(0(1(0(1(1(1(0(2(0(0(1(0(1(0(0(1(1(x1)))))))))))))))))))) → 1(1(2(2(2(2(2(1(2(0(1(2(0(0(1(2(2(2(0(2(0(x1))))))))))))))))))))) (144)
2(2(0(0(0(1(0(1(1(2(0(2(0(0(1(0(2(1(1(1(x1)))))))))))))))))))) → 2(2(0(0(2(0(2(0(2(0(0(2(2(1(1(0(0(0(2(2(2(x1))))))))))))))))))))) (145)
0(2(1(1(2(2(0(0(1(2(1(1(0(1(2(0(1(0(1(0(0(x1))))))))))))))))))))) → 2(0(1(2(2(1(2(2(2(2(2(2(2(0(2(0(2(2(2(0(2(0(2(0(x1)))))))))))))))))))))))) (146)
1(0(2(0(0(0(2(2(0(2(0(2(0(2(1(1(0(0(2(1(0(x1))))))))))))))))))))) → 1(0(0(1(0(2(2(0(0(2(2(2(1(0(0(0(2(0(2(1(0(x1))))))))))))))))))))) (147)
1(0(0(1(1(1(1(0(1(2(0(2(1(1(1(0(1(1(1(2(0(x1))))))))))))))))))))) → 1(0(0(2(1(0(0(2(1(1(2(0(2(0(0(1(0(2(2(0(1(2(x1)))))))))))))))))))))) (148)
0(1(0(0(1(2(1(1(1(0(1(2(1(2(1(1(0(1(0(0(1(x1))))))))))))))))))))) → 2(0(0(0(2(0(1(0(1(1(2(1(2(1(0(2(0(2(0(1(0(0(x1)))))))))))))))))))))) (149)
0(0(1(2(1(1(2(0(1(0(0(2(1(1(1(0(1(1(0(0(1(x1))))))))))))))))))))) → 0(0(0(1(1(1(2(0(0(2(1(2(0(0(2(1(0(2(0(1(0(0(x1)))))))))))))))))))))) (150)
0(2(1(0(1(0(1(1(1(0(1(1(1(2(0(0(0(0(1(1(1(x1))))))))))))))))))))) → 1(2(0(2(2(0(1(1(0(1(2(1(2(0(0(1(2(0(0(0(2(2(x1)))))))))))))))))))))) (151)
0(0(2(1(2(1(1(0(2(1(1(1(0(1(2(2(2(1(1(0(0(0(x1)))))))))))))))))))))) → 1(1(0(0(0(2(2(0(2(1(0(0(2(1(0(0(2(2(1(2(0(2(1(x1))))))))))))))))))))))) (152)
0(2(1(2(1(1(1(2(0(1(1(0(1(1(0(0(0(2(1(1(0(0(x1)))))))))))))))))))))) → 0(1(2(2(2(2(1(0(2(2(0(0(1(2(0(2(2(2(0(1(1(2(0(x1))))))))))))))))))))))) (153)
1(1(1(1(2(0(1(0(1(1(1(1(0(1(2(1(1(0(1(1(1(0(x1)))))))))))))))))))))) → 2(2(1(0(0(2(1(0(0(2(2(2(2(0(0(2(2(2(2(2(1(2(0(2(1(x1))))))))))))))))))))))))) (154)
1(1(0(2(1(1(1(0(2(1(1(2(2(2(1(1(0(2(1(1(2(0(x1)))))))))))))))))))))) → 2(1(0(0(0(1(0(1(2(2(1(0(0(1(0(2(0(2(0(2(2(1(0(x1))))))))))))))))))))))) (155)
1(1(1(0(1(0(0(2(0(1(1(1(0(1(1(1(0(1(0(2(2(0(x1)))))))))))))))))))))) → 2(0(2(0(0(2(2(0(0(1(0(1(1(0(2(2(0(0(2(2(2(1(1(x1))))))))))))))))))))))) (156)
1(1(2(1(1(1(1(1(0(2(0(0(0(1(2(1(1(2(0(2(2(0(x1)))))))))))))))))))))) → 1(2(0(2(1(0(2(2(1(0(1(0(2(0(2(2(2(2(2(2(2(0(0(x1))))))))))))))))))))))) (157)
1(1(1(0(1(0(1(1(0(1(0(1(0(0(0(2(0(1(1(2(1(0(0(x1))))))))))))))))))))))) → 0(2(0(2(2(1(2(0(2(1(0(2(2(2(0(0(0(1(2(2(2(0(2(1(x1)))))))))))))))))))))))) (158)
0(2(1(1(0(1(1(0(2(2(1(1(0(1(2(2(0(0(1(1(2(0(0(x1))))))))))))))))))))))) → 2(1(2(0(0(2(0(2(2(2(2(2(1(0(0(2(2(1(2(0(0(2(0(2(0(x1))))))))))))))))))))))))) (159)
2(0(2(0(1(0(0(1(1(1(1(2(2(0(0(1(0(0(0(1(0(0(1(x1))))))))))))))))))))))) → 2(2(1(0(1(1(2(2(1(0(2(2(2(1(2(1(0(2(2(2(1(0(2(2(x1)))))))))))))))))))))))) (160)
0(0(0(1(0(1(1(1(0(1(2(0(1(1(2(1(0(1(2(1(1(1(1(x1))))))))))))))))))))))) → 0(2(0(0(2(1(0(1(0(0(0(1(0(2(2(0(0(1(1(2(1(1(2(1(x1)))))))))))))))))))))))) (161)
1(0(1(1(1(0(1(2(1(2(1(0(2(0(1(1(0(2(0(2(2(2(1(x1))))))))))))))))))))))) → 2(0(0(2(0(0(0(0(0(2(2(2(2(2(2(0(1(2(1(0(2(1(0(0(x1)))))))))))))))))))))))) (162)
0(2(1(1(1(1(1(1(1(2(2(2(2(1(1(1(2(2(2(1(0(0(1(0(x1)))))))))))))))))))))))) → 0(2(2(0(2(0(2(2(0(0(1(2(1(0(1(0(2(2(1(1(1(2(0(2(1(x1))))))))))))))))))))))))) (163)
1(0(1(0(1(0(1(1(0(0(2(1(1(1(2(0(0(1(2(1(1(1(0(1(x1)))))))))))))))))))))))) → 0(0(2(2(0(0(2(0(2(0(2(2(2(2(0(0(1(2(1(0(0(2(2(0(1(2(2(x1))))))))))))))))))))))))))) (164)
2(0(2(0(0(0(1(2(2(0(1(2(1(2(2(2(2(0(0(0(2(0(1(1(x1)))))))))))))))))))))))) → 2(0(2(0(1(0(1(2(1(0(0(0(2(2(2(2(2(0(0(0(2(2(1(1(x1)))))))))))))))))))))))) (165)
0(1(2(2(2(2(1(0(1(0(1(0(2(0(0(1(2(2(2(2(0(1(2(1(x1)))))))))))))))))))))))) → 0(0(2(2(1(1(1(0(2(2(1(1(2(0(0(2(0(2(2(2(1(0(2(1(x1)))))))))))))))))))))))) (166)
0(0(1(1(2(1(0(2(2(2(1(1(1(0(0(1(1(0(2(0(1(2(0(1(0(x1))))))))))))))))))))))))) → 0(1(2(2(1(1(1(2(2(1(2(0(2(0(0(1(2(0(0(0(0(2(2(2(1(0(x1)))))))))))))))))))))))))) (167)
0(1(1(0(2(1(0(0(0(2(1(2(1(2(1(0(0(1(0(2(1(2(0(1(0(x1))))))))))))))))))))))))) → 2(2(2(0(0(2(2(2(2(0(0(0(0(0(0(0(2(2(1(2(2(1(1(2(2(1(x1)))))))))))))))))))))))))) (168)
0(0(1(1(2(2(2(0(0(1(0(0(2(0(2(0(2(0(2(2(0(0(0(2(0(x1))))))))))))))))))))))))) → 0(0(0(0(0(2(2(1(0(2(0(2(0(0(2(2(2(2(1(0(1(0(0(2(0(x1))))))))))))))))))))))))) (169)
1(2(0(1(2(0(1(0(1(0(2(2(0(2(1(2(0(1(0(0(0(1(0(2(0(x1))))))))))))))))))))))))) → 1(2(1(0(2(0(2(2(2(1(2(0(0(2(2(2(2(1(0(2(0(1(2(0(2(2(x1)))))))))))))))))))))))))) (170)
0(1(2(1(2(1(1(0(1(2(1(1(1(1(1(0(1(1(0(2(1(0(2(2(0(x1))))))))))))))))))))))))) → 2(2(1(0(2(0(0(2(2(0(1(1(1(2(0(2(2(0(1(1(2(0(0(0(1(1(x1)))))))))))))))))))))))))) (171)
0(2(2(0(0(2(0(0(2(0(0(1(1(0(0(2(1(1(0(0(1(0(1(0(1(x1))))))))))))))))))))))))) → 1(1(0(0(0(0(1(2(1(2(2(1(2(2(0(2(2(0(2(2(1(0(0(2(0(1(x1)))))))))))))))))))))))))) (172)
1(0(0(2(1(2(2(1(2(1(0(1(0(1(1(0(0(1(0(0(1(1(0(2(1(x1))))))))))))))))))))))))) → 2(0(2(0(2(2(1(2(1(0(0(0(2(0(2(0(0(2(2(0(1(2(0(1(1(2(x1)))))))))))))))))))))))))) (173)
1(0(2(0(1(1(0(2(1(1(0(1(0(2(0(2(0(0(1(0(1(0(0(1(2(x1))))))))))))))))))))))))) → 1(0(2(1(1(0(2(2(1(2(2(0(2(2(1(2(2(0(1(2(0(2(1(2(0(0(x1)))))))))))))))))))))))))) (174)
0(0(1(2(0(1(2(0(1(2(1(1(0(2(0(0(2(1(0(1(2(0(1(1(1(0(x1)))))))))))))))))))))))))) → 2(1(1(0(1(2(2(0(1(0(1(2(2(1(0(2(2(2(2(1(2(2(1(1(1(2(1(x1))))))))))))))))))))))))))) (175)
1(1(0(1(0(1(1(0(1(1(1(2(1(1(1(0(2(2(0(1(2(1(1(0(2(0(x1)))))))))))))))))))))))))) → 2(1(2(1(1(0(1(1(0(0(2(2(0(0(0(0(2(1(1(1(1(0(2(2(0(0(0(x1))))))))))))))))))))))))))) (176)
1(1(1(2(0(1(2(2(1(0(2(0(0(1(1(1(0(0(1(0(0(1(2(0(1(1(x1)))))))))))))))))))))))))) → 0(2(1(0(0(1(0(0(0(2(2(1(2(2(1(0(0(1(0(1(2(1(2(2(1(2(0(x1))))))))))))))))))))))))))) (177)
1(2(1(1(2(1(2(1(2(2(1(1(0(2(1(0(1(1(1(2(2(1(1(2(2(2(x1)))))))))))))))))))))))))) → 0(0(2(1(2(2(2(0(0(0(0(0(0(0(2(1(2(2(0(2(1(2(2(0(0(2(2(x1))))))))))))))))))))))))))) (178)
1(1(1(1(1(0(1(1(1(0(1(1(0(0(2(1(0(0(2(2(0(1(2(1(1(0(0(x1))))))))))))))))))))))))))) → 2(2(0(2(2(0(1(0(1(2(1(2(1(1(1(1(2(0(2(2(0(2(2(0(0(0(2(1(x1)))))))))))))))))))))))))))) (179)
0(0(2(0(1(1(0(1(1(0(1(0(1(1(2(0(1(1(1(1(1(1(1(1(1(1(0(x1))))))))))))))))))))))))))) → 0(2(1(0(2(2(0(0(1(1(2(0(1(2(0(2(0(0(1(0(1(2(0(0(0(1(2(0(0(x1))))))))))))))))))))))))))))) (180)
0(1(0(2(1(1(2(1(1(1(2(0(0(0(1(0(2(0(2(0(1(2(1(2(1(1(0(x1))))))))))))))))))))))))))) → 1(2(0(2(0(1(0(0(0(2(0(2(2(2(0(0(1(0(2(0(0(1(0(0(2(2(1(1(x1)))))))))))))))))))))))))))) (181)
1(0(1(2(1(2(1(2(2(0(2(0(1(1(2(0(2(0(0(1(0(0(1(1(1(0(1(x1))))))))))))))))))))))))))) → 1(0(2(2(2(2(2(1(2(2(2(2(1(1(0(2(2(0(0(0(1(1(2(1(0(2(0(1(x1)))))))))))))))))))))))))))) (182)
0(1(2(0(1(0(1(0(0(1(1(0(1(1(0(0(1(1(2(0(0(1(2(1(1(0(1(x1))))))))))))))))))))))))))) → 0(1(2(0(2(2(1(2(2(2(1(0(2(1(1(0(1(2(2(1(0(1(0(1(2(2(1(1(2(x1))))))))))))))))))))))))))))) (183)
0(1(1(1(0(1(0(2(0(1(0(0(0(1(1(2(0(2(0(1(0(1(0(0(2(0(1(x1))))))))))))))))))))))))))) → 1(1(2(1(2(0(2(1(2(1(2(0(0(2(2(2(1(2(1(1(2(0(2(1(0(0(2(2(x1)))))))))))))))))))))))))))) (184)
0(1(0(0(2(2(2(2(1(0(1(1(2(0(2(0(2(0(1(0(0(2(0(0(0(1(1(x1))))))))))))))))))))))))))) → 0(2(2(2(0(2(0(2(2(0(2(1(2(2(2(1(2(1(2(2(1(0(1(0(2(2(1(2(x1)))))))))))))))))))))))))))) (185)
1(1(1(1(2(2(0(0(1(0(2(1(1(2(1(0(1(2(0(1(1(0(2(2(1(1(1(x1))))))))))))))))))))))))))) → 2(1(2(1(1(0(2(2(1(0(2(1(1(0(1(2(2(2(1(1(2(2(1(2(0(0(2(0(x1)))))))))))))))))))))))))))) (186)
0(1(0(1(0(1(1(0(1(0(2(0(0(0(2(1(0(2(1(2(0(1(0(0(0(1(2(x1))))))))))))))))))))))))))) → 0(2(0(2(0(1(1(2(0(2(0(0(1(2(2(1(2(2(1(2(2(0(2(1(1(0(1(2(x1)))))))))))))))))))))))))))) (187)
2(0(0(0(2(0(1(2(1(2(1(2(1(2(0(0(1(2(2(0(2(1(1(1(1(1(2(x1))))))))))))))))))))))))))) → 2(1(1(0(2(1(0(1(2(2(2(1(2(2(2(1(0(0(2(1(2(2(1(2(2(2(2(0(0(x1))))))))))))))))))))))))))))) (188)
0(1(1(0(2(1(2(1(2(2(1(1(1(1(1(1(2(1(1(1(2(2(0(2(2(1(2(x1))))))))))))))))))))))))))) → 2(0(0(2(2(1(2(0(0(2(1(2(1(2(0(0(2(0(0(1(0(0(2(2(0(2(2(2(x1)))))))))))))))))))))))))))) (189)
0(2(1(0(2(1(2(2(0(0(1(2(1(1(1(0(2(1(1(1(1(2(1(2(0(1(1(0(x1)))))))))))))))))))))))))))) → 2(0(1(2(2(2(1(0(2(0(0(2(2(0(0(1(1(0(2(0(2(1(2(2(1(2(2(0(1(x1))))))))))))))))))))))))))))) (190)
1(0(2(2(0(1(0(1(2(1(0(0(0(1(2(0(1(0(0(1(1(1(1(0(1(1(1(0(x1)))))))))))))))))))))))))))) → 1(2(2(0(0(2(2(2(1(2(0(0(2(0(1(1(1(1(1(1(1(1(2(1(2(2(2(1(1(x1))))))))))))))))))))))))))))) (191)
1(0(2(1(1(0(2(0(0(1(0(1(2(1(0(1(2(1(0(1(2(2(1(0(1(1(0(1(x1)))))))))))))))))))))))))))) → 1(2(1(0(0(1(0(0(2(2(2(2(1(2(1(0(2(0(2(2(1(2(2(2(0(0(2(2(2(x1))))))))))))))))))))))))))))) (192)
2(2(0(1(2(1(0(0(1(1(1(1(1(0(1(0(2(2(2(1(1(2(1(2(0(1(1(1(x1)))))))))))))))))))))))))))) → 2(0(0(0(2(1(0(2(1(0(2(2(2(1(0(0(1(2(1(1(0(2(1(1(0(0(2(2(2(x1))))))))))))))))))))))))))))) (193)
2(1(1(2(0(0(0(1(1(0(1(2(1(1(0(1(1(0(0(1(2(0(2(2(2(2(2(2(x1)))))))))))))))))))))))))))) → 2(1(1(2(0(0(2(1(0(1(0(1(0(1(0(2(1(1(0(2(1(0(2(2(1(2(2(2(x1)))))))))))))))))))))))))))) (194)
0(2(1(0(0(1(1(2(1(2(2(0(1(1(0(1(1(1(0(1(2(2(0(1(0(2(0(0(0(x1))))))))))))))))))))))))))))) → 0(0(0(0(0(2(2(0(1(0(0(0(0(2(2(1(2(1(0(0(2(0(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))))))))) (195)
1(1(1(1(1(0(0(2(1(0(1(0(0(1(2(2(2(1(1(2(2(0(0(1(1(0(0(1(0(x1))))))))))))))))))))))))))))) → 0(2(2(2(2(0(0(1(2(0(2(2(0(1(2(0(2(1(2(0(0(1(2(2(1(2(2(0(2(2(x1)))))))))))))))))))))))))))))) (196)
2(0(1(0(0(1(0(1(2(2(0(0(1(1(1(2(1(0(2(0(0(0(2(0(2(0(0(0(1(x1))))))))))))))))))))))))))))) → 2(0(2(2(0(2(1(2(2(0(1(2(2(2(0(2(1(2(1(2(0(0(0(1(2(2(0(2(2(2(x1)))))))))))))))))))))))))))))) (197)
0(1(1(0(1(0(1(2(2(2(1(0(1(1(2(0(2(1(0(2(1(1(2(0(2(1(1(2(2(x1))))))))))))))))))))))))))))) → 0(0(1(1(1(1(1(2(2(2(0(0(2(2(1(1(1(0(2(2(2(1(2(0(0(1(1(2(1(x1))))))))))))))))))))))))))))) (198)
1(2(2(1(0(1(0(0(0(0(2(2(2(0(0(1(1(0(2(0(1(1(2(2(0(0(1(2(2(0(x1)))))))))))))))))))))))))))))) → 1(0(2(2(0(1(1(0(2(2(1(0(0(0(0(0(2(0(2(2(1(2(0(2(0(1(1(1(2(0(x1)))))))))))))))))))))))))))))) (199)
0(0(0(1(1(2(0(0(2(0(0(0(2(1(0(0(1(1(0(2(0(1(1(1(1(1(0(2(0(1(x1)))))))))))))))))))))))))))))) → 0(0(0(0(0(0(1(0(2(0(1(0(0(0(1(1(1(1(1(2(0(2(2(1(1(0(2(0(1(1(x1)))))))))))))))))))))))))))))) (200)

1.1 Closure Under Flat Contexts

Using the flat contexts

{0(☐), 1(☐), 2(☐)}

We obtain the transformed TRS

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

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

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

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

1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[10(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
[00(x1)] = 1 · x1 + 13
[22(x1)] = 1 · x1
[21(x1)] = 1 · x1 + 14
[11(x1)] = 1 · x1 + 33
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1 + 8
all of the following rules can be deleted.
10(02(20(00(00(02(22(20(02(20(02(20(02(21(11(10(00(02(21(10(00(x1))))))))))))))))))))) → 10(00(01(10(02(22(20(00(02(22(22(21(10(00(00(02(20(02(21(10(00(x1))))))))))))))))))))) (414)
10(02(20(00(00(02(22(20(02(20(02(20(02(21(11(10(00(02(21(10(02(x1))))))))))))))))))))) → 10(00(01(10(02(22(20(00(02(22(22(21(10(00(00(02(20(02(21(10(02(x1))))))))))))))))))))) (415)
10(02(20(00(00(02(22(20(02(20(02(20(02(21(11(10(00(02(21(10(01(x1))))))))))))))))))))) → 10(00(01(10(02(22(20(00(02(22(22(21(10(00(00(02(20(02(21(10(01(x1))))))))))))))))))))) (416)

1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.