Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/153288)

The rewrite relation of the following TRS is considered.

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

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
[1(x1)] = x1 +
1
[0(x1)] = x1 +
0
all of the following rules can be deleted.
0(0(0(0(0(0(0(0(0(1(0(1(1(1(0(0(1(1(1(0(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(1(0(0(0(1(1(0(0(1(1(0(0(x1)))))))))))))))))))) (1)
0(0(0(0(0(0(0(1(1(1(1(0(0(1(0(1(0(0(1(0(x1)))))))))))))))))))) → 0(1(0(0(0(0(1(0(1(0(0(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (2)
0(0(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(0(0(x1)))))))))))))))))))) → 0(0(1(0(1(0(1(0(0(1(0(0(0(0(1(0(0(1(0(1(x1)))))))))))))))))))) (3)
0(0(0(0(0(0(1(1(1(0(1(0(0(1(0(1(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(1(0(1(1(0(0(0(1(0(1(0(0(0(1(0(0(x1)))))))))))))))))))) (4)
0(0(0(0(0(1(0(1(1(1(0(1(0(0(0(1(1(1(0(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(1(0(1(0(0(1(0(0(0(1(0(0(1(x1)))))))))))))))))))) (6)
0(0(0(0(1(1(0(0(0(1(0(1(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(0(0(1(0(0(1(0(0(0(0(1(0(1(x1)))))))))))))))))))) (8)
0(0(0(0(1(1(0(1(0(1(0(1(1(0(1(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(0(0(1(1(0(0(1(0(1(1(1(1(0(0(x1)))))))))))))))))))) (10)
0(0(0(0(1(1(0(1(0(1(1(1(1(0(0(0(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(1(0(1(1(0(0(0(1(0(0(0(0(1(0(x1)))))))))))))))))))) (11)
0(0(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(0(1(1(x1)))))))))))))))))))) → 0(1(1(0(0(0(1(0(0(1(0(1(0(0(0(0(0(0(1(0(x1)))))))))))))))))))) (14)
0(0(0(1(0(0(0(1(0(1(0(0(1(1(1(1(0(1(0(0(x1)))))))))))))))))))) → 0(1(1(1(0(1(1(0(0(0(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))))) (15)
0(0(0(1(0(1(0(0(1(0(1(0(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(0(0(0(1(1(0(0(0(0(0(0(1(0(x1)))))))))))))))))))) (16)
0(0(0(1(0(1(1(0(1(1(0(0(0(1(1(0(1(0(0(0(x1)))))))))))))))))))) → 1(0(0(0(1(0(0(1(1(0(0(0(1(0(0(0(1(0(0(1(x1)))))))))))))))))))) (17)
0(0(0(1(1(0(0(0(0(1(0(1(1(1(0(1(1(0(0(0(x1)))))))))))))))))))) → 0(1(0(1(0(1(0(1(0(0(1(1(0(0(1(0(0(0(0(0(x1)))))))))))))))))))) (18)
0(0(0(1(1(0(1(0(1(1(0(1(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) → 0(1(0(0(0(0(1(0(0(1(0(1(0(0(1(0(1(0(0(0(x1)))))))))))))))))))) (20)
0(0(0(1(1(1(0(0(0(0(1(1(0(0(1(0(1(0(0(0(x1)))))))))))))))))))) → 0(1(0(0(1(0(0(0(1(0(1(0(0(1(0(1(0(0(0(0(x1)))))))))))))))))))) (21)
0(0(1(0(0(0(0(1(0(0(1(1(1(0(1(0(1(0(1(0(x1)))))))))))))))))))) → 0(1(0(1(1(0(0(0(0(0(1(0(0(1(0(0(0(1(0(1(x1)))))))))))))))))))) (23)
0(0(1(0(0(0(1(0(0(1(0(1(0(1(1(1(0(0(1(0(x1)))))))))))))))))))) → 0(1(1(0(0(1(0(1(0(1(0(0(0(0(0(1(0(0(0(1(x1)))))))))))))))))))) (24)
0(0(1(0(0(0(1(1(0(0(1(0(0(0(1(1(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(1(0(0(0(0(0(0(0(0(0(0(1(0(0(x1)))))))))))))))))))) (25)
0(0(1(0(0(0(1(1(1(0(0(0(1(1(0(0(1(0(1(0(x1)))))))))))))))))))) → 1(0(0(1(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(0(x1)))))))))))))))))))) (26)
0(0(1(0(1(0(0(0(1(1(0(0(1(1(1(0(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(0(0(0(1(1(0(0(1(1(0(0(0(0(x1)))))))))))))))))))) (27)
0(0(1(0(1(0(0(1(0(1(0(1(0(0(0(0(1(1(1(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(0(1(1(0(0(0(0(0(1(1(1(0(x1)))))))))))))))))))) (29)
0(0(1(0(1(1(0(0(0(1(1(1(1(0(0(0(0(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(x1)))))))))))))))))))) (30)
0(0(1(0(1(1(1(0(0(0(1(1(0(1(0(1(0(0(0(0(x1)))))))))))))))))))) → 0(0(1(1(0(1(0(1(1(0(0(0(0(0(0(0(0(1(1(0(x1)))))))))))))))))))) (31)
0(0(1(0(1(1(1(1(0(0(0(0(0(0(1(1(0(1(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(1(0(1(1(1(0(0(0(1(0(0(0(0(1(x1)))))))))))))))))))) (32)
0(0(1(0(1(1(1(1(0(0(0(1(0(0(0(1(1(0(0(0(x1)))))))))))))))))))) → 0(1(0(0(1(0(0(1(0(0(0(1(0(1(0(0(1(0(0(1(x1)))))))))))))))))))) (33)
0(0(1(1(0(0(1(1(0(1(0(0(0(1(0(0(1(0(1(0(x1)))))))))))))))))))) → 1(0(0(0(0(1(0(0(0(0(0(0(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (34)
0(0(1(1(0(1(0(0(0(0(1(1(0(0(1(0(0(1(0(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(0(0(1(0(1(0(0(1(0(0(0(0(0(x1)))))))))))))))))))) (35)
0(0(1(1(0(1(1(1(0(0(0(0(1(0(0(1(0(1(0(0(x1)))))))))))))))))))) → 1(1(1(0(0(0(0(1(1(0(0(0(0(0(0(0(1(0(0(1(x1)))))))))))))))))))) (36)
0(0(1(1(1(0(0(0(0(0(1(1(1(0(0(0(0(1(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(1(0(0(0(0(0(0(1(0(0(1(1(1(x1)))))))))))))))))))) (39)
0(1(0(0(0(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(1(1(0(0(0(1(0(1(1(0(0(1(x1)))))))))))))))))))) (42)
0(1(0(0(0(1(0(1(0(1(0(1(0(0(0(1(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(0(0(0(1(0(1(1(0(0(0(1(0(1(1(x1)))))))))))))))))))) (43)
0(1(0(1(0(0(0(0(1(1(1(0(1(0(1(0(0(0(1(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(1(0(0(1(1(0(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) (44)
0(1(0(1(0(0(0(1(0(1(0(1(1(0(1(0(1(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(1(1(0(0(1(1(0(0(0(0(0(1(0(1(0(x1)))))))))))))))))))) (45)
0(1(0(1(0(1(1(1(1(0(0(0(0(1(0(0(1(0(0(0(x1)))))))))))))))))))) → 1(1(0(1(1(0(0(1(0(0(0(0(0(0(1(1(0(0(0(0(x1)))))))))))))))))))) (47)
0(1(0(1(1(1(0(1(1(0(0(0(0(0(1(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(0(0(1(0(1(0(1(0(0(0(0(1(1(x1)))))))))))))))))))) (49)
0(1(1(0(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(0(x1)))))))))))))))))))) → 1(1(0(0(0(0(0(0(1(0(0(1(0(1(1(0(0(1(0(0(x1)))))))))))))))))))) (50)
0(1(1(0(0(1(1(1(1(0(0(0(1(0(0(0(0(0(1(0(x1)))))))))))))))))))) → 1(0(0(0(1(1(0(1(1(0(1(0(0(0(0(0(0(0(1(0(x1)))))))))))))))))))) (51)
0(1(1(0(1(1(0(0(0(0(0(0(0(1(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(1(1(1(0(0(0(0(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) (52)
0(1(1(1(1(0(0(0(0(1(0(0(1(0(0(1(0(0(1(0(x1)))))))))))))))))))) → 1(1(0(0(1(1(1(0(1(0(0(0(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) (53)
0(1(1(1(1(0(0(0(0(1(0(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 0(0(0(1(1(0(0(1(1(1(0(0(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) (54)
1(0(0(0(0(0(0(1(1(0(0(1(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(0(0(0(1(0(0(1(1(0(0(0(1(0(0(x1)))))))))))))))))))) (56)
1(0(0(0(0(0(1(1(1(0(0(1(1(0(1(1(0(0(0(0(x1)))))))))))))))))))) → 1(0(0(0(0(0(0(0(0(0(1(1(0(0(0(0(1(0(1(1(x1)))))))))))))))))))) (57)
1(0(0(0(0(1(1(0(1(1(0(0(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(1(1(0(0(0(0(1(1(1(0(0(0(0(1(x1)))))))))))))))))))) (58)
1(0(0(0(1(0(0(0(1(0(0(1(0(1(0(0(1(1(1(0(x1)))))))))))))))))))) → 0(0(0(0(1(0(0(0(0(0(0(1(0(0(0(1(1(1(0(0(x1)))))))))))))))))))) (60)
1(0(0(0(1(0(1(1(0(1(1(1(0(0(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(1(0(1(0(0(0(1(1(0(1(0(0(1(x1)))))))))))))))))))) (61)
1(0(0(0(1(1(0(0(0(1(0(1(0(0(0(1(0(1(1(0(x1)))))))))))))))))))) → 1(0(0(0(0(1(1(0(0(0(0(1(1(0(0(1(0(1(0(0(x1)))))))))))))))))))) (62)
1(0(0(0(1(1(0(0(1(0(1(1(0(0(1(1(0(0(0(0(x1)))))))))))))))))))) → 1(1(0(0(1(0(0(0(0(0(0(1(1(0(0(1(1(0(0(0(x1)))))))))))))))))))) (63)
1(0(0(0(1(1(1(0(0(1(0(0(0(0(0(1(1(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(0(0(0(0(0(0(0(0(1(1(0(1(1(x1)))))))))))))))))))) (64)
1(0(0(1(0(0(1(0(0(0(0(1(0(0(1(1(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(0(0(1(0(0(x1)))))))))))))))))))) (65)
1(0(0(1(0(0(1(1(1(0(0(0(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(1(0(1(1(1(0(0(0(1(0(1(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) (66)
1(0(0(1(0(1(0(0(0(0(1(1(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(1(0(0(0(0(1(0(1(0(0(0(1(1(0(0(0(x1)))))))))))))))))))) (67)
1(0(0(1(0(1(1(0(0(1(0(0(1(1(0(0(1(0(0(0(x1)))))))))))))))))))) → 1(0(0(1(0(0(1(0(1(1(1(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (69)
1(0(0(1(0(1(1(1(0(0(0(0(1(0(0(1(1(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(1(1(0(0(0(0(0(1(0(1(0(1(0(1(0(x1)))))))))))))))))))) (70)
1(0(0(1(0(1(1(1(0(0(1(0(1(1(0(1(1(0(1(1(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(1(1(0(1(1(1(0(0(1(0(1(0(1(x1)))))))))))))))))))) (71)
1(0(0(1(1(0(0(0(1(1(0(1(0(0(1(1(0(0(0(0(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(1(0(0(0(1(0(0(0(0(1(0(1(0(x1)))))))))))))))))))) (72)
1(0(0(1(1(0(0(1(0(1(0(0(0(0(1(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(1(0(0(1(1(0(0(0(0(0(0(1(0(0(1(x1)))))))))))))))))))) (73)
1(0(1(0(0(0(1(0(1(1(0(1(0(0(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(1(1(0(0(0(0(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) (75)
1(0(1(0(0(1(1(0(1(0(0(1(1(0(1(0(0(0(0(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(1(x1)))))))))))))))))))) (76)
1(0(1(1(1(0(0(1(0(1(1(0(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 1(1(0(0(1(1(1(0(0(0(0(0(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (78)
1(1(0(0(0(0(0(1(0(1(1(0(1(1(0(0(0(0(0(0(x1)))))))))))))))))))) → 1(1(0(1(0(0(0(0(1(0(0(0(0(0(0(0(0(1(0(0(x1)))))))))))))))))))) (79)
1(1(0(0(0(0(0(1(1(0(0(1(0(0(1(0(0(1(0(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(1(0(0(0(0(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (80)
1(1(0(0(0(0(1(1(0(1(1(0(1(0(0(0(0(0(1(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(0(1(0(0(0(0(0(0(1(1(0(1(1(x1)))))))))))))))))))) (81)
1(1(0(0(0(1(0(0(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(0(0(0(1(0(1(0(0(0(1(1(1(1(0(x1)))))))))))))))))))) (82)
1(1(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(1(1(1(0(0(0(0(1(0(1(0(1(0(0(0(x1)))))))))))))))))))) (83)
1(1(0(0(1(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) → 0(1(0(0(0(0(0(0(0(1(1(1(0(0(0(1(1(0(0(0(x1)))))))))))))))))))) (85)
1(1(0(0(1(1(0(0(1(0(0(0(0(0(1(1(1(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(1(1(1(0(1(0(0(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (86)
1(1(0(0(1(1(1(0(0(0(0(0(0(1(1(0(0(0(1(0(x1)))))))))))))))))))) → 1(0(1(0(0(0(0(0(0(0(1(0(1(1(0(0(1(0(0(1(x1)))))))))))))))))))) (87)
1(1(0(1(0(0(0(0(0(1(0(0(0(1(1(1(0(1(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(0(1(0(0(0(0(1(0(1(1(1(0(1(1(x1)))))))))))))))))))) (88)
1(1(0(1(0(1(0(0(0(0(1(0(0(1(0(0(0(0(1(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(1(0(1(0(0(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))))) (90)
1(1(0(1(0(1(0(0(0(1(1(1(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(1(0(1(0(0(1(0(0(1(0(0(0(0(x1)))))))))))))))))))) (91)
1(1(1(0(0(0(0(0(0(0(1(0(0(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 0(0(0(1(0(0(0(0(0(0(0(0(0(0(0(0(1(0(0(1(x1)))))))))))))))))))) (92)
1(1(1(0(1(0(0(1(0(0(0(1(1(1(0(0(0(0(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(0(1(0(1(0(1(0(0(1(0(1(1(0(x1)))))))))))))))))))) (94)
1(1(1(0(1(1(0(0(0(1(0(0(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) → 1(0(1(0(1(0(0(0(0(0(0(0(0(1(0(0(1(0(0(1(x1)))))))))))))))))))) (95)
1(1(1(1(1(1(0(0(0(1(0(0(0(0(1(0(0(0(0(0(x1)))))))))))))))))))) → 1(0(0(1(0(0(0(0(0(0(1(1(0(0(1(0(0(0(1(1(x1)))))))))))))))))))) (99)

1.1 Split

We split R in the relative problem D/R-D and R-D, where the rules D

0(0(0(0(1(0(0(0(1(1(1(1(1(0(1(1(0(0(0(1(x1)))))))))))))))))))) → 0(1(1(1(1(0(1(0(0(1(0(1(0(0(0(0(1(0(0(1(x1)))))))))))))))))))) (7)
0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(1(0(0(0(x1)))))))))))))))))))) → 0(1(1(0(1(0(0(1(1(0(0(1(0(0(1(1(0(1(0(0(x1)))))))))))))))))))) (12)
0(0(0(1(0(0(0(0(0(0(0(1(1(1(0(1(1(1(0(1(x1)))))))))))))))))))) → 0(1(0(0(1(1(0(0(0(1(1(0(0(1(0(0(1(0(0(1(x1)))))))))))))))))))) (13)
0(0(0(1(1(0(0(1(1(0(1(1(1(1(1(0(0(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(1(1(0(1(1(0(1(1(1(0(1(0(0(0(x1)))))))))))))))))))) (19)
0(0(1(0(0(0(0(0(1(1(1(1(1(1(0(1(0(0(0(1(x1)))))))))))))))))))) → 0(1(0(1(1(0(1(1(0(0(0(0(1(0(1(1(0(0(0(1(x1)))))))))))))))))))) (22)
0(0(1(0(1(0(0(1(0(0(1(1(1(0(0(0(0(1(1(1(x1)))))))))))))))))))) → 0(1(1(0(1(1(0(1(0(0(1(0(0(0(0(0(1(1(0(1(x1)))))))))))))))))))) (28)
0(0(1(1(0(1(1(1(1(1(0(1(0(1(0(0(0(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(0(0(0(1(1(0(1(0(1(1(0(1(1(0(1(0(x1)))))))))))))))))))) (38)
0(0(1(1(1(0(1(0(1(0(1(0(1(0(0(0(0(0(0(0(x1)))))))))))))))))))) → 0(0(1(0(1(0(0(0(0(1(0(1(0(0(0(1(0(1(1(0(x1)))))))))))))))))))) (40)
0(1(0(0(0(0(0(1(0(0(0(1(0(1(1(1(0(0(0(0(x1)))))))))))))))))))) → 0(0(0(0(0(0(1(0(1(0(0(1(0(0(1(0(1(1(0(0(x1)))))))))))))))))))) (41)
0(1(0(1(1(1(0(0(1(0(0(0(0(0(0(0(1(1(0(1(x1)))))))))))))))))))) → 0(0(0(0(0(1(0(1(0(1(1(1(0(1(0(0(0(1(0(1(x1)))))))))))))))))))) (48)
1(0(0(0(0(0(0(1(0(1(1(1(1(0(0(0(0(1(0(0(x1)))))))))))))))))))) → 0(1(0(1(0(0(0(1(0(0(1(1(0(0(0(1(0(0(1(0(x1)))))))))))))))))))) (55)
1(0(0(0(0(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(x1)))))))))))))))))))) → 1(0(0(0(0(0(1(1(0(1(0(0(0(0(1(1(0(1(0(1(x1)))))))))))))))))))) (59)
1(0(0(1(1(1(1(0(0(0(0(1(0(1(0(1(1(0(0(0(x1)))))))))))))))))))) → 1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(0(1(0(x1)))))))))))))))))))) (74)
1(0(1(1(1(0(0(0(0(0(0(1(0(1(1(1(0(0(1(0(x1)))))))))))))))))))) → 1(0(0(1(0(1(0(1(1(1(0(0(0(0(1(0(1(0(1(0(x1)))))))))))))))))))) (77)
1(1(0(0(0(1(1(0(1(0(0(0(0(1(1(1(0(0(0(1(x1)))))))))))))))))))) → 1(1(0(0(0(1(1(0(1(0(0(1(0(1(0(0(0(1(0(1(x1)))))))))))))))))))) (84)
1(1(1(0(0(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(x1)))))))))))))))))))) → 1(0(1(1(0(0(1(1(0(1(0(0(0(1(0(1(0(1(0(0(x1)))))))))))))))))))) (93)
1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(0(0(0(0(x1)))))))))))))))))))) → 0(1(0(0(1(1(0(0(0(0(1(0(0(1(0(1(1(0(1(0(x1)))))))))))))))))))) (96)
1(1(1(1(1(0(0(0(0(0(0(1(1(1(0(0(0(1(0(0(x1)))))))))))))))))))) → 1(1(0(1(0(0(1(0(1(0(1(0(0(1(0(0(0(1(1(0(x1)))))))))))))))))))) (97)
are deleted.

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(0(0(0(0(1(0(0(0(1(1(1(1(1(0(1(1(0(0(0(1(x1))))))))))))))))))))) → 1(0(1(1(1(1(0(1(0(0(1(0(1(0(0(0(0(1(0(0(1(x1))))))))))))))))))))) (100)
1(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(1(0(0(0(x1))))))))))))))))))))) → 1(0(1(1(0(1(0(0(1(1(0(0(1(0(0(1(1(0(1(0(0(x1))))))))))))))))))))) (101)
1(0(0(0(1(0(0(0(0(0(0(0(1(1(1(0(1(1(1(0(1(x1))))))))))))))))))))) → 1(0(1(0(0(1(1(0(0(0(1(1(0(0(1(0(0(1(0(0(1(x1))))))))))))))))))))) (102)
1(0(0(0(1(1(0(0(1(1(0(1(1(1(1(1(0(0(0(0(0(x1))))))))))))))))))))) → 1(0(0(1(0(0(0(1(1(0(1(1(0(1(1(1(0(1(0(0(0(x1))))))))))))))))))))) (103)
1(0(0(1(0(0(0(0(0(1(1(1(1(1(1(0(1(0(0(0(1(x1))))))))))))))))))))) → 1(0(1(0(1(1(0(1(1(0(0(0(0(1(0(1(1(0(0(0(1(x1))))))))))))))))))))) (104)
1(0(0(1(0(1(0(0(1(0(0(1(1(1(0(0(0(0(1(1(1(x1))))))))))))))))))))) → 1(0(1(1(0(1(1(0(1(0(0(1(0(0(0(0(0(1(1(0(1(x1))))))))))))))))))))) (105)
1(0(0(1(1(0(1(1(1(1(1(0(1(0(1(0(0(0(0(0(0(x1))))))))))))))))))))) → 1(0(0(1(0(0(0(0(1(1(0(1(0(1(1(0(1(1(0(1(0(x1))))))))))))))))))))) (106)
1(0(0(1(1(1(0(1(0(1(0(1(0(1(0(0(0(0(0(0(0(x1))))))))))))))))))))) → 1(0(0(1(0(1(0(0(0(0(1(0(1(0(0(0(1(0(1(1(0(x1))))))))))))))))))))) (107)
1(0(1(0(0(0(0(0(1(0(0(0(1(0(1(1(1(0(0(0(0(x1))))))))))))))))))))) → 1(0(0(0(0(0(0(1(0(1(0(0(1(0(0(1(0(1(1(0(0(x1))))))))))))))))))))) (108)
1(0(1(0(1(1(1(0(0(1(0(0(0(0(0(0(0(1(1(0(1(x1))))))))))))))))))))) → 1(0(0(0(0(0(1(0(1(0(1(1(1(0(1(0(0(0(1(0(1(x1))))))))))))))))))))) (109)
1(1(0(0(0(0(0(0(1(0(1(1(1(1(0(0(0(0(1(0(0(x1))))))))))))))))))))) → 1(0(1(0(1(0(0(0(1(0(0(1(1(0(0(0(1(0(0(1(0(x1))))))))))))))))))))) (110)
1(1(0(0(0(0(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(x1))))))))))))))))))))) → 1(1(0(0(0(0(0(1(1(0(1(0(0(0(0(1(1(0(1(0(1(x1))))))))))))))))))))) (111)
1(1(0(0(1(1(1(1(0(0(0(0(1(0(1(0(1(1(0(0(0(x1))))))))))))))))))))) → 1(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(0(1(0(x1))))))))))))))))))))) (112)
1(1(0(1(1(1(0(0(0(0(0(0(1(0(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 1(1(0(0(1(0(1(0(1(1(1(0(0(0(0(1(0(1(0(1(0(x1))))))))))))))))))))) (113)
1(1(1(0(0(0(1(1(0(1(0(0(0(0(1(1(1(0(0(0(1(x1))))))))))))))))))))) → 1(1(1(0(0(0(1(1(0(1(0(0(1(0(1(0(0(0(1(0(1(x1))))))))))))))))))))) (114)
1(1(1(1(0(0(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(x1))))))))))))))))))))) → 1(1(0(1(1(0(0(1(1(0(1(0(0(0(1(0(1(0(1(0(0(x1))))))))))))))))))))) (115)
1(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(0(0(0(0(x1))))))))))))))))))))) → 1(0(1(0(0(1(1(0(0(0(0(1(0(0(1(0(1(1(0(1(0(x1))))))))))))))))))))) (116)
1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(0(0(0(1(0(0(x1))))))))))))))))))))) → 1(1(1(0(1(0(0(1(0(1(0(1(0(0(1(0(0(0(1(1(0(x1))))))))))))))))))))) (117)
0(0(0(0(0(1(0(0(0(1(1(1(1(1(0(1(1(0(0(0(1(x1))))))))))))))))))))) → 0(0(1(1(1(1(0(1(0(0(1(0(1(0(0(0(0(1(0(0(1(x1))))))))))))))))))))) (118)
0(0(0(0(0(1(1(1(0(0(1(1(1(1(0(1(0(1(0(0(0(x1))))))))))))))))))))) → 0(0(1(1(0(1(0(0(1(1(0(0(1(0(0(1(1(0(1(0(0(x1))))))))))))))))))))) (119)
0(0(0(0(1(0(0(0(0(0(0(0(1(1(1(0(1(1(1(0(1(x1))))))))))))))))))))) → 0(0(1(0(0(1(1(0(0(0(1(1(0(0(1(0(0(1(0(0(1(x1))))))))))))))))))))) (120)
0(0(0(0(1(1(0(0(1(1(0(1(1(1(1(1(0(0(0(0(0(x1))))))))))))))))))))) → 0(0(0(1(0(0(0(1(1(0(1(1(0(1(1(1(0(1(0(0(0(x1))))))))))))))))))))) (121)
0(0(0(1(0(0(0(0(0(1(1(1(1(1(1(0(1(0(0(0(1(x1))))))))))))))))))))) → 0(0(1(0(1(1(0(1(1(0(0(0(0(1(0(1(1(0(0(0(1(x1))))))))))))))))))))) (122)
0(0(0(1(0(1(0(0(1(0(0(1(1(1(0(0(0(0(1(1(1(x1))))))))))))))))))))) → 0(0(1(1(0(1(1(0(1(0(0(1(0(0(0(0(0(1(1(0(1(x1))))))))))))))))))))) (123)
0(0(0(1(1(0(1(1(1(1(1(0(1(0(1(0(0(0(0(0(0(x1))))))))))))))))))))) → 0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(0(1(1(0(1(0(x1))))))))))))))))))))) (124)
0(0(0(1(1(1(0(1(0(1(0(1(0(1(0(0(0(0(0(0(0(x1))))))))))))))))))))) → 0(0(0(1(0(1(0(0(0(0(1(0(1(0(0(0(1(0(1(1(0(x1))))))))))))))))))))) (125)
0(0(1(0(0(0(0(0(1(0(0(0(1(0(1(1(1(0(0(0(0(x1))))))))))))))))))))) → 0(0(0(0(0(0(0(1(0(1(0(0(1(0(0(1(0(1(1(0(0(x1))))))))))))))))))))) (126)
0(0(1(0(1(1(1(0(0(1(0(0(0(0(0(0(0(1(1(0(1(x1))))))))))))))))))))) → 0(0(0(0(0(0(1(0(1(0(1(1(1(0(1(0(0(0(1(0(1(x1))))))))))))))))))))) (127)
0(1(0(0(0(0(0(0(1(0(1(1(1(1(0(0(0(0(1(0(0(x1))))))))))))))))))))) → 0(0(1(0(1(0(0(0(1(0(0(1(1(0(0(0(1(0(0(1(0(x1))))))))))))))))))))) (128)
0(1(0(0(0(0(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(x1))))))))))))))))))))) → 0(1(0(0(0(0(0(1(1(0(1(0(0(0(0(1(1(0(1(0(1(x1))))))))))))))))))))) (129)
0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(0(1(1(0(0(0(x1))))))))))))))))))))) → 0(1(1(1(0(0(1(0(1(0(0(0(1(1(0(0(0(1(0(1(0(x1))))))))))))))))))))) (130)
0(1(0(1(1(1(0(0(0(0(0(0(1(0(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 0(1(0(0(1(0(1(0(1(1(1(0(0(0(0(1(0(1(0(1(0(x1))))))))))))))))))))) (131)
0(1(1(0(0(0(1(1(0(1(0(0(0(0(1(1(1(0(0(0(1(x1))))))))))))))))))))) → 0(1(1(0(0(0(1(1(0(1(0(0(1(0(1(0(0(0(1(0(1(x1))))))))))))))))))))) (132)
0(1(1(1(0(0(1(0(0(0(0(1(0(0(1(1(0(0(1(1(0(x1))))))))))))))))))))) → 0(1(0(1(1(0(0(1(1(0(1(0(0(0(1(0(1(0(1(0(0(x1))))))))))))))))))))) (133)
0(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(0(0(0(0(x1))))))))))))))))))))) → 0(0(1(0(0(1(1(0(0(0(0(1(0(0(1(0(1(1(0(1(0(x1))))))))))))))))))))) (134)
0(1(1(1(1(1(0(0(0(0(0(0(1(1(1(0(0(0(1(0(0(x1))))))))))))))))))))) → 0(1(1(0(1(0(0(1(0(1(0(1(0(0(1(0(0(0(1(1(0(x1))))))))))))))))))))) (135)
1(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1))))))))))))))))))))) → 1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1))))))))))))))))))))) (136)
1(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1))))))))))))))))))))) → 1(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1))))))))))))))))))))) (137)
1(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1))))))))))))))))))))) → 1(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1))))))))))))))))))))) (138)
1(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 1(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1))))))))))))))))))))) (139)
1(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1))))))))))))))))))))) → 1(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1))))))))))))))))))))) (140)
1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (141)
1(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1))))))))))))))))))))) → 1(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))) (142)
0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1))))))))))))))))))))) → 0(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1))))))))))))))))))))) (143)
0(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1))))))))))))))))))))) → 0(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1))))))))))))))))))))) (144)
0(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1))))))))))))))))))))) → 0(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1))))))))))))))))))))) (145)
0(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1))))))))))))))))))))) (146)
0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1))))))))))))))))))))) → 0(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1))))))))))))))))))))) (147)
0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (148)
0(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1))))))))))))))))))))) → 0(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))) (149)

