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 matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[2(x1)] = x1 +
0
[1(x1)] = x1 +
33/2
[0(x1)] = x1 +
15/4
all of the following rules can be deleted.
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(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)
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(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)
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(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)
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)

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
2(0(1(0(2(0(0(0(2(1(0(0(2(1(2(2(2(x1))))))))))))))))) → 2(0(2(1(2(2(0(1(2(0(0(0(0(0(1(2(2(x1))))))))))))))))) (101)
2(0(2(0(1(0(2(0(0(2(0(0(2(2(0(0(2(2(0(x1))))))))))))))))))) → 2(0(2(0(1(0(2(2(2(0(0(0(2(0(0(0(2(2(0(x1))))))))))))))))))) (102)
2(0(1(2(0(0(1(1(2(0(2(0(2(0(2(2(0(0(0(2(0(1(x1)))))))))))))))))))))) → 2(0(1(2(0(2(0(0(0(1(2(2(2(0(0(2(2(0(1(0(0(1(x1)))))))))))))))))))))) (103)
2(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))))))))))))))))))))))))) → 2(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))))))))))))))))))))))))) (104)
2(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))))))))))))))))))))))))) → 2(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))))))))))))))))))))))))) (105)
2(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)))))))))))))))))))))))))) → 2(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)))))))))))))))))))))))))) (106)
2(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(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))))))))))))))))))))))))))))) (107)
2(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)))))))))))))))))))))))))))))) → 2(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)))))))))))))))))))))))))))))) (108)
2(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))))))))))))))))))))))))))))))) → 2(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))))))))))))))))))))))))))))))) (109)
2(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))))))))))))))))))))))))))))))) → 2(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))))))))))))))))))))))))))))))) (110)
1(0(1(0(2(0(0(0(2(1(0(0(2(1(2(2(2(x1))))))))))))))))) → 1(0(2(1(2(2(0(1(2(0(0(0(0(0(1(2(2(x1))))))))))))))))) (111)
1(0(2(0(1(0(2(0(0(2(0(0(2(2(0(0(2(2(0(x1))))))))))))))))))) → 1(0(2(0(1(0(2(2(2(0(0(0(2(0(0(0(2(2(0(x1))))))))))))))))))) (112)
1(0(1(2(0(0(1(1(2(0(2(0(2(0(2(2(0(0(0(2(0(1(x1)))))))))))))))))))))) → 1(0(1(2(0(2(0(0(0(1(2(2(2(0(0(2(2(0(1(0(0(1(x1)))))))))))))))))))))) (113)
1(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(1(2(2(0(0(0(2(2(2(2(2(0(0(0(1(2(1(0(1(0(2(0(2(x1))))))))))))))))))))))))) (114)
1(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(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))))))))))))))))))))))))) (115)
1(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)))))))))))))))))))))))))) → 1(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)))))))))))))))))))))))))) (116)
1(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))))))))))))))))))))))))))))) → 1(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))))))))))))))))))))))))))))) (117)
1(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(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)))))))))))))))))))))))))))))) (118)
1(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))))))))))))))))))))))))))))))) → 1(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))))))))))))))))))))))))))))))) (119)
1(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(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))))))))))))))))))))))))))))))) (120)
0(0(1(0(2(0(0(0(2(1(0(0(2(1(2(2(2(x1))))))))))))))))) → 0(0(2(1(2(2(0(1(2(0(0(0(0(0(1(2(2(x1))))))))))))))))) (121)
0(0(2(0(1(0(2(0(0(2(0(0(2(2(0(0(2(2(0(x1))))))))))))))))))) → 0(0(2(0(1(0(2(2(2(0(0(0(2(0(0(0(2(2(0(x1))))))))))))))))))) (122)
0(0(1(2(0(0(1(1(2(0(2(0(2(0(2(2(0(0(0(2(0(1(x1)))))))))))))))))))))) → 0(0(1(2(0(2(0(0(0(1(2(2(2(0(0(2(2(0(1(0(0(1(x1)))))))))))))))))))))) (123)
0(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))))))))))))))))))))))))) → 0(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))))))))))))))))))))))))) (124)
0(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))))))))))))))))))))))))) → 0(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))))))))))))))))))))))))) (125)
0(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(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)))))))))))))))))))))))))) (126)
0(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))))))))))))))))))))))))))))) → 0(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))))))))))))))))))))))))))))) (127)
0(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)))))))))))))))))))))))))))))) → 0(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)))))))))))))))))))))))))))))) (128)
0(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(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))))))))))))))))))))))))))))))) (129)
0(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))))))))))))))))))))))))))))))) → 0(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))))))))))))))))))))))))))))))) (130)

