Certification Problem

Input (TPDB SRS_Standard/Zantema_06/18)

The rewrite relation of the following TRS is considered.

a(a(x1)) → b(a(b(x1))) (1)
a(a(a(x1))) → a(b(a(b(a(x1))))) (2)
a(b(a(x1))) → b(b(a(b(b(x1))))) (3)
a(a(a(a(x1)))) → a(a(b(a(b(a(a(x1))))))) (4)
a(a(b(a(x1)))) → a(b(b(a(b(a(b(x1))))))) (5)
a(b(a(a(x1)))) → b(a(b(a(b(b(a(x1))))))) (6)
a(b(b(a(x1)))) → b(b(b(a(b(b(b(x1))))))) (7)
a(a(a(a(a(x1))))) → a(a(a(b(a(b(a(a(a(x1))))))))) (8)
a(a(a(b(a(x1))))) → a(a(b(b(a(b(a(a(b(x1))))))))) (9)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(a(b(a(x1))))))))) (10)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(a(b(b(x1))))))))) (11)
a(b(a(a(a(x1))))) → b(a(a(b(a(b(b(a(a(x1))))))))) (12)
a(b(a(b(a(x1))))) → b(a(b(b(a(b(b(a(b(x1))))))))) (13)
a(b(b(a(a(x1))))) → b(b(a(b(a(b(b(b(a(x1))))))))) (14)
a(b(b(b(a(x1))))) → b(b(b(b(a(b(b(b(b(x1))))))))) (15)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(a(a(x1))) → b(b(a(b(x1)))) (16)
b(a(a(a(x1)))) → b(a(b(a(b(a(x1)))))) (17)
b(a(b(a(x1)))) → b(b(b(a(b(b(x1)))))) (18)
b(a(a(a(a(x1))))) → b(a(a(b(a(b(a(a(x1)))))))) (19)
b(a(a(b(a(x1))))) → b(a(b(b(a(b(a(b(x1)))))))) (20)
b(a(b(a(a(x1))))) → b(b(a(b(a(b(b(a(x1)))))))) (21)
b(a(b(b(a(x1))))) → b(b(b(b(a(b(b(b(x1)))))))) (22)
b(a(a(a(a(a(x1)))))) → b(a(a(a(b(a(b(a(a(a(x1)))))))))) (23)
b(a(a(a(b(a(x1)))))) → b(a(a(b(b(a(b(a(a(b(x1)))))))))) (24)
b(a(a(b(a(a(x1)))))) → b(a(b(a(b(a(b(a(b(a(x1)))))))))) (25)
b(a(a(b(b(a(x1)))))) → b(a(b(b(b(a(b(a(b(b(x1)))))))))) (26)
b(a(b(a(a(a(x1)))))) → b(b(a(a(b(a(b(b(a(a(x1)))))))))) (27)
b(a(b(a(b(a(x1)))))) → b(b(a(b(b(a(b(b(a(b(x1)))))))))) (28)
b(a(b(b(a(a(x1)))))) → b(b(b(a(b(a(b(b(b(a(x1)))))))))) (29)
b(a(b(b(b(a(x1)))))) → b(b(b(b(b(a(b(b(b(b(x1)))))))))) (30)
a(a(a(x1))) → a(b(a(b(x1)))) (31)
a(a(a(a(x1)))) → a(a(b(a(b(a(x1)))))) (32)
a(a(b(a(x1)))) → a(b(b(a(b(b(x1)))))) (33)
a(a(a(a(a(x1))))) → a(a(a(b(a(b(a(a(x1)))))))) (34)
a(a(a(b(a(x1))))) → a(a(b(b(a(b(a(b(x1)))))))) (35)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(b(a(x1)))))))) (36)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(b(b(x1)))))))) (37)
a(a(a(a(a(a(x1)))))) → a(a(a(a(b(a(b(a(a(a(x1)))))))))) (38)
a(a(a(a(b(a(x1)))))) → a(a(a(b(b(a(b(a(a(b(x1)))))))))) (39)
a(a(a(b(a(a(x1)))))) → a(a(b(a(b(a(b(a(b(a(x1)))))))))) (40)
a(a(a(b(b(a(x1)))))) → a(a(b(b(b(a(b(a(b(b(x1)))))))))) (41)
a(a(b(a(a(a(x1)))))) → a(b(a(a(b(a(b(b(a(a(x1)))))))))) (42)
a(a(b(a(b(a(x1)))))) → a(b(a(b(b(a(b(b(a(b(x1)))))))))) (43)
a(a(b(b(a(a(x1)))))) → a(b(b(a(b(a(b(b(b(a(x1)))))))))) (44)
a(a(b(b(b(a(x1)))))) → a(b(b(b(b(a(b(b(b(b(x1)))))))))) (45)

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):

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