1.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS
01(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) → 01(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(11(x1))))))))))))))))))))) (150)
01(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) → 01(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(10(x1))))))))))))))))))))) (151)
11(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) → 11(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(11(x1))))))))))))))))))))) (152)
11(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) → 11(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(10(x1))))))))))))))))))))) (153)
01(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(01(x1))))))))))))))))))))) → 01(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(01(x1))))))))))))))))))))) (154)
01(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(00(x1))))))))))))))))))))) → 01(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(00(x1))))))))))))))))))))) (155)
11(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(01(x1))))))))))))))))))))) → 11(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(01(x1))))))))))))))))))))) (156)
11(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(00(x1))))))))))))))))))))) → 11(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(00(x1))))))))))))))))))))) (157)
01(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(11(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(11(x1))))))))))))))))))))) (158)
01(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(10(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(10(x1))))))))))))))))))))) (159)
11(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(11(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(11(x1))))))))))))))))))))) (160)
11(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(10(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(10(x1))))))))))))))))))))) (161)
01(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(01(x1))))))))))))))))))))) (162)
01(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(00(x1))))))))))))))))))))) (163)
11(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(01(x1))))))))))))))))))))) (164)
11(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(00(x1))))))))))))))))))))) (165)
01(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(11(x1))))))))))))))))))))) → 01(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) (166)
01(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(10(x1))))))))))))))))))))) → 01(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) (167)
11(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(11(x1))))))))))))))))))))) → 11(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) (168)
11(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(10(x1))))))))))))))))))))) → 11(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) (169)
01(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(11(x1))))))))))))))))))))) → 01(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) (170)
01(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(10(x1))))))))))))))))))))) → 01(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) (171)
11(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(11(x1))))))))))))))))))))) → 11(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) (172)
11(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(10(x1))))))))))))))))))))) → 11(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) (173)
01(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(01(x1))))))))))))))))))))) (174)
01(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(00(x1))))))))))))))))))))) (175)
11(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(01(x1))))))))))))))))))))) (176)
11(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(00(x1))))))))))))))))))))) (177)
01(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(01(x1))))))))))))))))))))) (178)
01(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(00(x1))))))))))))))))))))) (179)
11(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(01(x1))))))))))))))))))))) (180)
11(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(00(x1))))))))))))))))))))) (181)
01(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(01(x1))))))))))))))))))))) → 01(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(01(x1))))))))))))))))))))) (182)
01(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(00(x1))))))))))))))))))))) → 01(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(00(x1))))))))))))))))))))) (183)
11(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(01(x1))))))))))))))))))))) → 11(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(01(x1))))))))))))))))))))) (184)
11(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(00(x1))))))))))))))))))))) → 11(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(00(x1))))))))))))))))))))) (185)
01(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) → 01(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (186)
01(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) → 01(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (187)
11(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) → 11(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (188)
11(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) → 11(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (189)
00(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(01(x1))))))))))))))))))))) → 01(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(01(x1))))))))))))))))))))) (190)
00(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(00(x1))))))))))))))))))))) → 01(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(00(x1))))))))))))))))))))) (191)
10(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(01(x1))))))))))))))))))))) → 11(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(01(x1))))))))))))))))))))) (192)
10(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(00(x1))))))))))))))))))))) → 11(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(00(x1))))))))))))))))))))) (193)
00(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(11(x1))))))))))))))))))))) → 00(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(11(x1))))))))))))))))))))) (194)
00(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(10(x1))))))))))))))))))))) → 00(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(10(x1))))))))))))))))))))) (195)
10(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(11(x1))))))))))))))))))))) → 10(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(11(x1))))))))))))))))))))) (196)
10(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(10(x1))))))))))))))))))))) → 10(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(10(x1))))))))))))))))))))) (197)
00(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(01(x1))))))))))))))))))))) → 00(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(01(x1))))))))))))))))))))) (198)
00(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(00(x1))))))))))))))))))))) → 00(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(00(x1))))))))))))))))))))) (199)
10(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(01(x1))))))))))))))))))))) → 10(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(01(x1))))))))))))))))))))) (200)
10(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(00(x1))))))))))))))))))))) → 10(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(00(x1))))))))))))))))))))) (201)
00(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 00(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(01(x1))))))))))))))))))))) (202)
00(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 00(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(00(x1))))))))))))))))))))) (203)
10(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 10(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(01(x1))))))))))))))))))))) (204)
10(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 10(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(00(x1))))))))))))))))))))) (205)
00(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(11(x1))))))))))))))))))))) → 00(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (206)
00(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(10(x1))))))))))))))))))))) → 00(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (207)
10(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(11(x1))))))))))))))))))))) → 10(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (208)
10(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(10(x1))))))))))))))))))))) → 10(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (209)
00(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(01(x1))))))))))))))))))))) → 00(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(01(x1))))))))))))))))))))) (210)
00(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(00(x1))))))))))))))))))))) → 00(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(00(x1))))))))))))))))))))) (211)
10(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(01(x1))))))))))))))))))))) → 10(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(01(x1))))))))))))))))))))) (212)
10(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(00(x1))))))))))))))))))))) → 10(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(00(x1))))))))))))))))))))) (213)
00(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(01(x1))))))))))))))))))))) (214)
00(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(00(x1))))))))))))))))))))) (215)
10(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(01(x1))))))))))))))))))))) (216)
10(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(00(x1))))))))))))))))))))) (217)
00(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(01(x1))))))))))))))))))))) → 00(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(01(x1))))))))))))))))))))) (218)
00(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(00(x1))))))))))))))))))))) → 00(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(00(x1))))))))))))))))))))) (219)
10(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(01(x1))))))))))))))))))))) → 10(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(01(x1))))))))))))))))))))) (220)
10(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(00(x1))))))))))))))))))))) → 10(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(00(x1))))))))))))))))))))) (221)
01(01(01(01(01(00(11(01(00(11(00(11(00(10(10(10(10(10(10(11(01(x1))))))))))))))))))))) → 01(01(00(10(10(10(11(00(11(01(01(00(10(10(11(01(01(00(10(11(01(x1))))))))))))))))))))) (222)
01(01(01(01(01(00(11(01(00(11(00(11(00(10(10(10(10(10(10(11(00(x1))))))))))))))))))))) → 01(01(00(10(10(10(11(00(11(01(01(00(10(10(11(01(01(00(10(11(00(x1))))))))))))))))))))) (223)
11(01(01(01(01(00(11(01(00(11(00(11(00(10(10(10(10(10(10(11(01(x1))))))))))))))))))))) → 11(01(00(10(10(10(11(00(11(01(01(00(10(10(11(01(01(00(10(11(01(x1))))))))))))))))))))) (224)
11(01(01(01(01(00(11(01(00(11(00(11(00(10(10(10(10(10(10(11(00(x1))))))))))))))))))))) → 11(01(00(10(10(10(11(00(11(01(01(00(10(10(11(01(01(00(10(11(00(x1))))))))))))))))))))) (225)
01(01(01(01(00(10(11(00(11(00(11(01(00(10(11(01(00(10(11(00(11(x1))))))))))))))))))))) → 01(01(01(00(10(11(01(01(01(00(11(00(11(00(10(11(00(10(11(00(11(x1))))))))))))))))))))) (226)
01(01(01(01(00(10(11(00(11(00(11(01(00(10(11(01(00(10(11(00(10(x1))))))))))))))))))))) → 01(01(01(00(10(11(01(01(01(00(11(00(11(00(10(11(00(10(11(00(10(x1))))))))))))))))))))) (227)
11(01(01(01(00(10(11(00(11(00(11(01(00(10(11(01(00(10(11(00(11(x1))))))))))))))))))))) → 11(01(01(00(10(11(01(01(01(00(11(00(11(00(10(11(00(10(11(00(11(x1))))))))))))))))))))) (228)
11(01(01(01(00(10(11(00(11(00(11(01(00(10(11(01(00(10(11(00(10(x1))))))))))))))))))))) → 11(01(01(00(10(11(01(01(01(00(11(00(11(00(10(11(00(10(11(00(10(x1))))))))))))))))))))) (229)
01(01(00(10(11(00(10(10(10(11(01(00(11(01(00(11(01(01(00(11(01(x1))))))))))))))))))))) → 01(00(10(11(01(01(00(11(01(01(01(00(10(11(00(11(00(10(10(11(01(x1))))))))))))))))))))) (230)
01(01(00(10(11(00(10(10(10(11(01(00(11(01(00(11(01(01(00(11(00(x1))))))))))))))))))))) → 01(00(10(11(01(01(00(11(01(01(01(00(10(11(00(11(00(10(10(11(00(x1))))))))))))))))))))) (231)
11(01(00(10(11(00(10(10(10(11(01(00(11(01(00(11(01(01(00(11(01(x1))))))))))))))))))))) → 11(00(10(11(01(01(00(11(01(01(01(00(10(11(00(11(00(10(10(11(01(x1))))))))))))))))))))) (232)
11(01(00(10(11(00(10(10(10(11(01(00(11(01(00(11(01(01(00(11(00(x1))))))))))))))))))))) → 11(00(10(11(01(01(00(11(01(01(01(00(10(11(00(11(00(10(10(11(00(x1))))))))))))))))))))) (233)
01(00(11(00(11(01(00(10(10(11(01(00(10(10(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 01(00(11(00(11(00(11(01(01(00(10(10(10(10(10(11(01(00(10(11(01(x1))))))))))))))))))))) (234)
01(00(11(00(11(01(00(10(10(11(01(00(10(10(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 01(00(11(00(11(00(11(01(01(00(10(10(10(10(10(11(01(00(10(11(00(x1))))))))))))))))))))) (235)
11(00(11(00(11(01(00(10(10(11(01(00(10(10(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 11(00(11(00(11(00(11(01(01(00(10(10(10(10(10(11(01(00(10(11(01(x1))))))))))))))))))))) (236)
11(00(11(00(11(01(00(10(10(11(01(00(10(10(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 11(00(11(00(11(00(11(01(01(00(10(10(10(10(10(11(01(00(10(11(00(x1))))))))))))))))))))) (237)
00(11(01(00(11(00(11(00(11(01(01(00(10(10(11(01(00(11(01(00(11(x1))))))))))))))))))))) → 00(11(00(11(01(00(11(01(01(01(01(00(11(00(10(10(11(00(11(00(11(x1))))))))))))))))))))) (238)
00(11(01(00(11(00(11(00(11(01(01(00(10(10(11(01(00(11(01(00(10(x1))))))))))))))))))))) → 00(11(00(11(01(00(11(01(01(01(01(00(11(00(10(10(11(00(11(00(10(x1))))))))))))))))))))) (239)
10(11(01(00(11(00(11(00(11(01(01(00(10(10(11(01(00(11(01(00(11(x1))))))))))))))))))))) → 10(11(00(11(01(00(11(01(01(01(01(00(11(00(10(10(11(00(11(00(11(x1))))))))))))))))))))) (240)
10(11(01(00(11(00(11(00(11(01(01(00(10(10(11(01(00(11(01(00(10(x1))))))))))))))))))))) → 10(11(00(11(01(00(11(01(01(01(01(00(11(00(10(10(11(00(11(00(10(x1))))))))))))))))))))) (241)
00(10(11(00(11(01(00(10(10(10(11(00(11(00(10(11(00(11(00(11(01(x1))))))))))))))))))))) → 00(10(11(00(10(10(11(00(11(01(00(11(00(10(10(11(00(11(00(11(01(x1))))))))))))))))))))) (242)
00(10(11(00(11(01(00(10(10(10(11(00(11(00(10(11(00(11(00(11(00(x1))))))))))))))))))))) → 00(10(11(00(10(10(11(00(11(01(00(11(00(10(10(11(00(11(00(11(00(x1))))))))))))))))))))) (243)
10(10(11(00(11(01(00(10(10(10(11(00(11(00(10(11(00(11(00(11(01(x1))))))))))))))))))))) → 10(10(11(00(10(10(11(00(11(01(00(11(00(10(10(11(00(11(00(11(01(x1))))))))))))))))))))) (244)
10(10(11(00(11(01(00(10(10(10(11(00(11(00(10(11(00(11(00(11(00(x1))))))))))))))))))))) → 10(10(11(00(10(10(11(00(11(01(00(11(00(10(10(11(00(11(00(11(00(x1))))))))))))))))))))) (245)
00(10(10(10(10(11(00(11(01(00(10(11(00(11(01(01(00(11(01(01(01(x1))))))))))))))))))))) → 00(10(10(10(11(00(11(00(10(11(00(10(11(01(01(00(11(01(01(01(01(x1))))))))))))))))))))) (246)
00(10(10(10(10(11(00(11(01(00(10(11(00(11(01(01(00(11(01(01(00(x1))))))))))))))))))))) → 00(10(10(10(11(00(11(00(10(11(00(10(11(01(01(00(11(01(01(01(00(x1))))))))))))))))))))) (247)
10(10(10(10(10(11(00(11(01(00(10(11(00(11(01(01(00(11(01(01(01(x1))))))))))))))))))))) → 10(10(10(10(11(00(11(00(10(11(00(10(11(01(01(00(11(01(01(01(01(x1))))))))))))))))))))) (248)
10(10(10(10(10(11(00(11(01(00(10(11(00(11(01(01(00(11(01(01(00(x1))))))))))))))))))))) → 10(10(10(10(11(00(11(00(10(11(00(10(11(01(01(00(11(01(01(01(00(x1))))))))))))))))))))) (249)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[10(x1)] = x1 +
1
[11(x1)] = x1 +
0
[00(x1)] = x1 +
0
[01(x1)] = x1 +
1
all of the following rules can be deleted.
01(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) → 01(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(11(x1))))))))))))))))))))) (150)
01(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) → 01(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(10(x1))))))))))))))))))))) (151)
11(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) → 11(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(11(x1))))))))))))))))))))) (152)
11(01(01(01(00(11(01(01(00(10(10(10(10(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) → 11(00(10(10(10(11(00(11(01(00(11(00(11(01(01(01(00(11(01(00(10(x1))))))))))))))))))))) (153)
01(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(01(x1))))))))))))))))))))) → 01(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(01(x1))))))))))))))))))))) (154)
01(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(00(x1))))))))))))))))))))) → 01(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(00(x1))))))))))))))))))))) (155)
11(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(01(x1))))))))))))))))))))) → 11(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(01(x1))))))))))))))))))))) (156)
11(01(01(01(00(10(10(11(01(00(10(10(10(11(00(11(00(11(01(01(00(x1))))))))))))))))))))) → 11(00(10(11(00(11(01(00(10(11(01(00(11(01(00(10(11(00(11(01(00(x1))))))))))))))))))))) (157)
01(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(11(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(11(x1))))))))))))))))))))) (158)
01(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(10(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(10(x1))))))))))))))))))))) (159)
11(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(11(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(11(x1))))))))))))))))))))) (160)
11(01(01(00(11(01(01(01(01(01(01(00(10(10(11(00(10(10(11(00(10(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(00(10(11(01(00(11(01(00(11(01(00(10(x1))))))))))))))))))))) (161)
01(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(01(x1))))))))))))))))))))) (162)
01(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(00(x1))))))))))))))))))))) (163)
11(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(01(x1))))))))))))))))))))) (164)
11(01(01(00(10(11(01(00(10(11(00(10(10(10(10(11(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(01(01(00(10(11(00(10(11(00(10(10(11(00(11(01(01(00(x1))))))))))))))))))))) (165)
01(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(11(x1))))))))))))))))))))) → 01(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) (166)
01(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(10(x1))))))))))))))))))))) → 01(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) (167)
11(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(11(x1))))))))))))))))))))) → 11(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(11(x1))))))))))))))))))))) (168)
11(01(00(11(01(01(01(01(00(10(10(10(10(10(11(00(11(01(01(00(10(x1))))))))))))))))))))) → 11(00(11(00(10(11(00(10(11(01(01(01(00(11(00(10(11(01(01(00(10(x1))))))))))))))))))))) (169)
01(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(11(x1))))))))))))))))))))) → 01(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) (170)
01(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(10(x1))))))))))))))))))))) → 01(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) (171)
11(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(11(x1))))))))))))))))))))) → 11(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) (172)
11(01(00(11(00(11(01(00(11(01(00(10(10(11(01(01(01(00(10(10(10(x1))))))))))))))))))))) → 11(00(10(11(00(10(11(00(11(01(00(11(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) (173)
01(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(01(x1))))))))))))))))))))) (174)
01(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(00(x1))))))))))))))))))))) (175)
11(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(01(x1))))))))))))))))))))) (176)
11(01(00(10(11(00(10(10(10(10(11(00(11(00(11(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(01(01(01(00(10(11(00(11(00(10(11(00(10(11(00(11(00(x1))))))))))))))))))))) (177)
01(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(01(x1))))))))))))))))))))) (178)
01(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(00(x1))))))))))))))))))))) (179)
11(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(01(x1))))))))))))))))))))) (180)
11(01(00(10(10(11(00(11(00(11(00(11(00(11(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(01(00(11(00(11(01(01(01(00(11(00(11(01(01(00(11(00(10(11(00(x1))))))))))))))))))))) (181)
01(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(01(x1))))))))))))))))))))) → 01(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(01(x1))))))))))))))))))))) (182)
01(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(00(x1))))))))))))))))))))) → 01(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(00(x1))))))))))))))))))))) (183)
11(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(01(x1))))))))))))))))))))) → 11(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(01(x1))))))))))))))))))))) (184)
11(00(11(01(01(01(01(00(11(01(01(00(11(00(10(10(11(01(01(01(00(x1))))))))))))))))))))) → 11(01(01(01(01(01(00(11(00(11(01(00(11(01(00(11(00(10(11(01(00(x1))))))))))))))))))))) (185)
01(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) → 01(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (186)
01(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) → 01(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (187)
11(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(11(x1))))))))))))))))))))) → 11(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (188)
11(00(11(00(10(10(11(01(00(11(01(01(01(01(01(01(00(10(11(00(10(x1))))))))))))))))))))) → 11(01(01(01(01(00(11(00(11(00(10(10(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (189)
00(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(01(x1))))))))))))))))))))) → 01(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(01(x1))))))))))))))))))))) (190)
00(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(00(x1))))))))))))))))))))) → 01(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(00(x1))))))))))))))))))))) (191)
10(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(01(x1))))))))))))))))))))) → 11(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(01(x1))))))))))))))))))))) (192)
10(11(01(01(01(01(01(00(11(00(10(10(10(11(01(01(01(00(11(01(00(x1))))))))))))))))))))) → 11(00(11(00(11(01(01(00(11(01(00(10(11(01(01(00(11(01(00(11(00(x1))))))))))))))))))))) (193)
00(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(11(x1))))))))))))))))))))) → 00(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(11(x1))))))))))))))))))))) (194)
00(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(10(x1))))))))))))))))))))) → 00(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(10(x1))))))))))))))))))))) (195)
10(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(11(x1))))))))))))))))))))) → 10(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(11(x1))))))))))))))))))))) (196)
10(11(01(01(01(00(10(10(10(11(01(00(11(01(01(01(01(01(00(10(10(x1))))))))))))))))))))) → 10(11(01(01(01(01(00(10(11(00(11(01(01(01(00(10(11(00(11(00(10(x1))))))))))))))))))))) (197)
00(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(01(x1))))))))))))))))))))) → 00(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(01(x1))))))))))))))))))))) (198)
00(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(00(x1))))))))))))))))))))) → 00(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(00(x1))))))))))))))))))))) (199)
10(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(01(x1))))))))))))))))))))) → 10(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(01(x1))))))))))))))))))))) (200)
10(11(01(00(10(10(10(11(01(01(01(00(11(00(11(00(10(11(01(01(00(x1))))))))))))))))))))) → 10(10(10(11(01(00(11(00(11(01(01(00(10(11(01(01(00(11(00(11(00(x1))))))))))))))))))))) (201)
00(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 00(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(01(x1))))))))))))))))))))) (202)
00(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 00(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(00(x1))))))))))))))))))))) (203)
10(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(01(x1))))))))))))))))))))) → 10(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(01(x1))))))))))))))))))))) (204)
10(11(00(10(10(11(01(01(01(01(01(00(11(00(10(10(11(01(00(11(00(x1))))))))))))))))))))) → 10(11(01(00(11(00(11(00(10(10(11(01(01(01(00(11(00(11(00(11(00(x1))))))))))))))))))))) (205)
00(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(11(x1))))))))))))))))))))) → 00(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (206)
00(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(10(x1))))))))))))))))))))) → 00(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (207)
10(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(11(x1))))))))))))))))))))) → 10(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(11(x1))))))))))))))))))))) (208)
10(10(11(01(01(00(10(11(00(11(01(01(01(00(10(10(11(01(01(00(10(x1))))))))))))))))))))) → 10(10(11(01(01(00(10(11(00(11(01(00(11(00(11(01(01(00(11(00(10(x1))))))))))))))))))))) (209)
00(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(01(x1))))))))))))))))))))) → 00(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(01(x1))))))))))))))))))))) (210)
00(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(00(x1))))))))))))))))))))) → 00(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(00(x1))))))))))))))))))))) (211)
10(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(01(x1))))))))))))))))))))) → 10(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(01(x1))))))))))))))))))))) (212)
10(10(10(11(01(00(11(01(01(01(00(11(01(00(10(11(01(00(10(11(00(x1))))))))))))))))))))) → 10(11(00(10(11(01(00(10(11(00(11(01(01(00(11(00(11(00(11(01(00(x1))))))))))))))))))))) (213)
00(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(01(x1))))))))))))))))))))) (214)
00(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 01(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(00(x1))))))))))))))))))))) (215)
10(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(01(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(01(x1))))))))))))))))))))) (216)
10(10(10(11(00(10(10(10(11(01(01(00(11(01(01(01(01(01(01(01(00(x1))))))))))))))))))))) → 11(00(11(01(00(10(11(01(01(01(00(11(01(00(11(00(10(11(00(11(00(x1))))))))))))))))))))) (217)
00(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(01(x1))))))))))))))))))))) → 00(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(01(x1))))))))))))))))))))) (218)
00(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(00(x1))))))))))))))))))))) → 00(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(00(x1))))))))))))))))))))) (219)
10(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(01(x1))))))))))))))))))))) → 10(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(01(x1))))))))))))))))))))) (220)
10(10(10(10(10(11(01(01(01(01(01(00(10(10(11(01(01(00(11(01(00(x1))))))))))))))))))))) → 10(10(11(00(11(01(00(11(00(11(00(11(01(00(11(01(01(00(10(11(00(x1))))))))))))))))))))) (221)