1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

As carrier we take the set {0,1,2}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 3):

[2(x1)] = 3x1 + 0
[1(x1)] = 3x1 + 1
[0(x1)] = 3x1 + 2

We obtain the labeled TRS
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (131)
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (132)
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (133)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (134)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (135)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (136)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (137)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (138)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (139)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (140)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (141)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (142)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (143)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (144)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (145)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (146)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (147)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (148)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (149)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (150)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (151)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (152)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (153)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (154)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (155)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (156)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (157)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (158)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (159)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (160)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (161)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (162)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (163)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (164)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (165)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (166)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (167)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (168)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (169)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (170)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (171)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (172)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (173)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (174)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (175)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (176)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (177)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (178)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (179)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (180)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (181)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (182)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (183)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (184)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (185)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (186)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (187)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (188)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (189)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (190)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (191)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (192)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (193)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (194)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (195)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (196)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (197)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (198)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (199)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (200)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (201)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (202)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (203)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (204)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (205)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (206)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (207)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (208)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (209)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (210)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (211)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (212)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (213)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (214)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (215)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (216)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (217)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (218)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (219)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (220)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[20(x1)] = x1 +
0
[21(x1)] = x1 +
7
[22(x1)] = x1 +
1
[10(x1)] = x1 +
1
[11(x1)] = x1 +
0
[12(x1)] = x1 +
0
[00(x1)] = x1 +
1
[01(x1)] = x1 +
0
[02(x1)] = x1 +
0
all of the following rules can be deleted.
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (131)
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (132)
02(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 02(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (133)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (134)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (135)
12(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 12(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (136)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(22(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(22(x1))))))))))))))))) (137)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(21(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(21(x1))))))))))))))))) (138)
22(01(12(00(22(02(02(00(21(12(02(00(21(10(20(20(20(x1))))))))))))))))) → 22(00(21(10(20(22(01(10(22(02(02(02(02(01(10(20(20(x1))))))))))))))))) (139)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (140)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (141)
02(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 02(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (142)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (143)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (144)
12(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 12(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (145)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(02(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(02(x1))))))))))))))))))) (146)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(01(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(01(x1))))))))))))))))))) (147)
22(00(22(01(12(00(22(02(00(22(02(00(20(22(02(00(20(22(00(x1))))))))))))))))))) → 22(00(22(01(12(00(20(20(22(02(02(00(22(02(02(00(20(22(00(x1))))))))))))))))))) (148)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (149)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (150)
02(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 02(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (151)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (152)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (153)
12(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 12(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (154)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(12(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(12(x1)))))))))))))))))))))) (155)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(11(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(11(x1)))))))))))))))))))))) (156)
22(01(10(22(02(01(11(10(22(00(22(00(22(00(20(22(02(02(00(22(01(10(x1)))))))))))))))))))))) → 22(01(10(22(00(22(02(02(01(10(20(20(22(02(00(20(22(01(12(02(01(10(x1)))))))))))))))))))))) (157)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (158)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (159)
01(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 01(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (160)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (161)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (162)
11(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 11(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (163)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(22(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(22(x1))))))))))))))))))))))))) (164)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(21(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(21(x1))))))))))))))))))))))))) (165)
21(11(12(00(22(02(02(00(20(20(20(21(10(21(12(00(20(21(12(02(02(00(22(00(20(x1))))))))))))))))))))))))) → 21(11(10(20(22(02(02(00(20(20(20(20(22(02(02(01(10(21(12(01(12(00(22(00(20(x1))))))))))))))))))))))))) (166)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (167)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (168)
01(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 01(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (169)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (170)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (171)
11(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 11(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (172)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(02(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(02(x1))))))))))))))))))))))))) (173)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(01(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(01(x1))))))))))))))))))))))))) (174)
21(10(21(12(00(20(20(20(21(12(02(00(22(01(12(01(12(01(10(20(20(20(21(12(00(x1))))))))))))))))))))))))) → 21(10(22(01(10(20(20(22(00(22(02(00(21(11(10(20(22(01(11(11(10(20(22(02(00(x1))))))))))))))))))))))))) (175)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (176)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (177)
02(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 02(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (178)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (179)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (180)
12(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 12(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (181)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(02(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(02(x1)))))))))))))))))))))))))) (182)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(01(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(01(x1)))))))))))))))))))))))))) (183)
22(00(22(02(02(00(20(22(00(22(00(22(00(22(02(01(12(02(00(20(20(21(11(12(02(00(x1)))))))))))))))))))))))))) → 22(00(22(02(01(12(01(10(20(20(20(22(02(00(22(00(22(01(10(20(22(02(02(02(02(00(x1)))))))))))))))))))))))))) (184)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (185)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (186)
00(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 00(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (187)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (188)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (189)
10(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 10(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (190)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(22(x1))))))))))))))))))))))))))))) (191)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(21(x1))))))))))))))))))))))))))))) (192)
20(20(20(20(20(20(22(00(21(12(02(01(11(12(01(11(10(21(12(01(11(12(02(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) → 20(20(20(21(10(20(22(01(10(22(01(11(10(22(01(12(01(12(01(12(01(10(22(02(00(21(11(10(20(x1))))))))))))))))))))))))))))) (193)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (194)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (195)
00(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 01(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (196)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (197)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (198)
10(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 11(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (199)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(02(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(02(x1)))))))))))))))))))))))))))))) (200)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(01(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(01(x1)))))))))))))))))))))))))))))) (201)
20(20(21(11(10(22(00(21(11(10(22(01(10(22(00(21(11(12(01(10(20(20(21(12(01(12(01(11(12(00(x1)))))))))))))))))))))))))))))) → 21(10(21(11(12(02(00(21(10(20(20(22(01(11(11(10(20(22(02(00(20(20(21(11(11(11(11(12(02(00(x1)))))))))))))))))))))))))))))) (202)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (203)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (204)
02(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 02(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (205)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (206)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (207)
12(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 12(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (208)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(12(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(12(x1))))))))))))))))))))))))))))))) (209)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(11(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(11(x1))))))))))))))))))))))))))))))) (210)
22(00(20(21(12(02(00(20(21(11(12(00(22(01(11(12(02(00(20(20(22(02(02(02(01(12(01(10(20(21(10(x1))))))))))))))))))))))))))))))) → 22(00(21(11(11(12(00(22(00(21(10(20(22(00(22(02(02(02(02(01(10(20(22(01(11(12(00(20(22(01(10(x1))))))))))))))))))))))))))))))) (211)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (212)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (213)
01(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 01(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (214)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (215)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (216)
11(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 11(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (217)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(02(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(02(x1))))))))))))))))))))))))))))))) (218)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(01(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(01(x1))))))))))))))))))))))))))))))) (219)
21(12(00(22(01(11(11(11(11(12(00(22(01(11(12(02(01(10(22(02(02(00(22(02(00(21(11(12(02(02(00(x1))))))))))))))))))))))))))))))) → 21(11(12(00(22(01(11(10(20(22(00(21(11(11(11(11(12(02(02(01(12(00(22(01(12(02(02(02(02(02(00(x1))))))))))))))))))))))))))))))) (220)

1.1.1.1.1 R is empty

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