We obtain the labeled TRS
a1(a1(a1(x1))) → a0(b1(a0(b1(x1)))) (46)
a1(a1(a0(x1))) → a0(b1(a0(b0(x1)))) (47)
b1(a1(a1(x1))) → b0(b1(a0(b1(x1)))) (48)
b1(a1(a0(x1))) → b0(b1(a0(b0(x1)))) (49)
a1(a1(a1(a1(x1)))) → a1(a0(b1(a0(b1(a1(x1)))))) (50)
a1(a1(a1(a0(x1)))) → a1(a0(b1(a0(b1(a0(x1)))))) (51)
b1(a1(a1(a1(x1)))) → b1(a0(b1(a0(b1(a1(x1)))))) (52)
b1(a1(a1(a0(x1)))) → b1(a0(b1(a0(b1(a0(x1)))))) (53)
a1(a0(b1(a1(x1)))) → a0(b0(b1(a0(b0(b1(x1)))))) (54)
a1(a0(b1(a0(x1)))) → a0(b0(b1(a0(b0(b0(x1)))))) (55)
b1(a0(b1(a1(x1)))) → b0(b0(b1(a0(b0(b1(x1)))))) (56)
b1(a0(b1(a0(x1)))) → b0(b0(b1(a0(b0(b0(x1)))))) (57)
a1(a1(a1(a1(a1(x1))))) → a1(a1(a0(b1(a0(b1(a1(a1(x1)))))))) (58)
a1(a1(a1(a1(a0(x1))))) → a1(a1(a0(b1(a0(b1(a1(a0(x1)))))))) (59)
b1(a1(a1(a1(a1(x1))))) → b1(a1(a0(b1(a0(b1(a1(a1(x1)))))))) (60)
b1(a1(a1(a1(a0(x1))))) → b1(a1(a0(b1(a0(b1(a1(a0(x1)))))))) (61)
a1(a1(a0(b1(a1(x1))))) → a1(a0(b0(b1(a0(b1(a0(b1(x1)))))))) (62)
a1(a1(a0(b1(a0(x1))))) → a1(a0(b0(b1(a0(b1(a0(b0(x1)))))))) (63)
b1(a1(a0(b1(a1(x1))))) → b1(a0(b0(b1(a0(b1(a0(b1(x1)))))))) (64)
b1(a1(a0(b1(a0(x1))))) → b1(a0(b0(b1(a0(b1(a0(b0(x1)))))))) (65)
a1(a0(b1(a1(a1(x1))))) → a0(b1(a0(b1(a0(b0(b1(a1(x1)))))))) (66)
a1(a0(b1(a1(a0(x1))))) → a0(b1(a0(b1(a0(b0(b1(a0(x1)))))))) (67)
b1(a0(b1(a1(a1(x1))))) → b0(b1(a0(b1(a0(b0(b1(a1(x1)))))))) (68)
b1(a0(b1(a1(a0(x1))))) → b0(b1(a0(b1(a0(b0(b1(a0(x1)))))))) (69)
a1(a0(b0(b1(a1(x1))))) → a0(b0(b0(b1(a0(b0(b0(b1(x1)))))))) (70)
a1(a0(b0(b1(a0(x1))))) → a0(b0(b0(b1(a0(b0(b0(b0(x1)))))))) (71)
b1(a0(b0(b1(a1(x1))))) → b0(b0(b0(b1(a0(b0(b0(b1(x1)))))))) (72)
b1(a0(b0(b1(a0(x1))))) → b0(b0(b0(b1(a0(b0(b0(b0(x1)))))))) (73)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(a0(b1(a0(b1(a1(a1(a1(x1)))))))))) (74)
a1(a1(a1(a1(a1(a0(x1)))))) → a1(a1(a1(a0(b1(a0(b1(a1(a1(a0(x1)))))))))) (75)
b1(a1(a1(a1(a1(a1(x1)))))) → b1(a1(a1(a0(b1(a0(b1(a1(a1(a1(x1)))))))))) (76)
b1(a1(a1(a1(a1(a0(x1)))))) → b1(a1(a1(a0(b1(a0(b1(a1(a1(a0(x1)))))))))) (77)
a1(a1(a1(a0(b1(a1(x1)))))) → a1(a1(a0(b0(b1(a0(b1(a1(a0(b1(x1)))))))))) (78)
a1(a1(a1(a0(b1(a0(x1)))))) → a1(a1(a0(b0(b1(a0(b1(a1(a0(b0(x1)))))))))) (79)
b1(a1(a1(a0(b1(a1(x1)))))) → b1(a1(a0(b0(b1(a0(b1(a1(a0(b1(x1)))))))))) (80)
b1(a1(a1(a0(b1(a0(x1)))))) → b1(a1(a0(b0(b1(a0(b1(a1(a0(b0(x1)))))))))) (81)
a1(a1(a0(b1(a1(a1(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))))) (82)
a1(a1(a0(b1(a1(a0(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))))) (83)
b1(a1(a0(b1(a1(a1(x1)))))) → b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))))) (84)
b1(a1(a0(b1(a1(a0(x1)))))) → b1(a0(b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))))) (85)
a1(a1(a0(b0(b1(a1(x1)))))) → a1(a0(b0(b0(b1(a0(b1(a0(b0(b1(x1)))))))))) (86)
a1(a1(a0(b0(b1(a0(x1)))))) → a1(a0(b0(b0(b1(a0(b1(a0(b0(b0(x1)))))))))) (87)
b1(a1(a0(b0(b1(a1(x1)))))) → b1(a0(b0(b0(b1(a0(b1(a0(b0(b1(x1)))))))))) (88)
b1(a1(a0(b0(b1(a0(x1)))))) → b1(a0(b0(b0(b1(a0(b1(a0(b0(b0(x1)))))))))) (89)
a1(a0(b1(a1(a1(a1(x1)))))) → a0(b1(a1(a0(b1(a0(b0(b1(a1(a1(x1)))))))))) (90)
a1(a0(b1(a1(a1(a0(x1)))))) → a0(b1(a1(a0(b1(a0(b0(b1(a1(a0(x1)))))))))) (91)
b1(a0(b1(a1(a1(a1(x1)))))) → b0(b1(a1(a0(b1(a0(b0(b1(a1(a1(x1)))))))))) (92)
b1(a0(b1(a1(a1(a0(x1)))))) → b0(b1(a1(a0(b1(a0(b0(b1(a1(a0(x1)))))))))) (93)
a1(a0(b1(a0(b1(a1(x1)))))) → a0(b1(a0(b0(b1(a0(b0(b1(a0(b1(x1)))))))))) (94)
a1(a0(b1(a0(b1(a0(x1)))))) → a0(b1(a0(b0(b1(a0(b0(b1(a0(b0(x1)))))))))) (95)
b1(a0(b1(a0(b1(a1(x1)))))) → b0(b1(a0(b0(b1(a0(b0(b1(a0(b1(x1)))))))))) (96)
b1(a0(b1(a0(b1(a0(x1)))))) → b0(b1(a0(b0(b1(a0(b0(b1(a0(b0(x1)))))))))) (97)
a1(a0(b0(b1(a1(a1(x1)))))) → a0(b0(b1(a0(b1(a0(b0(b0(b1(a1(x1)))))))))) (98)
a1(a0(b0(b1(a1(a0(x1)))))) → a0(b0(b1(a0(b1(a0(b0(b0(b1(a0(x1)))))))))) (99)
b1(a0(b0(b1(a1(a1(x1)))))) → b0(b0(b1(a0(b1(a0(b0(b0(b1(a1(x1)))))))))) (100)
b1(a0(b0(b1(a1(a0(x1)))))) → b0(b0(b1(a0(b1(a0(b0(b0(b1(a0(x1)))))))))) (101)
a1(a0(b0(b0(b1(a1(x1)))))) → a0(b0(b0(b0(b1(a0(b0(b0(b0(b1(x1)))))))))) (102)
a1(a0(b0(b0(b1(a0(x1)))))) → a0(b0(b0(b0(b1(a0(b0(b0(b0(b0(x1)))))))))) (103)
b1(a0(b0(b0(b1(a1(x1)))))) → b0(b0(b0(b0(b1(a0(b0(b0(b0(b1(x1)))))))))) (104)
b1(a0(b0(b0(b1(a0(x1)))))) → b0(b0(b0(b0(b1(a0(b0(b0(b0(b0(x1)))))))))) (105)