1.1.1.1.1.1 R is empty

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

1.1.2 Split

We split R in the relative problem D/R-D and R-D, where the rules D

0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1)))))))))))))))))))) → 0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1)))))))))))))))))))) (5)
0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1)))))))))))))))))))) → 0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1)))))))))))))))))))) (9)
0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))) → 0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1)))))))))))))))))))) (37)
0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1)))))))))))))))))))) → 0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1)))))))))))))))))))) (46)
1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))) → 1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1)))))))))))))))))))) (68)
1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))) → 1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))) (98)
are deleted.

1.1.2.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1))))))))))))))))))))) → 1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1))))))))))))))))))))) (136)
1(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1))))))))))))))))))))) → 1(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1))))))))))))))))))))) (137)
1(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1))))))))))))))))))))) → 1(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1))))))))))))))))))))) (138)
1(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 1(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1))))))))))))))))))))) (139)
1(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1))))))))))))))))))))) → 1(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1))))))))))))))))))))) (140)
1(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1))))))))))))))))))))) → 1(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))) (142)
0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1))))))))))))))))))))) → 0(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1))))))))))))))))))))) (143)
0(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1))))))))))))))))))))) → 0(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1))))))))))))))))))))) (144)
0(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1))))))))))))))))))))) → 0(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1))))))))))))))))))))) (145)
0(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1))))))))))))))))))))) → 0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1))))))))))))))))))))) (146)
0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1))))))))))))))))))))) → 0(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1))))))))))))))))))))) (147)
0(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1))))))))))))))))))))) → 0(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1))))))))))))))))))))) (149)
1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (141)
0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (148)

