Certification Problem

Input (TPDB SRS_Standard/Zantema_06/17)

The rewrite relation of the following TRS is considered.

a(a(x1)) → b(x1) (1)
a(a(a(x1))) → a(b(a(x1))) (2)
a(b(a(x1))) → b(b(b(x1))) (3)
a(a(a(a(x1)))) → a(a(b(a(a(x1))))) (4)
a(a(b(a(x1)))) → a(b(b(a(b(x1))))) (5)
a(b(a(a(x1)))) → b(a(b(b(a(x1))))) (6)
a(b(b(a(x1)))) → b(b(b(b(b(x1))))) (7)
a(a(a(a(a(x1))))) → a(a(a(b(a(a(a(x1))))))) (8)
a(a(a(b(a(x1))))) → a(a(b(b(a(a(b(x1))))))) (9)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(a(x1))))))) (10)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(b(x1))))))) (11)
a(b(a(a(a(x1))))) → b(a(a(b(b(a(a(x1))))))) (12)
a(b(a(b(a(x1))))) → b(a(b(b(b(a(b(x1))))))) (13)
a(b(b(a(a(x1))))) → b(b(a(b(b(b(a(x1))))))) (14)
a(b(b(b(a(x1))))) → b(b(b(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(x1)) (16)
b(a(a(a(x1)))) → b(a(b(a(x1)))) (17)
b(a(b(a(x1)))) → b(b(b(b(x1)))) (18)
b(a(a(a(a(x1))))) → b(a(a(b(a(a(x1)))))) (19)
b(a(a(b(a(x1))))) → b(a(b(b(a(b(x1)))))) (20)
b(a(b(a(a(x1))))) → b(b(a(b(b(a(x1)))))) (21)
b(a(b(b(a(x1))))) → b(b(b(b(b(b(x1)))))) (22)
b(a(a(a(a(a(x1)))))) → b(a(a(a(b(a(a(a(x1)))))))) (23)
b(a(a(a(b(a(x1)))))) → b(a(a(b(b(a(a(b(x1)))))))) (24)
b(a(a(b(a(a(x1)))))) → b(a(b(a(b(a(b(a(x1)))))))) (25)
b(a(a(b(b(a(x1)))))) → b(a(b(b(b(a(b(b(x1)))))))) (26)
b(a(b(a(a(a(x1)))))) → b(b(a(a(b(b(a(a(x1)))))))) (27)
b(a(b(a(b(a(x1)))))) → b(b(a(b(b(b(a(b(x1)))))))) (28)
b(a(b(b(a(a(x1)))))) → b(b(b(a(b(b(b(a(x1)))))))) (29)
b(a(b(b(b(a(x1)))))) → b(b(b(b(b(b(b(b(x1)))))))) (30)
a(a(a(x1))) → a(b(x1)) (31)
a(a(a(a(x1)))) → a(a(b(a(x1)))) (32)
a(a(b(a(x1)))) → a(b(b(b(x1)))) (33)
a(a(a(a(a(x1))))) → a(a(a(b(a(a(x1)))))) (34)
a(a(a(b(a(x1))))) → a(a(b(b(a(b(x1)))))) (35)
a(a(b(a(a(x1))))) → a(b(a(b(b(a(x1)))))) (36)
a(a(b(b(a(x1))))) → a(b(b(b(b(b(x1)))))) (37)
a(a(a(a(a(a(x1)))))) → a(a(a(a(b(a(a(a(x1)))))))) (38)
a(a(a(a(b(a(x1)))))) → a(a(a(b(b(a(a(b(x1)))))))) (39)
a(a(a(b(a(a(x1)))))) → a(a(b(a(b(a(b(a(x1)))))))) (40)
a(a(a(b(b(a(x1)))))) → a(a(b(b(b(a(b(b(x1)))))))) (41)
a(a(b(a(a(a(x1)))))) → a(b(a(a(b(b(a(a(x1)))))))) (42)
a(a(b(a(b(a(x1)))))) → a(b(a(b(b(b(a(b(x1)))))))) (43)
a(a(b(b(a(a(x1)))))) → a(b(b(a(b(b(b(a(x1)))))))) (44)
a(a(b(b(b(a(x1)))))) → a(b(b(b(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(x1)) (46)
a1(a1(a0(x1))) → a0(b0(x1)) (47)
b1(a1(a1(x1))) → b0(b1(x1)) (48)
b1(a1(a0(x1))) → b0(b0(x1)) (49)
a1(a1(a1(a1(x1)))) → a1(a0(b1(a1(x1)))) (50)
a1(a1(a1(a0(x1)))) → a1(a0(b1(a0(x1)))) (51)
b1(a1(a1(a1(x1)))) → b1(a0(b1(a1(x1)))) (52)
b1(a1(a1(a0(x1)))) → b1(a0(b1(a0(x1)))) (53)
a1(a0(b1(a1(x1)))) → a0(b0(b0(b1(x1)))) (54)
a1(a0(b1(a0(x1)))) → a0(b0(b0(b0(x1)))) (55)
b1(a0(b1(a1(x1)))) → b0(b0(b0(b1(x1)))) (56)
b1(a0(b1(a0(x1)))) → b0(b0(b0(b0(x1)))) (57)
a1(a1(a1(a1(a1(x1))))) → a1(a1(a0(b1(a1(a1(x1)))))) (58)
a1(a1(a1(a1(a0(x1))))) → a1(a1(a0(b1(a1(a0(x1)))))) (59)
b1(a1(a1(a1(a1(x1))))) → b1(a1(a0(b1(a1(a1(x1)))))) (60)
b1(a1(a1(a1(a0(x1))))) → b1(a1(a0(b1(a1(a0(x1)))))) (61)
a1(a1(a0(b1(a1(x1))))) → a1(a0(b0(b1(a0(b1(x1)))))) (62)
a1(a1(a0(b1(a0(x1))))) → a1(a0(b0(b1(a0(b0(x1)))))) (63)
b1(a1(a0(b1(a1(x1))))) → b1(a0(b0(b1(a0(b1(x1)))))) (64)
b1(a1(a0(b1(a0(x1))))) → b1(a0(b0(b1(a0(b0(x1)))))) (65)
a1(a0(b1(a1(a1(x1))))) → a0(b1(a0(b0(b1(a1(x1)))))) (66)
a1(a0(b1(a1(a0(x1))))) → a0(b1(a0(b0(b1(a0(x1)))))) (67)
b1(a0(b1(a1(a1(x1))))) → b0(b1(a0(b0(b1(a1(x1)))))) (68)
b1(a0(b1(a1(a0(x1))))) → b0(b1(a0(b0(b1(a0(x1)))))) (69)
a1(a0(b0(b1(a1(x1))))) → a0(b0(b0(b0(b0(b1(x1)))))) (70)
a1(a0(b0(b1(a0(x1))))) → a0(b0(b0(b0(b0(b0(x1)))))) (71)
b1(a0(b0(b1(a1(x1))))) → b0(b0(b0(b0(b0(b1(x1)))))) (72)
b1(a0(b0(b1(a0(x1))))) → b0(b0(b0(b0(b0(b0(x1)))))) (73)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(a0(b1(a1(a1(a1(x1)))))))) (74)
a1(a1(a1(a1(a1(a0(x1)))))) → a1(a1(a1(a0(b1(a1(a1(a0(x1)))))))) (75)
b1(a1(a1(a1(a1(a1(x1)))))) → b1(a1(a1(a0(b1(a1(a1(a1(x1)))))))) (76)
b1(a1(a1(a1(a1(a0(x1)))))) → b1(a1(a1(a0(b1(a1(a1(a0(x1)))))))) (77)
a1(a1(a1(a0(b1(a1(x1)))))) → a1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) (78)
a1(a1(a1(a0(b1(a0(x1)))))) → a1(a1(a0(b0(b1(a1(a0(b0(x1)))))))) (79)
b1(a1(a1(a0(b1(a1(x1)))))) → b1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) (80)
b1(a1(a1(a0(b1(a0(x1)))))) → b1(a1(a0(b0(b1(a1(a0(b0(x1)))))))) (81)
a1(a1(a0(b1(a1(a1(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) (82)
a1(a1(a0(b1(a1(a0(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) (83)
b1(a1(a0(b1(a1(a1(x1)))))) → 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(x1)))))))) (85)
a1(a1(a0(b0(b1(a1(x1)))))) → a1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) (86)
a1(a1(a0(b0(b1(a0(x1)))))) → a1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) (87)
b1(a1(a0(b0(b1(a1(x1)))))) → b1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) (88)
b1(a1(a0(b0(b1(a0(x1)))))) → b1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) (89)
a1(a0(b1(a1(a1(a1(x1)))))) → a0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) (90)
a1(a0(b1(a1(a1(a0(x1)))))) → a0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) (91)
b1(a0(b1(a1(a1(a1(x1)))))) → b0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) (92)
b1(a0(b1(a1(a1(a0(x1)))))) → b0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) (93)
a1(a0(b1(a0(b1(a1(x1)))))) → a0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) (94)
a1(a0(b1(a0(b1(a0(x1)))))) → a0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) (95)
b1(a0(b1(a0(b1(a1(x1)))))) → b0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) (96)
b1(a0(b1(a0(b1(a0(x1)))))) → b0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) (97)
a1(a0(b0(b1(a1(a1(x1)))))) → a0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) (98)
a1(a0(b0(b1(a1(a0(x1)))))) → a0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) (99)
b1(a0(b0(b1(a1(a1(x1)))))) → b0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) (100)
b1(a0(b0(b1(a1(a0(x1)))))) → b0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) (101)
a1(a0(b0(b0(b1(a1(x1)))))) → a0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) (102)
a1(a0(b0(b0(b1(a0(x1)))))) → a0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) (103)
b1(a0(b0(b0(b1(a1(x1)))))) → b0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) (104)
b1(a0(b0(b0(b1(a0(x1)))))) → b0(b0(b0(b0(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(x1)) (46)
a1(a1(a0(x1))) → a0(b0(x1)) (47)
b1(a1(a1(x1))) → b0(b1(x1)) (48)
b1(a1(a0(x1))) → b0(b0(x1)) (49)
a1(a1(a1(a1(x1)))) → a1(a0(b1(a1(x1)))) (50)
a1(a1(a1(a0(x1)))) → a1(a0(b1(a0(x1)))) (51)
b1(a1(a1(a1(x1)))) → b1(a0(b1(a1(x1)))) (52)
b1(a1(a1(a0(x1)))) → b1(a0(b1(a0(x1)))) (53)
a1(a0(b1(a1(x1)))) → a0(b0(b0(b1(x1)))) (54)
a1(a0(b1(a0(x1)))) → a0(b0(b0(b0(x1)))) (55)
b1(a0(b1(a1(x1)))) → b0(b0(b0(b1(x1)))) (56)
a1(a1(a1(a1(a1(x1))))) → a1(a1(a0(b1(a1(a1(x1)))))) (58)
a1(a1(a1(a1(a0(x1))))) → a1(a1(a0(b1(a1(a0(x1)))))) (59)
b1(a1(a1(a1(a1(x1))))) → b1(a1(a0(b1(a1(a1(x1)))))) (60)
b1(a1(a1(a1(a0(x1))))) → b1(a1(a0(b1(a1(a0(x1)))))) (61)
a1(a1(a0(b1(a1(x1))))) → a1(a0(b0(b1(a0(b1(x1)))))) (62)
a1(a1(a0(b1(a0(x1))))) → a1(a0(b0(b1(a0(b0(x1)))))) (63)
b1(a1(a0(b1(a1(x1))))) → b1(a0(b0(b1(a0(b1(x1)))))) (64)
b1(a1(a0(b1(a0(x1))))) → b1(a0(b0(b1(a0(b0(x1)))))) (65)
a1(a0(b1(a1(a1(x1))))) → a0(b1(a0(b0(b1(a1(x1)))))) (66)
a1(a0(b1(a1(a0(x1))))) → a0(b1(a0(b0(b1(a0(x1)))))) (67)
b1(a0(b1(a1(a1(x1))))) → b0(b1(a0(b0(b1(a1(x1)))))) (68)
b1(a0(b1(a1(a0(x1))))) → b0(b1(a0(b0(b1(a0(x1)))))) (69)
a1(a0(b0(b1(a1(x1))))) → a0(b0(b0(b0(b0(b1(x1)))))) (70)
a1(a0(b0(b1(a0(x1))))) → a0(b0(b0(b0(b0(b0(x1)))))) (71)
b1(a0(b0(b1(a1(x1))))) → b0(b0(b0(b0(b0(b1(x1)))))) (72)
a1(a1(a1(a0(b1(a1(x1)))))) → a1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) (78)
b1(a1(a1(a0(b1(a1(x1)))))) → b1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) (80)
a1(a1(a0(b1(a1(a1(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) (82)
a1(a1(a0(b1(a1(a0(x1)))))) → a1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) (83)
b1(a1(a0(b1(a1(a1(x1)))))) → 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(x1)))))))) (85)
a1(a1(a0(b0(b1(a1(x1)))))) → a1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) (86)
a1(a1(a0(b0(b1(a0(x1)))))) → a1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) (87)
b1(a1(a0(b0(b1(a1(x1)))))) → b1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) (88)
b1(a1(a0(b0(b1(a0(x1)))))) → b1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) (89)
a1(a0(b1(a1(a1(a1(x1)))))) → a0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) (90)
a1(a0(b1(a1(a1(a0(x1)))))) → a0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) (91)
a1(a0(b1(a0(b1(a1(x1)))))) → a0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) (94)
a1(a0(b1(a0(b1(a0(x1)))))) → a0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) (95)
b1(a0(b1(a0(b1(a1(x1)))))) → b0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) (96)
a1(a0(b0(b1(a1(a1(x1)))))) → a0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) (98)
a1(a0(b0(b1(a1(a0(x1)))))) → a0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) (99)
b1(a0(b0(b1(a1(a1(x1)))))) → b0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) (100)
b1(a0(b0(b1(a1(a0(x1)))))) → b0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) (101)
a1(a0(b0(b0(b1(a1(x1)))))) → a0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) (102)
a1(a0(b0(b0(b1(a0(x1)))))) → a0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) (103)
b1(a0(b0(b0(b1(a1(x1)))))) → b0(b0(b0(b0(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(b0(b0(x1)))) (106)
a0(b1(b0(a0(b1(x1))))) → b0(b0(b0(b0(b0(b0(x1)))))) (107)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (108)
a0(a1(a1(a1(a1(a1(x1)))))) → a0(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (109)
a1(a1(a1(a1(a1(b1(x1)))))) → a1(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (110)
a0(a1(a1(a1(a1(b1(x1)))))) → a0(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (111)
a0(b1(a0(a1(a1(a1(x1)))))) → b0(a0(a1(b1(b0(a0(a1(a1(x1)))))))) (112)
a0(b1(a0(a1(a1(b1(x1)))))) → b0(a0(a1(b1(b0(a0(a1(b1(x1)))))))) (113)
a1(a1(a1(b1(a0(b1(x1)))))) → a1(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (114)
a0(a1(a1(b1(a0(b1(x1)))))) → a0(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (115)
a0(b1(a0(b1(a0(b1(x1)))))) → b0(a0(b1(b0(b0(a0(b1(b0(x1)))))))) (116)
a0(b1(b0(b0(a0(b1(x1)))))) → b0(b0(b0(b0(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(a0(b1(a0(b1(x1)))))) → a0#(b1(b0(x1))) (118)
a0#(b1(a0(b1(a0(b1(x1)))))) → a0#(b1(b0(b0(a0(b1(b0(x1))))))) (119)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(a1(b1(x1))) (120)
a0#(b1(a0(a1(a1(b1(x1)))))) → a0#(a1(b1(b0(a0(a1(b1(x1))))))) (121)
a0#(b1(a0(a1(a1(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(x1)))))) (122)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(b1(b0(a0(a1(a1(x1))))))) (123)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(a1(x1))) (124)
a0#(b1(a0(a1(a1(a1(x1)))))) → a1#(b1(b0(a0(a1(a1(x1)))))) (125)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (126)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (127)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (128)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(b0(x1))))))) (129)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (130)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (131)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(a1(a1(b1(x1)))))) (132)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(a1(a1(b1(x1))))))) (133)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (134)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (135)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(a1(a1(a1(x1)))))) (136)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(a1(a1(a1(x1))))))) (137)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (138)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (139)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(b0(x1))))))) (140)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (141)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (142)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(a1(a1(b1(x1)))))) (143)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(a1(a1(b1(x1))))))) (144)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (145)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (146)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(a1(a1(a1(x1)))))) (147)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(a1(a1(a1(x1))))))) (148)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (149)

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(b0(b0(x1)))) (106)
a0(b1(b0(a0(b1(x1))))) → b0(b0(b0(b0(b0(b0(x1)))))) (107)
a1(a1(a1(a1(a1(a1(x1)))))) → a1(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (108)
a0(a1(a1(a1(a1(a1(x1)))))) → a0(a1(a1(b1(a0(a1(a1(a1(x1)))))))) (109)
a1(a1(a1(a1(a1(b1(x1)))))) → a1(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (110)
a0(a1(a1(a1(a1(b1(x1)))))) → a0(a1(a1(b1(a0(a1(a1(b1(x1)))))))) (111)
a0(b1(a0(a1(a1(a1(x1)))))) → b0(a0(a1(b1(b0(a0(a1(a1(x1)))))))) (112)
a0(b1(a0(a1(a1(b1(x1)))))) → b0(a0(a1(b1(b0(a0(a1(b1(x1)))))))) (113)
a1(a1(a1(b1(a0(b1(x1)))))) → a1(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (114)
a0(a1(a1(b1(a0(b1(x1)))))) → a0(a1(b1(b0(a0(a1(b1(b0(x1)))))))) (115)
a0(b1(a0(b1(a0(b1(x1)))))) → b0(a0(b1(b0(b0(a0(b1(b0(x1)))))))) (116)
a0(b1(b0(b0(a0(b1(x1)))))) → b0(b0(b0(b0(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#(a1(b1(x1))) (120)
a0#(b1(a0(a1(a1(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(x1)))))) (122)
a0#(b1(a0(a1(a1(a1(x1)))))) → a0#(a1(a1(x1))) (124)
a0#(b1(a0(a1(a1(a1(x1)))))) → a1#(b1(b0(a0(a1(a1(x1)))))) (125)
a0#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (126)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (128)
a0#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(b0(x1))))))) (129)
a0#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (130)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(a1(a1(b1(x1)))))) (132)
a0#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(a1(a1(b1(x1))))))) (133)
a0#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (135)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(a1(a1(a1(x1)))))) (136)
a0#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(a1(a1(a1(x1))))))) (137)
a1#(a1(a1(b1(a0(b1(x1)))))) → a0#(a1(b1(b0(x1)))) (138)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(x1))) (139)
a1#(a1(a1(b1(a0(b1(x1)))))) → a1#(b1(b0(a0(a1(b1(b0(x1))))))) (140)
a1#(a1(a1(a1(a1(b1(x1)))))) → a0#(a1(a1(b1(x1)))) (142)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(b1(a0(a1(a1(b1(x1)))))) (143)
a1#(a1(a1(a1(a1(b1(x1)))))) → a1#(a1(b1(a0(a1(a1(b1(x1))))))) (144)
a1#(a1(a1(a1(a1(a1(x1)))))) → a0#(a1(a1(a1(x1)))) (146)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(b1(a0(a1(a1(a1(x1)))))) (147)
a1#(a1(a1(a1(a1(a1(x1)))))) → a1#(a1(b1(a0(a1(a1(a1(x1))))))) (148)
and no rules could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.