1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[b0(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a1(x1)] = x1 +
1
all of the following rules can be deleted.
a1(a1(a1(x1))) → a0(b1(a0(b1(x1)))) (46)
a1(a1(a0(x1))) → a0(b1(a0(b0(x1)))) (47)
b1(a1(a1(x1))) → b0(b1(a0(b1(x1)))) (48)
b1(a1(a0(x1))) → b0(b1(a0(b0(x1)))) (49)
a1(a1(a1(a1(x1)))) → a1(a0(b1(a0(b1(a1(x1)))))) (50)
a1(a1(a1(a0(x1)))) → a1(a0(b1(a0(b1(a0(x1)))))) (51)
b1(a1(a1(a1(x1)))) → b1(a0(b1(a0(b1(a1(x1)))))) (52)
b1(a1(a1(a0(x1)))) → b1(a0(b1(a0(b1(a0(x1)))))) (53)
a1(a0(b1(a1(x1)))) → a0(b0(b1(a0(b0(b1(x1)))))) (54)
a1(a0(b1(a0(x1)))) → a0(b0(b1(a0(b0(b0(x1)))))) (55)
b1(a0(b1(a1(x1)))) → b0(b0(b1(a0(b0(b1(x1)))))) (56)
a1(a1(a1(a1(a1(x1))))) → a1(a1(a0(b1(a0(b1(a1(a1(x1)))))))) (58)
a1(a1(a1(a1(a0(x1))))) → a1(a1(a0(b1(a0(b1(a1(a0(x1)))))))) (59)
b1(a1(a1(a1(a1(x1))))) → b1(a1(a0(b1(a0(b1(a1(a1(x1)))))))) (60)
b1(a1(a1(a1(a0(x1))))) → b1(a1(a0(b1(a0(b1(a1(a0(x1)))))))) (61)
a1(a1(a0(b1(a1(x1))))) → a1(a0(b0(b1(a0(b1(a0(b1(x1)))))))) (62)
a1(a1(a0(b1(a0(x1))))) → a1(a0(b0(b1(a0(b1(a0(b0(x1)))))))) (63)
b1(a1(a0(b1(a1(x1))))) → b1(a0(b0(b1(a0(b1(a0(b1(x1)))))))) (64)
b1(a1(a0(b1(a0(x1))))) → b1(a0(b0(b1(a0(b1(a0(b0(x1)))))))) (65)
a1(a0(b1(a1(a1(x1))))) → a0(b1(a0(b1(a0(b0(b1(a1(x1)))))))) (66)
a1(a0(b1(a1(a0(x1))))) → a0(b1(a0(b1(a0(b0(b1(a0(x1)))))))) (67)
b1(a0(b1(a1(a1(x1))))) → b0(b1(a0(b1(a0(b0(b1(a1(x1)))))))) (68)
b1(a0(b1(a1(a0(x1))))) → b0(b1(a0(b1(a0(b0(b1(a0(x1)))))))) (69)
a1(a0(b0(b1(a1(x1))))) → a0(b0(b0(b1(a0(b0(b0(b1(x1)))))))) (70)
a1(a0(b0(b1(a0(x1))))) → a0(b0(b0(b1(a0(b0(b0(b0(x1)))))))) (71)
b1(a0(b0(b1(a1(x1))))) → b0(b0(b0(b1(a0(b0(b0(b1(x1)))))))) (72)
a1(a1(a1(a0(b1(a1(x1)))))) → a1(a1(a0(b0(b1(a0(b1(a1(a0(b1(x1)))))))))) (78)
b1(a1(a1(a0(b1(a1(x1)))))) → b1(a1(a0(b0(b1(a0(b1(a1(a0(b1(x1)))))))))) (80)
a1(a1(a0(b1(a1(a1(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))))) (82)
a1(a1(a0(b1(a1(a0(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))))) (83)
b1(a1(a0(b1(a1(a1(x1)))))) → b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))))) (84)
b1(a1(a0(b1(a1(a0(x1)))))) → b1(a0(b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))))) (85)
a1(a1(a0(b0(b1(a1(x1)))))) → a1(a0(b0(b0(b1(a0(b1(a0(b0(b1(x1)))))))))) (86)
a1(a1(a0(b0(b1(a0(x1)))))) → a1(a0(b0(b0(b1(a0(b1(a0(b0(b0(x1)))))))))) (87)
b1(a1(a0(b0(b1(a1(x1)))))) → b1(a0(b0(b0(b1(a0(b1(a0(b0(b1(x1)))))))))) (88)
b1(a1(a0(b0(b1(a0(x1)))))) → b1(a0(b0(b0(b1(a0(b1(a0(b0(b0(x1)))))))))) (89)
a1(a0(b1(a1(a1(a1(x1)))))) → a0(b1(a1(a0(b1(a0(b0(b1(a1(a1(x1)))))))))) (90)
a1(a0(b1(a1(a1(a0(x1)))))) → a0(b1(a1(a0(b1(a0(b0(b1(a1(a0(x1)))))))))) (91)
a1(a0(b1(a0(b1(a1(x1)))))) → a0(b1(a0(b0(b1(a0(b0(b1(a0(b1(x1)))))))))) (94)
a1(a0(b1(a0(b1(a0(x1)))))) → a0(b1(a0(b0(b1(a0(b0(b1(a0(b0(x1)))))))))) (95)
b1(a0(b1(a0(b1(a1(x1)))))) → b0(b1(a0(b0(b1(a0(b0(b1(a0(b1(x1)))))))))) (96)
a1(a0(b0(b1(a1(a1(x1)))))) → a0(b0(b1(a0(b1(a0(b0(b0(b1(a1(x1)))))))))) (98)
a1(a0(b0(b1(a1(a0(x1)))))) → a0(b0(b1(a0(b1(a0(b0(b0(b1(a0(x1)))))))))) (99)
b1(a0(b0(b1(a1(a1(x1)))))) → b0(b0(b1(a0(b1(a0(b0(b0(b1(a1(x1)))))))))) (100)
b1(a0(b0(b1(a1(a0(x1)))))) → b0(b0(b1(a0(b1(a0(b0(b0(b1(a0(x1)))))))))) (101)
a1(a0(b0(b0(b1(a1(x1)))))) → a0(b0(b0(b0(b1(a0(b0(b0(b0(b1(x1)))))))))) (102)
a1(a0(b0(b0(b1(a0(x1)))))) → a0(b0(b0(b0(b1(a0(b0(b0(b0(b0(x1)))))))))) (103)
b1(a0(b0(b0(b1(a1(x1)))))) → b0(b0(b0(b0(b1(a0(b0(b0(b0(b1(x1)))))))))) (104)

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a0(b1(a0(b1(x1)))) → b0(b0(a0(b1(b0(b0(x1)))))) (106)
a0(b1(b0(a0(b1(x1))))) → b0(b0(b0(a0(b1(b0(b0(b0(x1)))))))) (107)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (108)
a0(a1(a1(a1(a1(a1(x1)))))) → a0(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (109)
a1(a1(a1(a1(a1(b1(x1)))))) → a1(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (110)
a0(a1(a1(a1(a1(b1(x1)))))) → a0(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (111)
a0(b1(a0(a1(a1(a1(x1)))))) → b0(a0(a1(b1(a0(b1(b0(a0(a1(a1(x1)))))))))) (112)
a0(b1(a0(a1(a1(b1(x1)))))) → b0(a0(a1(b1(a0(b1(b0(a0(a1(b1(x1)))))))))) (113)
a1(a1(a1(b1(a0(b1(x1)))))) → a1(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (114)
a0(a1(a1(b1(a0(b1(x1)))))) → a0(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (115)
a0(b1(a0(b1(a0(b1(x1)))))) → b0(a0(b1(b0(a0(b1(b0(a0(b1(b0(x1)))))))))) (116)
a0(b1(b0(b0(a0(b1(x1)))))) → b0(b0(b0(b0(a0(b1(b0(b0(b0(b0(x1)))))))))) (117)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a0#(b1(b0(b0(a0(b1(x1)))))) → a0#(b1(b0(b0(b0(b0(x1)))))) (118)
a0#(b1(b0(a0(b1(x1))))) → a0#(b1(b0(b0(b0(x1))))) (119)
a0#(b1(a0(b1(x1)))) → a0#(b1(b0(b0(x1)))) (120)
a0#(b1(a0(b1(a0(b1(x1)))))) → a0#(b1(b0(x1))) (121)
a0#(b1(a0(b1(a0(b1(x1)))))) → a0#(b1(b0(a0(b1(b0(x1)))))) (122)
a0#(b1(a0(b1(a0(b1(x1)))))) → a0#(b1(b0(a0(b1(b0(a0(b1(b0(x1))))))))) (123)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(b1(b0(a0(a1(b1(x1)))))) (124)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(a1(b1(x1))) (125)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(a1(b1(a0(b1(b0(a0(a1(b1(x1))))))))) (126)
a0#(b1(a0(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(b0(a0(a1(b1(x1)))))))) (127)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(b1(b0(a0(a1(a1(x1)))))) (128)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(b1(a0(b1(b0(a0(a1(a1(x1))))))))) (129)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(a1(x1))) (130)
a0#(b1(a0(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(b0(a0(a1(a1(x1)))))))) (131)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(b1(a0(a1(b1(b0(x1)))))) (132)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (133)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (134)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (135)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(b1(a0(a1(b1(b0(x1))))))))) (136)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(b1(a0(a1(a1(b1(x1)))))) (137)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (138)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (139)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(b1(x1)))))))) (140)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(b1(x1))))))))) (141)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(b1(a0(a1(a1(a1(x1)))))) (142)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (143)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (144)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(a1(x1)))))))) (145)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(a1(x1))))))))) (146)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(b1(a0(a1(b1(b0(x1)))))) (147)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (148)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (149)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(b1(a0(a1(b1(b0(x1))))))))) (150)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (151)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(b1(a0(a1(a1(b1(x1)))))) (152)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (153)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(b1(x1)))))))) (154)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(b1(x1))))))))) (155)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (156)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(b1(a0(a1(a1(a1(x1)))))) (157)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (158)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(a1(x1)))))))) (159)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(a1(x1))))))))) (160)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (161)

1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[b0(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a1(x1)] = x1 +
1
[a0#(x1)] = x1 +
0
[a1#(x1)] = x1 +
0
together with the usable rules
a0(b1(a0(b1(x1)))) → b0(b0(a0(b1(b0(b0(x1)))))) (106)
a0(b1(b0(a0(b1(x1))))) → b0(b0(b0(a0(b1(b0(b0(b0(x1)))))))) (107)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (108)
a0(a1(a1(a1(a1(a1(x1)))))) → a0(a1(a1(b1(a0(b1(a0(a1(a1(a1(x1)))))))))) (109)
a1(a1(a1(a1(a1(b1(x1)))))) → a1(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (110)
a0(a1(a1(a1(a1(b1(x1)))))) → a0(a1(a1(b1(a0(b1(a0(a1(a1(b1(x1)))))))))) (111)
a0(b1(a0(a1(a1(a1(x1)))))) → b0(a0(a1(b1(a0(b1(b0(a0(a1(a1(x1)))))))))) (112)
a0(b1(a0(a1(a1(b1(x1)))))) → b0(a0(a1(b1(a0(b1(b0(a0(a1(b1(x1)))))))))) (113)
a1(a1(a1(b1(a0(b1(x1)))))) → a1(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (114)
a0(a1(a1(b1(a0(b1(x1)))))) → a0(a1(b1(b0(a0(b1(a0(a1(b1(b0(x1)))))))))) (115)
a0(b1(a0(b1(a0(b1(x1)))))) → b0(a0(b1(b0(a0(b1(b0(a0(b1(b0(x1)))))))))) (116)
a0(b1(b0(b0(a0(b1(x1)))))) → b0(b0(b0(b0(a0(b1(b0(b0(b0(b0(x1)))))))))) (117)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(b1(b0(a0(a1(b1(x1)))))) (124)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(a1(b1(x1))) (125)
a0#(b1(a0(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(b0(a0(a1(b1(x1)))))))) (127)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(b1(b0(a0(a1(a1(x1)))))) (128)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(a1(x1))) (130)
a0#(b1(a0(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(b0(a0(a1(a1(x1)))))))) (131)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(b1(a0(a1(b1(b0(x1)))))) (132)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (133)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (135)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(b1(a0(a1(b1(b0(x1))))))))) (136)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(b1(a0(a1(a1(b1(x1)))))) (137)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (138)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(b1(x1)))))))) (140)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(b1(x1))))))))) (141)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(b1(a0(a1(a1(a1(x1)))))) (142)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (144)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(a1(x1)))))))) (145)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(a1(x1))))))))) (146)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(b1(a0(a1(b1(b0(x1)))))) (147)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (148)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (149)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(b1(a0(a1(b1(b0(x1))))))))) (150)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(b1(a0(a1(a1(b1(x1)))))) (152)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (153)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(b1(x1)))))))) (154)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(b1(x1))))))))) (155)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(b1(a0(a1(a1(a1(x1)))))) (157)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (158)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(b1(a0(a1(a1(a1(x1)))))))) (159)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(b1(a0(a1(a1(a1(x1))))))))) (160)
and no rules could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.