1.1.2.1.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(1(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1)))))))))))))))))))))) → 1(1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1)))))))))))))))))))))) (250)
1(1(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1)))))))))))))))))))))) → 1(1(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1)))))))))))))))))))))) (251)
1(1(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))))) → 1(1(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1)))))))))))))))))))))) (252)
1(1(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1)))))))))))))))))))))) → 1(1(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1)))))))))))))))))))))) (253)
1(1(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))))) → 1(1(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1)))))))))))))))))))))) (254)
1(1(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))))) → 1(1(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))))) (255)
1(0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1)))))))))))))))))))))) → 1(0(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1)))))))))))))))))))))) (256)
1(0(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1)))))))))))))))))))))) → 1(0(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1)))))))))))))))))))))) (257)
1(0(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))))) → 1(0(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1)))))))))))))))))))))) (258)
1(0(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1)))))))))))))))))))))) → 1(0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1)))))))))))))))))))))) (259)
1(0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))))) → 1(0(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1)))))))))))))))))))))) (260)
1(0(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))))) → 1(0(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))))) (261)
0(1(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1)))))))))))))))))))))) → 0(1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1)))))))))))))))))))))) (262)
0(1(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1)))))))))))))))))))))) → 0(1(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1)))))))))))))))))))))) (263)
0(1(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))))) → 0(1(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1)))))))))))))))))))))) (264)
0(1(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1)))))))))))))))))))))) → 0(1(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1)))))))))))))))))))))) (265)
0(1(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))))) → 0(1(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1)))))))))))))))))))))) (266)
0(1(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))))) → 0(1(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))))) (267)
0(0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(1(1(1(1(1(0(x1)))))))))))))))))))))) → 0(0(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(0(1(1(0(x1)))))))))))))))))))))) (268)
0(0(0(0(0(0(1(1(0(1(0(1(0(0(1(1(0(0(1(1(0(1(x1)))))))))))))))))))))) → 0(0(0(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(x1)))))))))))))))))))))) (269)
0(0(0(0(1(1(0(1(1(1(1(0(0(1(0(0(1(0(0(0(1(0(x1)))))))))))))))))))))) → 0(0(0(1(1(0(0(0(1(0(0(0(0(1(1(0(1(0(1(1(1(0(x1)))))))))))))))))))))) (270)
0(0(0(1(0(1(0(0(1(1(1(0(0(1(1(1(1(1(0(0(1(0(x1)))))))))))))))))))))) → 0(0(0(1(0(1(0(1(0(0(0(1(1(1(1(1(1(0(0(1(1(0(x1)))))))))))))))))))))) (271)
0(0(1(0(0(1(0(1(0(1(0(0(0(1(1(1(0(0(1(0(0(1(x1)))))))))))))))))))))) → 0(0(1(0(1(0(0(1(0(0(0(0(0(1(0(1(1(1(0(1(0(1(x1)))))))))))))))))))))) (272)
0(0(1(1(1(1(1(0(1(0(0(1(1(0(1(0(0(0(1(0(0(0(x1)))))))))))))))))))))) → 0(0(1(1(1(1(0(1(0(1(1(0(1(1(0(0(0(1(0(0(0(0(x1)))))))))))))))))))))) (273)
1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 1(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (274)
1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (275)
0(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 0(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (276)
0(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 0(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (277)

1.1.2.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS

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

1.1.2.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[10(x1)] = x1 +
3/2
[12(x1)] = x1 +
0
[11(x1)] = x1 +
0
[13(x1)] = x1 +
1
[00(x1)] = x1 +
0
[02(x1)] = x1 +
3/2
[01(x1)] = x1 +
1
[03(x1)] = x1 +
0
all of the following rules can be deleted.
03(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(03(x1)))))))))))))))))))))) → 03(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(03(x1)))))))))))))))))))))) (278)
03(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(01(x1)))))))))))))))))))))) → 03(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(01(x1)))))))))))))))))))))) (279)
03(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(02(x1)))))))))))))))))))))) → 03(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(02(x1)))))))))))))))))))))) (280)
03(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(00(x1)))))))))))))))))))))) → 03(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(00(x1)))))))))))))))))))))) (281)
02(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(03(x1)))))))))))))))))))))) → 02(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(03(x1)))))))))))))))))))))) (282)
02(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(01(x1)))))))))))))))))))))) → 02(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(01(x1)))))))))))))))))))))) (283)
02(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(02(x1)))))))))))))))))))))) → 02(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(02(x1)))))))))))))))))))))) (284)
02(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(00(x1)))))))))))))))))))))) → 02(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(00(x1)))))))))))))))))))))) (285)
13(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(03(x1)))))))))))))))))))))) → 13(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(03(x1)))))))))))))))))))))) (286)
13(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(01(x1)))))))))))))))))))))) → 13(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(01(x1)))))))))))))))))))))) (287)
13(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(02(x1)))))))))))))))))))))) → 13(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(02(x1)))))))))))))))))))))) (288)
13(03(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(00(x1)))))))))))))))))))))) → 13(03(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(00(x1)))))))))))))))))))))) (289)
12(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(03(x1)))))))))))))))))))))) → 12(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(03(x1)))))))))))))))))))))) (290)
12(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(13(01(x1)))))))))))))))))))))) → 12(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(13(01(x1)))))))))))))))))))))) (291)
12(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(02(x1)))))))))))))))))))))) → 12(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(02(x1)))))))))))))))))))))) (292)
12(13(03(03(03(01(02(13(01(02(11(02(11(00(10(10(10(10(10(12(11(00(x1)))))))))))))))))))))) → 12(13(01(00(10(10(12(11(02(13(03(01(00(10(12(13(03(01(00(12(11(00(x1)))))))))))))))))))))) (293)
03(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(13(x1)))))))))))))))))))))) → 03(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(13(x1)))))))))))))))))))))) (294)
03(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(11(x1)))))))))))))))))))))) → 03(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(11(x1)))))))))))))))))))))) (295)
03(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(12(x1)))))))))))))))))))))) → 03(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(12(x1)))))))))))))))))))))) (296)
03(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(10(x1)))))))))))))))))))))) → 03(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(10(x1)))))))))))))))))))))) (297)
02(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(13(x1)))))))))))))))))))))) → 02(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(13(x1)))))))))))))))))))))) (298)
02(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(11(x1)))))))))))))))))))))) → 02(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(11(x1)))))))))))))))))))))) (299)
02(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(12(x1)))))))))))))))))))))) → 02(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(12(x1)))))))))))))))))))))) (300)
02(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(10(x1)))))))))))))))))))))) → 02(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(10(x1)))))))))))))))))))))) (301)
13(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(13(x1)))))))))))))))))))))) → 13(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(13(x1)))))))))))))))))))))) (302)
13(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(11(x1)))))))))))))))))))))) → 13(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(11(x1)))))))))))))))))))))) (303)
13(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(12(x1)))))))))))))))))))))) → 13(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(12(x1)))))))))))))))))))))) (304)
13(03(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(10(x1)))))))))))))))))))))) → 13(03(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(10(x1)))))))))))))))))))))) (305)
12(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(13(x1)))))))))))))))))))))) → 12(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(13(x1)))))))))))))))))))))) (306)
12(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(02(11(x1)))))))))))))))))))))) → 12(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(02(11(x1)))))))))))))))))))))) (307)
12(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(12(x1)))))))))))))))))))))) → 12(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(12(x1)))))))))))))))))))))) (308)
12(13(03(03(01(00(12(11(02(11(02(13(01(00(12(13(01(00(12(11(00(10(x1)))))))))))))))))))))) → 12(13(03(01(00(12(13(03(03(01(02(11(02(11(00(12(11(00(12(11(00(10(x1)))))))))))))))))))))) (309)
03(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(03(x1)))))))))))))))))))))) → 03(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(03(x1)))))))))))))))))))))) (310)
03(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(01(x1)))))))))))))))))))))) → 03(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(01(x1)))))))))))))))))))))) (311)
03(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(02(x1)))))))))))))))))))))) → 03(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(02(x1)))))))))))))))))))))) (312)
03(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(00(x1)))))))))))))))))))))) → 03(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(00(x1)))))))))))))))))))))) (313)
02(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(03(x1)))))))))))))))))))))) → 02(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(03(x1)))))))))))))))))))))) (314)
02(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(01(x1)))))))))))))))))))))) → 02(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(01(x1)))))))))))))))))))))) (315)
02(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(02(x1)))))))))))))))))))))) → 02(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(02(x1)))))))))))))))))))))) (316)
02(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(00(x1)))))))))))))))))))))) → 02(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(00(x1)))))))))))))))))))))) (317)
13(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(03(x1)))))))))))))))))))))) → 13(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(03(x1)))))))))))))))))))))) (318)
13(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(01(x1)))))))))))))))))))))) → 13(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(01(x1)))))))))))))))))))))) (319)
13(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(02(x1)))))))))))))))))))))) → 13(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(02(x1)))))))))))))))))))))) (320)
13(03(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(00(x1)))))))))))))))))))))) → 13(01(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(00(x1)))))))))))))))))))))) (321)
12(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(03(x1)))))))))))))))))))))) → 12(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(03(x1)))))))))))))))))))))) (322)
12(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(13(01(x1)))))))))))))))))))))) → 12(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(13(01(x1)))))))))))))))))))))) (323)
12(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(02(x1)))))))))))))))))))))) → 12(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(02(x1)))))))))))))))))))))) (324)
12(13(01(00(12(11(00(10(10(12(13(01(02(13(01(02(13(03(01(02(11(00(x1)))))))))))))))))))))) → 12(11(00(12(13(03(01(02(13(03(03(01(00(12(11(02(11(00(10(12(11(00(x1)))))))))))))))))))))) (325)
03(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(03(x1)))))))))))))))))))))) → 03(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(03(x1)))))))))))))))))))))) (326)
03(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(01(x1)))))))))))))))))))))) → 03(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(01(x1)))))))))))))))))))))) (327)
03(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(02(x1)))))))))))))))))))))) → 03(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(02(x1)))))))))))))))))))))) (328)
03(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(00(x1)))))))))))))))))))))) → 03(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(00(x1)))))))))))))))))))))) (329)
02(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(03(x1)))))))))))))))))))))) → 02(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(03(x1)))))))))))))))))))))) (330)
02(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(01(x1)))))))))))))))))))))) → 02(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(01(x1)))))))))))))))))))))) (331)
02(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(02(x1)))))))))))))))))))))) → 02(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(02(x1)))))))))))))))))))))) (332)
02(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(00(x1)))))))))))))))))))))) → 02(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(00(x1)))))))))))))))))))))) (333)
13(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(03(x1)))))))))))))))))))))) → 13(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(03(x1)))))))))))))))))))))) (334)
13(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(01(x1)))))))))))))))))))))) → 13(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(01(x1)))))))))))))))))))))) (335)
13(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(02(x1)))))))))))))))))))))) → 13(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(02(x1)))))))))))))))))))))) (336)
13(01(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(00(x1)))))))))))))))))))))) → 13(01(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(00(x1)))))))))))))))))))))) (337)
12(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(03(x1)))))))))))))))))))))) → 12(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(03(x1)))))))))))))))))))))) (338)
12(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(13(01(x1)))))))))))))))))))))) → 12(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(13(01(x1)))))))))))))))))))))) (339)
12(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(02(x1)))))))))))))))))))))) → 12(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(02(x1)))))))))))))))))))))) (340)
12(11(02(11(02(13(01(00(10(12(13(01(00(10(10(10(12(13(01(02(11(00(x1)))))))))))))))))))))) → 12(11(02(11(02(11(02(13(03(01(00(10(10(10(10(12(13(01(00(12(11(00(x1)))))))))))))))))))))) (341)
01(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(13(x1)))))))))))))))))))))) → 01(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(13(x1)))))))))))))))))))))) (342)
01(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(11(x1)))))))))))))))))))))) → 01(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(11(x1)))))))))))))))))))))) (343)
01(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(12(x1)))))))))))))))))))))) → 01(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(12(x1)))))))))))))))))))))) (344)
01(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(10(x1)))))))))))))))))))))) → 01(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(10(x1)))))))))))))))))))))) (345)
00(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(13(x1)))))))))))))))))))))) → 00(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(13(x1)))))))))))))))))))))) (346)
00(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(11(x1)))))))))))))))))))))) → 00(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(11(x1)))))))))))))))))))))) (347)
00(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(12(x1)))))))))))))))))))))) → 00(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(12(x1)))))))))))))))))))))) (348)
00(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(10(x1)))))))))))))))))))))) → 00(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(10(x1)))))))))))))))))))))) (349)
11(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(13(x1)))))))))))))))))))))) → 11(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(13(x1)))))))))))))))))))))) (350)
11(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(11(x1)))))))))))))))))))))) → 11(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(11(x1)))))))))))))))))))))) (351)
11(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(12(x1)))))))))))))))))))))) → 11(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(12(x1)))))))))))))))))))))) (352)
11(02(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(10(x1)))))))))))))))))))))) → 11(02(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(10(x1)))))))))))))))))))))) (353)
10(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(13(x1)))))))))))))))))))))) → 10(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(13(x1)))))))))))))))))))))) (354)
10(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(02(11(x1)))))))))))))))))))))) → 10(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(02(11(x1)))))))))))))))))))))) (355)
10(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(12(x1)))))))))))))))))))))) → 10(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(12(x1)))))))))))))))))))))) (356)
10(12(13(01(02(11(02(11(02(13(03(01(00(10(12(13(01(02(13(01(00(10(x1)))))))))))))))))))))) → 10(12(11(02(13(01(02(13(03(03(03(01(02(11(00(10(12(11(02(11(00(10(x1)))))))))))))))))))))) (357)
01(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(03(x1)))))))))))))))))))))) → 01(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(03(x1)))))))))))))))))))))) (358)
01(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(01(x1)))))))))))))))))))))) → 01(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(01(x1)))))))))))))))))))))) (359)
01(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(02(x1)))))))))))))))))))))) → 01(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(02(x1)))))))))))))))))))))) (360)
01(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(00(x1)))))))))))))))))))))) → 01(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(00(x1)))))))))))))))))))))) (361)
00(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(03(x1)))))))))))))))))))))) → 00(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(03(x1)))))))))))))))))))))) (362)
00(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(01(x1)))))))))))))))))))))) → 00(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(01(x1)))))))))))))))))))))) (363)
00(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(02(x1)))))))))))))))))))))) → 00(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(02(x1)))))))))))))))))))))) (364)
00(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(00(x1)))))))))))))))))))))) → 00(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(00(x1)))))))))))))))))))))) (365)
11(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(03(x1)))))))))))))))))))))) → 11(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(03(x1)))))))))))))))))))))) (366)
11(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(01(x1)))))))))))))))))))))) → 11(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(01(x1)))))))))))))))))))))) (367)
11(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(02(x1)))))))))))))))))))))) → 11(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(02(x1)))))))))))))))))))))) (368)
11(00(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(00(x1)))))))))))))))))))))) → 11(00(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(00(x1)))))))))))))))))))))) (369)
10(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(03(x1)))))))))))))))))))))) → 10(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(03(x1)))))))))))))))))))))) (370)
10(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(03(01(x1)))))))))))))))))))))) → 10(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(03(01(x1)))))))))))))))))))))) (371)
10(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(02(x1)))))))))))))))))))))) → 10(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(02(x1)))))))))))))))))))))) (372)
10(10(10(10(10(12(11(02(13(01(00(12(11(02(13(03(01(02(13(03(01(00(x1)))))))))))))))))))))) → 10(10(10(10(12(11(02(11(00(12(11(00(12(13(03(01(02(13(03(03(01(00(x1)))))))))))))))))))))) (373)

1.1.2.1.1.1.1.1 R is empty

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

1.1.2.2 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (141)
0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))) → 0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))) (148)

1.1.2.2.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 1(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (274)
1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (275)
0(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 0(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (276)
0(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1)))))))))))))))))))))) → 0(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1)))))))))))))))))))))) (277)

1.1.2.2.1.1 Closure Under Flat Contexts

Using the flat contexts

{1(☐), 0(☐)}

We obtain the transformed TRS
1(1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 1(1(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (390)
1(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 1(1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (391)
1(0(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 1(0(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (392)
1(0(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 1(0(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (393)
0(1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 0(1(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (394)
0(1(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 0(1(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (395)
0(0(1(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 0(0(1(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (396)
0(0(0(1(1(0(1(0(0(1(1(1(1(0(1(0(1(1(0(1(0(1(0(x1))))))))))))))))))))))) → 0(0(0(1(1(0(1(1(1(0(1(0(0(1(0(1(1(1(0(1(0(1(0(x1))))))))))))))))))))))) (397)

1.1.2.2.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (398)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (399)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (400)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (401)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (402)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (403)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (404)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (405)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (406)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (407)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (408)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (409)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (410)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (411)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (412)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (413)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (414)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (415)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (416)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (417)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (418)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (419)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (420)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (421)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (422)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (423)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (424)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (425)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (426)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (427)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (428)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (429)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (430)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (431)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (432)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (433)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (434)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (435)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (436)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (437)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (438)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (439)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (440)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (441)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (442)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (443)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (444)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (445)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (446)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (447)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (448)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (449)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (450)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (451)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (452)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (453)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (454)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (455)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (456)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (457)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (458)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (459)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (460)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (461)

1.1.2.2.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[10(x1)] = x1 +
1
[14(x1)] = x1 +
0
[12(x1)] = x1 +
0
[11(x1)] = x1 +
0
[15(x1)] = x1 +
1
[13(x1)] = x1 +
0
[17(x1)] = x1 +
0
[00(x1)] = x1 +
0
[04(x1)] = x1 +
1
[02(x1)] = x1 +
0
[06(x1)] = x1 +
0
[01(x1)] = x1 +
1
[05(x1)] = x1 +
0
[03(x1)] = x1 +
0
[07(x1)] = x1 +
0
all of the following rules can be deleted.
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (398)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (399)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (400)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (401)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (402)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (403)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (404)
10(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 10(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (405)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (406)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (407)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (408)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (409)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (410)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (411)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (412)
12(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 12(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (413)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (414)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (415)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (416)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (417)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (418)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (419)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (420)
11(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 11(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (421)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (422)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (423)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (424)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (425)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (426)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (427)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (428)
13(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 13(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (429)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (430)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (431)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (432)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (433)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (434)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (435)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (436)
00(10(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 00(10(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (437)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (438)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (439)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (440)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (441)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (442)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (443)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (444)
02(11(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 02(11(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (445)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (446)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (447)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (448)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (449)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (450)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (451)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (452)
01(00(14(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 01(00(14(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (453)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(00(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(00(x1))))))))))))))))))))))) (454)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(11(04(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(11(04(x1))))))))))))))))))))))) (455)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(02(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(02(x1))))))))))))))))))))))) (456)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(02(15(06(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(02(15(06(x1))))))))))))))))))))))) (457)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(01(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(01(x1))))))))))))))))))))))) (458)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(13(05(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(13(05(x1))))))))))))))))))))))) (459)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(03(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(03(x1))))))))))))))))))))))) (460)
03(01(04(12(15(06(13(01(00(10(14(12(15(02(11(04(12(15(02(15(06(17(07(x1))))))))))))))))))))))) → 03(01(04(12(11(00(14(12(15(06(13(05(02(11(00(14(12(15(02(15(06(17(07(x1))))))))))))))))))))))) (461)

1.1.2.2.1.1.1.1.1 R is empty

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