Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup12)

The rewrite relation of the following TRS is considered.

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1)))))) (1)
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1)))) (2)
a(a(d(d(x1)))) → d(d(c(c(x1)))) (3)
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1)))))) (4)
d(d(c(c(x1)))) → b(b(d(d(x1)))) (5)
d(d(c(c(x1)))) → d(d(b(b(d(d(x1)))))) (6)
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1)))) (7)

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
[d(x1)] = x1 +
0
[c(x1)] = x1 +
1
[b(x1)] = x1 +
1
[a(x1)] = x1 +
1
all of the following rules can be deleted.
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1)))) (2)

1.1 Split

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

a(a(d(d(x1)))) → d(d(c(c(x1)))) (3)
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1)))))) (4)
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1)))) (7)
are deleted.

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐), a(☐)}

We obtain the transformed TRS
d(a(a(d(d(x1))))) → d(d(d(c(c(x1))))) (8)
d(b(b(b(b(b(b(x1))))))) → d(a(a(b(b(c(c(x1))))))) (9)
d(d(d(a(a(c(c(x1))))))) → d(b(b(b(b(x1))))) (10)
c(a(a(d(d(x1))))) → c(d(d(c(c(x1))))) (11)
c(b(b(b(b(b(b(x1))))))) → c(a(a(b(b(c(c(x1))))))) (12)
c(d(d(a(a(c(c(x1))))))) → c(b(b(b(b(x1))))) (13)
b(a(a(d(d(x1))))) → b(d(d(c(c(x1))))) (14)
b(b(b(b(b(b(b(x1))))))) → b(a(a(b(b(c(c(x1))))))) (15)
b(d(d(a(a(c(c(x1))))))) → b(b(b(b(b(x1))))) (16)
a(a(a(d(d(x1))))) → a(d(d(c(c(x1))))) (17)
a(b(b(b(b(b(b(x1))))))) → a(a(a(b(b(c(c(x1))))))) (18)
a(d(d(a(a(c(c(x1))))))) → a(b(b(b(b(x1))))) (19)
d(b(b(d(d(b(b(x1))))))) → d(c(c(d(d(b(b(x1))))))) (20)
d(d(d(c(c(x1))))) → d(b(b(d(d(x1))))) (21)
d(d(d(c(c(x1))))) → d(d(d(b(b(d(d(x1))))))) (22)
c(b(b(d(d(b(b(x1))))))) → c(c(c(d(d(b(b(x1))))))) (23)
c(d(d(c(c(x1))))) → c(b(b(d(d(x1))))) (24)
c(d(d(c(c(x1))))) → c(d(d(b(b(d(d(x1))))))) (25)
b(b(b(d(d(b(b(x1))))))) → b(c(c(d(d(b(b(x1))))))) (26)
b(d(d(c(c(x1))))) → b(b(b(d(d(x1))))) (27)
b(d(d(c(c(x1))))) → b(d(d(b(b(d(d(x1))))))) (28)
a(b(b(d(d(b(b(x1))))))) → a(c(c(d(d(b(b(x1))))))) (29)
a(d(d(c(c(x1))))) → a(b(b(d(d(x1))))) (30)
a(d(d(c(c(x1))))) → a(d(d(b(b(d(d(x1))))))) (31)

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

[d(x1)] = 4x1 + 0
[c(x1)] = 4x1 + 1
[b(x1)] = 4x1 + 2
[a(x1)] = 4x1 + 3

We obtain the labeled TRS
b3(a3(a0(d0(d2(x1))))) → b0(d0(d1(c1(c2(x1))))) (32)
b3(a3(a0(d0(d0(x1))))) → b0(d0(d1(c1(c0(x1))))) (33)
b3(a3(a0(d0(d1(x1))))) → b0(d0(d1(c1(c1(x1))))) (34)
b3(a3(a0(d0(d3(x1))))) → b0(d0(d1(c1(c3(x1))))) (35)
d3(a3(a0(d0(d2(x1))))) → d0(d0(d1(c1(c2(x1))))) (36)
d3(a3(a0(d0(d0(x1))))) → d0(d0(d1(c1(c0(x1))))) (37)
d3(a3(a0(d0(d1(x1))))) → d0(d0(d1(c1(c1(x1))))) (38)
d3(a3(a0(d0(d3(x1))))) → d0(d0(d1(c1(c3(x1))))) (39)
c3(a3(a0(d0(d2(x1))))) → c0(d0(d1(c1(c2(x1))))) (40)
c3(a3(a0(d0(d0(x1))))) → c0(d0(d1(c1(c0(x1))))) (41)
c3(a3(a0(d0(d1(x1))))) → c0(d0(d1(c1(c1(x1))))) (42)
c3(a3(a0(d0(d3(x1))))) → c0(d0(d1(c1(c3(x1))))) (43)
a3(a3(a0(d0(d2(x1))))) → a0(d0(d1(c1(c2(x1))))) (44)
a3(a3(a0(d0(d0(x1))))) → a0(d0(d1(c1(c0(x1))))) (45)
a3(a3(a0(d0(d1(x1))))) → a0(d0(d1(c1(c1(x1))))) (46)
a3(a3(a0(d0(d3(x1))))) → a0(d0(d1(c1(c3(x1))))) (47)
b2(b2(b2(b2(b2(b2(b2(x1))))))) → b3(a3(a2(b2(b1(c1(c2(x1))))))) (48)
b2(b2(b2(b2(b2(b2(b0(x1))))))) → b3(a3(a2(b2(b1(c1(c0(x1))))))) (49)
b2(b2(b2(b2(b2(b2(b1(x1))))))) → b3(a3(a2(b2(b1(c1(c1(x1))))))) (50)
b2(b2(b2(b2(b2(b2(b3(x1))))))) → b3(a3(a2(b2(b1(c1(c3(x1))))))) (51)
d2(b2(b2(b2(b2(b2(b2(x1))))))) → d3(a3(a2(b2(b1(c1(c2(x1))))))) (52)
d2(b2(b2(b2(b2(b2(b0(x1))))))) → d3(a3(a2(b2(b1(c1(c0(x1))))))) (53)
d2(b2(b2(b2(b2(b2(b1(x1))))))) → d3(a3(a2(b2(b1(c1(c1(x1))))))) (54)
d2(b2(b2(b2(b2(b2(b3(x1))))))) → d3(a3(a2(b2(b1(c1(c3(x1))))))) (55)
c2(b2(b2(b2(b2(b2(b2(x1))))))) → c3(a3(a2(b2(b1(c1(c2(x1))))))) (56)
c2(b2(b2(b2(b2(b2(b0(x1))))))) → c3(a3(a2(b2(b1(c1(c0(x1))))))) (57)
c2(b2(b2(b2(b2(b2(b1(x1))))))) → c3(a3(a2(b2(b1(c1(c1(x1))))))) (58)
c2(b2(b2(b2(b2(b2(b3(x1))))))) → c3(a3(a2(b2(b1(c1(c3(x1))))))) (59)
a2(b2(b2(b2(b2(b2(b2(x1))))))) → a3(a3(a2(b2(b1(c1(c2(x1))))))) (60)
a2(b2(b2(b2(b2(b2(b0(x1))))))) → a3(a3(a2(b2(b1(c1(c0(x1))))))) (61)
a2(b2(b2(b2(b2(b2(b1(x1))))))) → a3(a3(a2(b2(b1(c1(c1(x1))))))) (62)
a2(b2(b2(b2(b2(b2(b3(x1))))))) → a3(a3(a2(b2(b1(c1(c3(x1))))))) (63)
b0(d0(d3(a3(a1(c1(c2(x1))))))) → b2(b2(b2(b2(b2(x1))))) (64)
b0(d0(d3(a3(a1(c1(c0(x1))))))) → b2(b2(b2(b2(b0(x1))))) (65)
b0(d0(d3(a3(a1(c1(c1(x1))))))) → b2(b2(b2(b2(b1(x1))))) (66)
b0(d0(d3(a3(a1(c1(c3(x1))))))) → b2(b2(b2(b2(b3(x1))))) (67)
d0(d0(d3(a3(a1(c1(c2(x1))))))) → d2(b2(b2(b2(b2(x1))))) (68)
d0(d0(d3(a3(a1(c1(c0(x1))))))) → d2(b2(b2(b2(b0(x1))))) (69)
d0(d0(d3(a3(a1(c1(c1(x1))))))) → d2(b2(b2(b2(b1(x1))))) (70)
d0(d0(d3(a3(a1(c1(c3(x1))))))) → d2(b2(b2(b2(b3(x1))))) (71)
c0(d0(d3(a3(a1(c1(c2(x1))))))) → c2(b2(b2(b2(b2(x1))))) (72)
c0(d0(d3(a3(a1(c1(c0(x1))))))) → c2(b2(b2(b2(b0(x1))))) (73)
c0(d0(d3(a3(a1(c1(c1(x1))))))) → c2(b2(b2(b2(b1(x1))))) (74)
c0(d0(d3(a3(a1(c1(c3(x1))))))) → c2(b2(b2(b2(b3(x1))))) (75)
a0(d0(d3(a3(a1(c1(c2(x1))))))) → a2(b2(b2(b2(b2(x1))))) (76)
a0(d0(d3(a3(a1(c1(c0(x1))))))) → a2(b2(b2(b2(b0(x1))))) (77)
a0(d0(d3(a3(a1(c1(c1(x1))))))) → a2(b2(b2(b2(b1(x1))))) (78)
a0(d0(d3(a3(a1(c1(c3(x1))))))) → a2(b2(b2(b2(b3(x1))))) (79)
b2(b2(b0(d0(d2(b2(b2(x1))))))) → b1(c1(c0(d0(d2(b2(b2(x1))))))) (80)
b2(b2(b0(d0(d2(b2(b0(x1))))))) → b1(c1(c0(d0(d2(b2(b0(x1))))))) (81)
b2(b2(b0(d0(d2(b2(b1(x1))))))) → b1(c1(c0(d0(d2(b2(b1(x1))))))) (82)
b2(b2(b0(d0(d2(b2(b3(x1))))))) → b1(c1(c0(d0(d2(b2(b3(x1))))))) (83)
d2(b2(b0(d0(d2(b2(b2(x1))))))) → d1(c1(c0(d0(d2(b2(b2(x1))))))) (84)
d2(b2(b0(d0(d2(b2(b0(x1))))))) → d1(c1(c0(d0(d2(b2(b0(x1))))))) (85)
d2(b2(b0(d0(d2(b2(b1(x1))))))) → d1(c1(c0(d0(d2(b2(b1(x1))))))) (86)
d2(b2(b0(d0(d2(b2(b3(x1))))))) → d1(c1(c0(d0(d2(b2(b3(x1))))))) (87)
c2(b2(b0(d0(d2(b2(b2(x1))))))) → c1(c1(c0(d0(d2(b2(b2(x1))))))) (88)
c2(b2(b0(d0(d2(b2(b0(x1))))))) → c1(c1(c0(d0(d2(b2(b0(x1))))))) (89)
c2(b2(b0(d0(d2(b2(b1(x1))))))) → c1(c1(c0(d0(d2(b2(b1(x1))))))) (90)
c2(b2(b0(d0(d2(b2(b3(x1))))))) → c1(c1(c0(d0(d2(b2(b3(x1))))))) (91)
a2(b2(b0(d0(d2(b2(b2(x1))))))) → a1(c1(c0(d0(d2(b2(b2(x1))))))) (92)
a2(b2(b0(d0(d2(b2(b0(x1))))))) → a1(c1(c0(d0(d2(b2(b0(x1))))))) (93)
a2(b2(b0(d0(d2(b2(b1(x1))))))) → a1(c1(c0(d0(d2(b2(b1(x1))))))) (94)
a2(b2(b0(d0(d2(b2(b3(x1))))))) → a1(c1(c0(d0(d2(b2(b3(x1))))))) (95)
b0(d0(d1(c1(c2(x1))))) → b2(b2(b0(d0(d2(x1))))) (96)
b0(d0(d1(c1(c0(x1))))) → b2(b2(b0(d0(d0(x1))))) (97)
b0(d0(d1(c1(c1(x1))))) → b2(b2(b0(d0(d1(x1))))) (98)
b0(d0(d1(c1(c3(x1))))) → b2(b2(b0(d0(d3(x1))))) (99)
d0(d0(d1(c1(c2(x1))))) → d2(b2(b0(d0(d2(x1))))) (100)
d0(d0(d1(c1(c0(x1))))) → d2(b2(b0(d0(d0(x1))))) (101)
d0(d0(d1(c1(c1(x1))))) → d2(b2(b0(d0(d1(x1))))) (102)
d0(d0(d1(c1(c3(x1))))) → d2(b2(b0(d0(d3(x1))))) (103)
c0(d0(d1(c1(c2(x1))))) → c2(b2(b0(d0(d2(x1))))) (104)
c0(d0(d1(c1(c0(x1))))) → c2(b2(b0(d0(d0(x1))))) (105)
c0(d0(d1(c1(c1(x1))))) → c2(b2(b0(d0(d1(x1))))) (106)
c0(d0(d1(c1(c3(x1))))) → c2(b2(b0(d0(d3(x1))))) (107)
a0(d0(d1(c1(c2(x1))))) → a2(b2(b0(d0(d2(x1))))) (108)
a0(d0(d1(c1(c0(x1))))) → a2(b2(b0(d0(d0(x1))))) (109)
a0(d0(d1(c1(c1(x1))))) → a2(b2(b0(d0(d1(x1))))) (110)
a0(d0(d1(c1(c3(x1))))) → a2(b2(b0(d0(d3(x1))))) (111)
b0(d0(d1(c1(c2(x1))))) → b0(d0(d2(b2(b0(d0(d2(x1))))))) (112)
b0(d0(d1(c1(c0(x1))))) → b0(d0(d2(b2(b0(d0(d0(x1))))))) (113)
b0(d0(d1(c1(c1(x1))))) → b0(d0(d2(b2(b0(d0(d1(x1))))))) (114)
b0(d0(d1(c1(c3(x1))))) → b0(d0(d2(b2(b0(d0(d3(x1))))))) (115)
d0(d0(d1(c1(c2(x1))))) → d0(d0(d2(b2(b0(d0(d2(x1))))))) (116)
d0(d0(d1(c1(c0(x1))))) → d0(d0(d2(b2(b0(d0(d0(x1))))))) (117)
d0(d0(d1(c1(c1(x1))))) → d0(d0(d2(b2(b0(d0(d1(x1))))))) (118)
d0(d0(d1(c1(c3(x1))))) → d0(d0(d2(b2(b0(d0(d3(x1))))))) (119)
c0(d0(d1(c1(c2(x1))))) → c0(d0(d2(b2(b0(d0(d2(x1))))))) (120)
c0(d0(d1(c1(c0(x1))))) → c0(d0(d2(b2(b0(d0(d0(x1))))))) (121)
c0(d0(d1(c1(c1(x1))))) → c0(d0(d2(b2(b0(d0(d1(x1))))))) (122)
c0(d0(d1(c1(c3(x1))))) → c0(d0(d2(b2(b0(d0(d3(x1))))))) (123)
a0(d0(d1(c1(c2(x1))))) → a0(d0(d2(b2(b0(d0(d2(x1))))))) (124)
a0(d0(d1(c1(c0(x1))))) → a0(d0(d2(b2(b0(d0(d0(x1))))))) (125)
a0(d0(d1(c1(c1(x1))))) → a0(d0(d2(b2(b0(d0(d1(x1))))))) (126)
a0(d0(d1(c1(c3(x1))))) → a0(d0(d2(b2(b0(d0(d3(x1))))))) (127)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
0
[d1(x1)] = x1 +
1
[d2(x1)] = x1 +
0
[d3(x1)] = x1 +
1
[c0(x1)] = x1 +
0
[c1(x1)] = x1 +
1
[c2(x1)] = x1 +
0
[c3(x1)] = x1 +
1
[b0(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
1
[b3(x1)] = x1 +
1
[a0(x1)] = x1 +
2
[a1(x1)] = x1 +
1
[a2(x1)] = x1 +
0
[a3(x1)] = x1 +
1
all of the following rules can be deleted.
b3(a3(a0(d0(d2(x1))))) → b0(d0(d1(c1(c2(x1))))) (32)
b3(a3(a0(d0(d0(x1))))) → b0(d0(d1(c1(c0(x1))))) (33)
b3(a3(a0(d0(d1(x1))))) → b0(d0(d1(c1(c1(x1))))) (34)
b3(a3(a0(d0(d3(x1))))) → b0(d0(d1(c1(c3(x1))))) (35)
d3(a3(a0(d0(d2(x1))))) → d0(d0(d1(c1(c2(x1))))) (36)
d3(a3(a0(d0(d0(x1))))) → d0(d0(d1(c1(c0(x1))))) (37)
d3(a3(a0(d0(d1(x1))))) → d0(d0(d1(c1(c1(x1))))) (38)
d3(a3(a0(d0(d3(x1))))) → d0(d0(d1(c1(c3(x1))))) (39)
c3(a3(a0(d0(d2(x1))))) → c0(d0(d1(c1(c2(x1))))) (40)
c3(a3(a0(d0(d0(x1))))) → c0(d0(d1(c1(c0(x1))))) (41)
c3(a3(a0(d0(d1(x1))))) → c0(d0(d1(c1(c1(x1))))) (42)
c3(a3(a0(d0(d3(x1))))) → c0(d0(d1(c1(c3(x1))))) (43)
b2(b2(b2(b2(b2(b2(b2(x1))))))) → b3(a3(a2(b2(b1(c1(c2(x1))))))) (48)
b2(b2(b2(b2(b2(b2(b0(x1))))))) → b3(a3(a2(b2(b1(c1(c0(x1))))))) (49)
b2(b2(b2(b2(b2(b2(b1(x1))))))) → b3(a3(a2(b2(b1(c1(c1(x1))))))) (50)
b2(b2(b2(b2(b2(b2(b3(x1))))))) → b3(a3(a2(b2(b1(c1(c3(x1))))))) (51)
d2(b2(b2(b2(b2(b2(b2(x1))))))) → d3(a3(a2(b2(b1(c1(c2(x1))))))) (52)
d2(b2(b2(b2(b2(b2(b0(x1))))))) → d3(a3(a2(b2(b1(c1(c0(x1))))))) (53)
d2(b2(b2(b2(b2(b2(b3(x1))))))) → d3(a3(a2(b2(b1(c1(c3(x1))))))) (55)
c2(b2(b2(b2(b2(b2(b2(x1))))))) → c3(a3(a2(b2(b1(c1(c2(x1))))))) (56)
c2(b2(b2(b2(b2(b2(b0(x1))))))) → c3(a3(a2(b2(b1(c1(c0(x1))))))) (57)
c2(b2(b2(b2(b2(b2(b3(x1))))))) → c3(a3(a2(b2(b1(c1(c3(x1))))))) (59)
a2(b2(b2(b2(b2(b2(b2(x1))))))) → a3(a3(a2(b2(b1(c1(c2(x1))))))) (60)
a2(b2(b2(b2(b2(b2(b0(x1))))))) → a3(a3(a2(b2(b1(c1(c0(x1))))))) (61)
a2(b2(b2(b2(b2(b2(b3(x1))))))) → a3(a3(a2(b2(b1(c1(c3(x1))))))) (63)
b0(d0(d3(a3(a1(c1(c1(x1))))))) → b2(b2(b2(b2(b1(x1))))) (66)
b0(d0(d3(a3(a1(c1(c3(x1))))))) → b2(b2(b2(b2(b3(x1))))) (67)
d0(d0(d3(a3(a1(c1(c1(x1))))))) → d2(b2(b2(b2(b1(x1))))) (70)
d0(d0(d3(a3(a1(c1(c3(x1))))))) → d2(b2(b2(b2(b3(x1))))) (71)
c0(d0(d3(a3(a1(c1(c1(x1))))))) → c2(b2(b2(b2(b1(x1))))) (74)
c0(d0(d3(a3(a1(c1(c3(x1))))))) → c2(b2(b2(b2(b3(x1))))) (75)
a0(d0(d3(a3(a1(c1(c2(x1))))))) → a2(b2(b2(b2(b2(x1))))) (76)
a0(d0(d3(a3(a1(c1(c0(x1))))))) → a2(b2(b2(b2(b0(x1))))) (77)
a0(d0(d3(a3(a1(c1(c1(x1))))))) → a2(b2(b2(b2(b1(x1))))) (78)
a0(d0(d3(a3(a1(c1(c3(x1))))))) → a2(b2(b2(b2(b3(x1))))) (79)
b2(b2(b0(d0(d2(b2(b2(x1))))))) → b1(c1(c0(d0(d2(b2(b2(x1))))))) (80)
b2(b2(b0(d0(d2(b2(b0(x1))))))) → b1(c1(c0(d0(d2(b2(b0(x1))))))) (81)
b2(b2(b0(d0(d2(b2(b1(x1))))))) → b1(c1(c0(d0(d2(b2(b1(x1))))))) (82)
b2(b2(b0(d0(d2(b2(b3(x1))))))) → b1(c1(c0(d0(d2(b2(b3(x1))))))) (83)
a0(d0(d1(c1(c2(x1))))) → a2(b2(b0(d0(d2(x1))))) (108)
a0(d0(d1(c1(c0(x1))))) → a2(b2(b0(d0(d0(x1))))) (109)
a0(d0(d1(c1(c1(x1))))) → a2(b2(b0(d0(d1(x1))))) (110)
a0(d0(d1(c1(c3(x1))))) → a2(b2(b0(d0(d3(x1))))) (111)

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[d0(x1)] =
1
· x1 +
0
[d1(x1)] =
1
· x1 +
0
[d2(x1)] =
1
· x1 +
0
[d3(x1)] =
1
· x1 +
0
[c0(x1)] =
2
· x1 +
0
[c1(x1)] =
2
· x1 +
0
[c2(x1)] =
2
· x1 +
0
[c3(x1)] =
2
· x1 +
0
[b0(x1)] =
2
· x1 +
0
[b1(x1)] =
1
· x1 +
1
[b2(x1)] =
2
· x1 +
0
[b3(x1)] =
2
· x1 +
1
[a0(x1)] =
2
· x1 +
1
[a1(x1)] =
2
· x1 +
0
[a2(x1)] =
2
· x1 +
1
[a3(x1)] =
2
· x1 +
1
all of the following rules can be deleted.
a3(a3(a0(d0(d2(x1))))) → a0(d0(d1(c1(c2(x1))))) (44)
a3(a3(a0(d0(d0(x1))))) → a0(d0(d1(c1(c0(x1))))) (45)
a3(a3(a0(d0(d1(x1))))) → a0(d0(d1(c1(c1(x1))))) (46)
a3(a3(a0(d0(d3(x1))))) → a0(d0(d1(c1(c3(x1))))) (47)
d2(b2(b2(b2(b2(b2(b1(x1))))))) → d3(a3(a2(b2(b1(c1(c1(x1))))))) (54)
c2(b2(b2(b2(b2(b2(b1(x1))))))) → c3(a3(a2(b2(b1(c1(c1(x1))))))) (58)
a2(b2(b2(b2(b2(b2(b1(x1))))))) → a3(a3(a2(b2(b1(c1(c1(x1))))))) (62)
b0(d0(d3(a3(a1(c1(c2(x1))))))) → b2(b2(b2(b2(b2(x1))))) (64)
b0(d0(d3(a3(a1(c1(c0(x1))))))) → b2(b2(b2(b2(b0(x1))))) (65)
d0(d0(d3(a3(a1(c1(c2(x1))))))) → d2(b2(b2(b2(b2(x1))))) (68)
d0(d0(d3(a3(a1(c1(c0(x1))))))) → d2(b2(b2(b2(b0(x1))))) (69)
c0(d0(d3(a3(a1(c1(c2(x1))))))) → c2(b2(b2(b2(b2(x1))))) (72)
c0(d0(d3(a3(a1(c1(c0(x1))))))) → c2(b2(b2(b2(b0(x1))))) (73)
a2(b2(b0(d0(d2(b2(b2(x1))))))) → a1(c1(c0(d0(d2(b2(b2(x1))))))) (92)
a2(b2(b0(d0(d2(b2(b0(x1))))))) → a1(c1(c0(d0(d2(b2(b0(x1))))))) (93)
a2(b2(b0(d0(d2(b2(b1(x1))))))) → a1(c1(c0(d0(d2(b2(b1(x1))))))) (94)
a2(b2(b0(d0(d2(b2(b3(x1))))))) → a1(c1(c0(d0(d2(b2(b3(x1))))))) (95)

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
0
[d1(x1)] = x1 +
1
[d2(x1)] = x1 +
1
[d3(x1)] = x1 +
0
[c0(x1)] = x1 +
0
[c1(x1)] = x1 +
1
[c2(x1)] = x1 +
1
[c3(x1)] = x1 +
1
[b0(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[b3(x1)] = x1 +
0
[a0(x1)] = x1 +
0
all of the following rules can be deleted.
b0(d0(d1(c1(c2(x1))))) → b2(b2(b0(d0(d2(x1))))) (96)
b0(d0(d1(c1(c0(x1))))) → b2(b2(b0(d0(d0(x1))))) (97)
b0(d0(d1(c1(c1(x1))))) → b2(b2(b0(d0(d1(x1))))) (98)
b0(d0(d1(c1(c3(x1))))) → b2(b2(b0(d0(d3(x1))))) (99)
d0(d0(d1(c1(c3(x1))))) → d2(b2(b0(d0(d3(x1))))) (103)
c0(d0(d1(c1(c3(x1))))) → c2(b2(b0(d0(d3(x1))))) (107)
b0(d0(d1(c1(c3(x1))))) → b0(d0(d2(b2(b0(d0(d3(x1))))))) (115)
d0(d0(d1(c1(c3(x1))))) → d0(d0(d2(b2(b0(d0(d3(x1))))))) (119)
c0(d0(d1(c1(c3(x1))))) → c0(d0(d2(b2(b0(d0(d3(x1))))))) (123)
a0(d0(d1(c1(c3(x1))))) → a0(d0(d2(b2(b0(d0(d3(x1))))))) (127)

1.1.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

d(d(c(c(x1)))) → d(d(b(b(d(d(x1)))))) (6)
are deleted.

1.1.2.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐)}

We obtain the transformed TRS
d(d(d(c(c(x1))))) → d(d(d(b(b(d(d(x1))))))) (22)
c(d(d(c(c(x1))))) → c(d(d(b(b(d(d(x1))))))) (25)
b(d(d(c(c(x1))))) → b(d(d(b(b(d(d(x1))))))) (28)
d(b(b(d(d(b(b(x1))))))) → d(c(c(d(d(b(b(x1))))))) (20)
d(d(d(c(c(x1))))) → d(b(b(d(d(x1))))) (21)
c(b(b(d(d(b(b(x1))))))) → c(c(c(d(d(b(b(x1))))))) (23)
c(d(d(c(c(x1))))) → c(b(b(d(d(x1))))) (24)
b(b(b(d(d(b(b(x1))))))) → b(c(c(d(d(b(b(x1))))))) (26)
b(d(d(c(c(x1))))) → b(b(b(d(d(x1))))) (27)

1.1.2.1.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐)}

We obtain the transformed TRS
d(d(d(d(c(c(x1)))))) → d(d(d(d(b(b(d(d(x1)))))))) (128)
d(c(d(d(c(c(x1)))))) → d(c(d(d(b(b(d(d(x1)))))))) (129)
d(b(d(d(c(c(x1)))))) → d(b(d(d(b(b(d(d(x1)))))))) (130)
c(d(d(d(c(c(x1)))))) → c(d(d(d(b(b(d(d(x1)))))))) (131)
c(c(d(d(c(c(x1)))))) → c(c(d(d(b(b(d(d(x1)))))))) (132)
c(b(d(d(c(c(x1)))))) → c(b(d(d(b(b(d(d(x1)))))))) (133)
b(d(d(d(c(c(x1)))))) → b(d(d(d(b(b(d(d(x1)))))))) (134)
b(c(d(d(c(c(x1)))))) → b(c(d(d(b(b(d(d(x1)))))))) (135)
b(b(d(d(c(c(x1)))))) → b(b(d(d(b(b(d(d(x1)))))))) (136)
d(d(b(b(d(d(b(b(x1)))))))) → d(d(c(c(d(d(b(b(x1)))))))) (137)
d(d(d(d(c(c(x1)))))) → d(d(b(b(d(d(x1)))))) (138)
d(c(b(b(d(d(b(b(x1)))))))) → d(c(c(c(d(d(b(b(x1)))))))) (139)
d(c(d(d(c(c(x1)))))) → d(c(b(b(d(d(x1)))))) (140)
d(b(b(b(d(d(b(b(x1)))))))) → d(b(c(c(d(d(b(b(x1)))))))) (141)
d(b(d(d(c(c(x1)))))) → d(b(b(b(d(d(x1)))))) (142)
c(d(b(b(d(d(b(b(x1)))))))) → c(d(c(c(d(d(b(b(x1)))))))) (143)
c(d(d(d(c(c(x1)))))) → c(d(b(b(d(d(x1)))))) (144)
c(c(b(b(d(d(b(b(x1)))))))) → c(c(c(c(d(d(b(b(x1)))))))) (145)
c(c(d(d(c(c(x1)))))) → c(c(b(b(d(d(x1)))))) (146)
c(b(b(b(d(d(b(b(x1)))))))) → c(b(c(c(d(d(b(b(x1)))))))) (147)
c(b(d(d(c(c(x1)))))) → c(b(b(b(d(d(x1)))))) (148)
b(d(b(b(d(d(b(b(x1)))))))) → b(d(c(c(d(d(b(b(x1)))))))) (149)
b(d(d(d(c(c(x1)))))) → b(d(b(b(d(d(x1)))))) (150)
b(c(b(b(d(d(b(b(x1)))))))) → b(c(c(c(d(d(b(b(x1)))))))) (151)
b(c(d(d(c(c(x1)))))) → b(c(b(b(d(d(x1)))))) (152)
b(b(b(b(d(d(b(b(x1)))))))) → b(b(c(c(d(d(b(b(x1)))))))) (153)
b(b(d(d(c(c(x1)))))) → b(b(b(b(d(d(x1)))))) (154)

1.1.2.1.1.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐)}

We obtain the transformed TRS
d(d(d(d(d(c(c(x1))))))) → d(d(d(d(d(b(b(d(d(x1))))))))) (155)
d(d(c(d(d(c(c(x1))))))) → d(d(c(d(d(b(b(d(d(x1))))))))) (156)
d(d(b(d(d(c(c(x1))))))) → d(d(b(d(d(b(b(d(d(x1))))))))) (157)
d(c(d(d(d(c(c(x1))))))) → d(c(d(d(d(b(b(d(d(x1))))))))) (158)
d(c(c(d(d(c(c(x1))))))) → d(c(c(d(d(b(b(d(d(x1))))))))) (159)
d(c(b(d(d(c(c(x1))))))) → d(c(b(d(d(b(b(d(d(x1))))))))) (160)
d(b(d(d(d(c(c(x1))))))) → d(b(d(d(d(b(b(d(d(x1))))))))) (161)
d(b(c(d(d(c(c(x1))))))) → d(b(c(d(d(b(b(d(d(x1))))))))) (162)
d(b(b(d(d(c(c(x1))))))) → d(b(b(d(d(b(b(d(d(x1))))))))) (163)
c(d(d(d(d(c(c(x1))))))) → c(d(d(d(d(b(b(d(d(x1))))))))) (164)
c(d(c(d(d(c(c(x1))))))) → c(d(c(d(d(b(b(d(d(x1))))))))) (165)
c(d(b(d(d(c(c(x1))))))) → c(d(b(d(d(b(b(d(d(x1))))))))) (166)
c(c(d(d(d(c(c(x1))))))) → c(c(d(d(d(b(b(d(d(x1))))))))) (167)
c(c(c(d(d(c(c(x1))))))) → c(c(c(d(d(b(b(d(d(x1))))))))) (168)
c(c(b(d(d(c(c(x1))))))) → c(c(b(d(d(b(b(d(d(x1))))))))) (169)
c(b(d(d(d(c(c(x1))))))) → c(b(d(d(d(b(b(d(d(x1))))))))) (170)
c(b(c(d(d(c(c(x1))))))) → c(b(c(d(d(b(b(d(d(x1))))))))) (171)
c(b(b(d(d(c(c(x1))))))) → c(b(b(d(d(b(b(d(d(x1))))))))) (172)
b(d(d(d(d(c(c(x1))))))) → b(d(d(d(d(b(b(d(d(x1))))))))) (173)
b(d(c(d(d(c(c(x1))))))) → b(d(c(d(d(b(b(d(d(x1))))))))) (174)
b(d(b(d(d(c(c(x1))))))) → b(d(b(d(d(b(b(d(d(x1))))))))) (175)
b(c(d(d(d(c(c(x1))))))) → b(c(d(d(d(b(b(d(d(x1))))))))) (176)
b(c(c(d(d(c(c(x1))))))) → b(c(c(d(d(b(b(d(d(x1))))))))) (177)
b(c(b(d(d(c(c(x1))))))) → b(c(b(d(d(b(b(d(d(x1))))))))) (178)
b(b(d(d(d(c(c(x1))))))) → b(b(d(d(d(b(b(d(d(x1))))))))) (179)
b(b(c(d(d(c(c(x1))))))) → b(b(c(d(d(b(b(d(d(x1))))))))) (180)
b(b(b(d(d(c(c(x1))))))) → b(b(b(d(d(b(b(d(d(x1))))))))) (181)
d(d(d(b(b(d(d(b(b(x1))))))))) → d(d(d(c(c(d(d(b(b(x1))))))))) (182)
d(d(d(d(d(c(c(x1))))))) → d(d(d(b(b(d(d(x1))))))) (183)
d(d(c(b(b(d(d(b(b(x1))))))))) → d(d(c(c(c(d(d(b(b(x1))))))))) (184)
d(d(c(d(d(c(c(x1))))))) → d(d(c(b(b(d(d(x1))))))) (185)
d(d(b(b(b(d(d(b(b(x1))))))))) → d(d(b(c(c(d(d(b(b(x1))))))))) (186)
d(d(b(d(d(c(c(x1))))))) → d(d(b(b(b(d(d(x1))))))) (187)
d(c(d(b(b(d(d(b(b(x1))))))))) → d(c(d(c(c(d(d(b(b(x1))))))))) (188)
d(c(d(d(d(c(c(x1))))))) → d(c(d(b(b(d(d(x1))))))) (189)
d(c(c(b(b(d(d(b(b(x1))))))))) → d(c(c(c(c(d(d(b(b(x1))))))))) (190)
d(c(c(d(d(c(c(x1))))))) → d(c(c(b(b(d(d(x1))))))) (191)
d(c(b(b(b(d(d(b(b(x1))))))))) → d(c(b(c(c(d(d(b(b(x1))))))))) (192)
d(c(b(d(d(c(c(x1))))))) → d(c(b(b(b(d(d(x1))))))) (193)
d(b(d(b(b(d(d(b(b(x1))))))))) → d(b(d(c(c(d(d(b(b(x1))))))))) (194)
d(b(d(d(d(c(c(x1))))))) → d(b(d(b(b(d(d(x1))))))) (195)
d(b(c(b(b(d(d(b(b(x1))))))))) → d(b(c(c(c(d(d(b(b(x1))))))))) (196)
d(b(c(d(d(c(c(x1))))))) → d(b(c(b(b(d(d(x1))))))) (197)
d(b(b(b(b(d(d(b(b(x1))))))))) → d(b(b(c(c(d(d(b(b(x1))))))))) (198)
d(b(b(d(d(c(c(x1))))))) → d(b(b(b(b(d(d(x1))))))) (199)
c(d(d(b(b(d(d(b(b(x1))))))))) → c(d(d(c(c(d(d(b(b(x1))))))))) (200)
c(d(d(d(d(c(c(x1))))))) → c(d(d(b(b(d(d(x1))))))) (201)
c(d(c(b(b(d(d(b(b(x1))))))))) → c(d(c(c(c(d(d(b(b(x1))))))))) (202)
c(d(c(d(d(c(c(x1))))))) → c(d(c(b(b(d(d(x1))))))) (203)
c(d(b(b(b(d(d(b(b(x1))))))))) → c(d(b(c(c(d(d(b(b(x1))))))))) (204)
c(d(b(d(d(c(c(x1))))))) → c(d(b(b(b(d(d(x1))))))) (205)
c(c(d(b(b(d(d(b(b(x1))))))))) → c(c(d(c(c(d(d(b(b(x1))))))))) (206)
c(c(d(d(d(c(c(x1))))))) → c(c(d(b(b(d(d(x1))))))) (207)
c(c(c(b(b(d(d(b(b(x1))))))))) → c(c(c(c(c(d(d(b(b(x1))))))))) (208)
c(c(c(d(d(c(c(x1))))))) → c(c(c(b(b(d(d(x1))))))) (209)
c(c(b(b(b(d(d(b(b(x1))))))))) → c(c(b(c(c(d(d(b(b(x1))))))))) (210)
c(c(b(d(d(c(c(x1))))))) → c(c(b(b(b(d(d(x1))))))) (211)
c(b(d(b(b(d(d(b(b(x1))))))))) → c(b(d(c(c(d(d(b(b(x1))))))))) (212)
c(b(d(d(d(c(c(x1))))))) → c(b(d(b(b(d(d(x1))))))) (213)
c(b(c(b(b(d(d(b(b(x1))))))))) → c(b(c(c(c(d(d(b(b(x1))))))))) (214)
c(b(c(d(d(c(c(x1))))))) → c(b(c(b(b(d(d(x1))))))) (215)
c(b(b(b(b(d(d(b(b(x1))))))))) → c(b(b(c(c(d(d(b(b(x1))))))))) (216)
c(b(b(d(d(c(c(x1))))))) → c(b(b(b(b(d(d(x1))))))) (217)
b(d(d(b(b(d(d(b(b(x1))))))))) → b(d(d(c(c(d(d(b(b(x1))))))))) (218)
b(d(d(d(d(c(c(x1))))))) → b(d(d(b(b(d(d(x1))))))) (219)
b(d(c(b(b(d(d(b(b(x1))))))))) → b(d(c(c(c(d(d(b(b(x1))))))))) (220)
b(d(c(d(d(c(c(x1))))))) → b(d(c(b(b(d(d(x1))))))) (221)
b(d(b(b(b(d(d(b(b(x1))))))))) → b(d(b(c(c(d(d(b(b(x1))))))))) (222)
b(d(b(d(d(c(c(x1))))))) → b(d(b(b(b(d(d(x1))))))) (223)
b(c(d(b(b(d(d(b(b(x1))))))))) → b(c(d(c(c(d(d(b(b(x1))))))))) (224)
b(c(d(d(d(c(c(x1))))))) → b(c(d(b(b(d(d(x1))))))) (225)
b(c(c(b(b(d(d(b(b(x1))))))))) → b(c(c(c(c(d(d(b(b(x1))))))))) (226)
b(c(c(d(d(c(c(x1))))))) → b(c(c(b(b(d(d(x1))))))) (227)
b(c(b(b(b(d(d(b(b(x1))))))))) → b(c(b(c(c(d(d(b(b(x1))))))))) (228)
b(c(b(d(d(c(c(x1))))))) → b(c(b(b(b(d(d(x1))))))) (229)
b(b(d(b(b(d(d(b(b(x1))))))))) → b(b(d(c(c(d(d(b(b(x1))))))))) (230)
b(b(d(d(d(c(c(x1))))))) → b(b(d(b(b(d(d(x1))))))) (231)
b(b(c(b(b(d(d(b(b(x1))))))))) → b(b(c(c(c(d(d(b(b(x1))))))))) (232)
b(b(c(d(d(c(c(x1))))))) → b(b(c(b(b(d(d(x1))))))) (233)
b(b(b(b(b(d(d(b(b(x1))))))))) → b(b(b(c(c(d(d(b(b(x1))))))))) (234)
b(b(b(d(d(c(c(x1))))))) → b(b(b(b(b(d(d(x1))))))) (235)

1.1.2.1.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[d(x1)] = 3x1 + 0
[c(x1)] = 3x1 + 1
[b(x1)] = 3x1 + 2

We obtain the labeled TRS

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

1.1.2.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
0
[d9(x1)] = x1 +
24
[d18(x1)] = x1 +
0
[d3(x1)] = x1 +
0
[d12(x1)] = x1 +
24
[d21(x1)] = x1 +
5
[d6(x1)] = x1 +
51
[d15(x1)] = x1 +
0
[d24(x1)] = x1 +
0
[d1(x1)] = x1 +
0
[d10(x1)] = x1 +
0
[d19(x1)] = x1 +
0
[d4(x1)] = x1 +
0
[d13(x1)] = x1 +
26
[d22(x1)] = x1 +
24
[d7(x1)] = x1 +
0
[d16(x1)] = x1 +
0
[d25(x1)] = x1 +
29
[d2(x1)] = x1 +
51
[d11(x1)] = x1 +
0
[d20(x1)] = x1 +
49
[d5(x1)] = x1 +
0
[d14(x1)] = x1 +
0
[d23(x1)] = x1 +
0
[d8(x1)] = x1 +
24
[d17(x1)] = x1 +
0
[d26(x1)] = x1 +
5
[c0(x1)] = x1 +
181
[c9(x1)] = x1 +
24
[c18(x1)] = x1 +
0
[c3(x1)] = x1 +
181
[c12(x1)] = x1 +
49
[c21(x1)] = x1 +
51
[c6(x1)] = x1 +
181
[c15(x1)] = x1 +
0
[c24(x1)] = x1 +
51
[c1(x1)] = x1 +
0
[c10(x1)] = x1 +
49
[c19(x1)] = x1 +
51
[c4(x1)] = x1 +
2
[c13(x1)] = x1 +
29
[c22(x1)] = x1 +
24
[c7(x1)] = x1 +
181
[c16(x1)] = x1 +
24
[c25(x1)] = x1 +
24
[c2(x1)] = x1 +
181
[c11(x1)] = x1 +
0
[c20(x1)] = x1 +
51
[c5(x1)] = x1 +
181
[c14(x1)] = x1 +
24
[c23(x1)] = x1 +
51
[c8(x1)] = x1 +
0
[c17(x1)] = x1 +
24
[c26(x1)] = x1 +
29
[b0(x1)] = x1 +
0
[b9(x1)] = x1 +
25
[b18(x1)] = x1 +
24
[b3(x1)] = x1 +
181
[b12(x1)] = x1 +
0
[b21(x1)] = x1 +
51
[b6(x1)] = x1 +
181
[b15(x1)] = x1 +
0
[b24(x1)] = x1 +
5
[b1(x1)] = x1 +
181
[b10(x1)] = x1 +
0
[b19(x1)] = x1 +
51
[b4(x1)] = x1 +
24
[b13(x1)] = x1 +
0
[b22(x1)] = x1 +
0
[b7(x1)] = x1 +
181
[b16(x1)] = x1 +
0
[b25(x1)] = x1 +
51
[b2(x1)] = x1 +
0
[b11(x1)] = x1 +
0
[b20(x1)] = x1 +
0
[b5(x1)] = x1 +
181
[b14(x1)] = x1 +
0
[b23(x1)] = x1 +
51
[b8(x1)] = x1 +
5
[b17(x1)] = x1 +
0
[b26(x1)] = x1 +
5
all of the following rules can be deleted.

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

1.1.2.1.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

{d(☐), c(☐), b(☐)}

We obtain the transformed TRS
d(b(b(d(d(b(b(x1))))))) → d(c(c(d(d(b(b(x1))))))) (20)
d(d(d(c(c(x1))))) → d(b(b(d(d(x1))))) (21)
c(b(b(d(d(b(b(x1))))))) → c(c(c(d(d(b(b(x1))))))) (23)
c(d(d(c(c(x1))))) → c(b(b(d(d(x1))))) (24)
b(b(b(d(d(b(b(x1))))))) → b(c(c(d(d(b(b(x1))))))) (26)
b(d(d(c(c(x1))))) → b(b(b(d(d(x1))))) (27)

1.1.2.2.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[d(x1)] = 3x1 + 0
[c(x1)] = 3x1 + 1
[b(x1)] = 3x1 + 2

We obtain the labeled TRS
b2(b2(b0(d0(d2(b2(b2(x1))))))) → b1(c1(c0(d0(d2(b2(b2(x1))))))) (80)
b2(b2(b0(d0(d2(b2(b0(x1))))))) → b1(c1(c0(d0(d2(b2(b0(x1))))))) (81)
b2(b2(b0(d0(d2(b2(b1(x1))))))) → b1(c1(c0(d0(d2(b2(b1(x1))))))) (82)
d2(b2(b0(d0(d2(b2(b2(x1))))))) → d1(c1(c0(d0(d2(b2(b2(x1))))))) (84)
d2(b2(b0(d0(d2(b2(b0(x1))))))) → d1(c1(c0(d0(d2(b2(b0(x1))))))) (85)
d2(b2(b0(d0(d2(b2(b1(x1))))))) → d1(c1(c0(d0(d2(b2(b1(x1))))))) (86)
c2(b2(b0(d0(d2(b2(b2(x1))))))) → c1(c1(c0(d0(d2(b2(b2(x1))))))) (88)
c2(b2(b0(d0(d2(b2(b0(x1))))))) → c1(c1(c0(d0(d2(b2(b0(x1))))))) (89)
c2(b2(b0(d0(d2(b2(b1(x1))))))) → c1(c1(c0(d0(d2(b2(b1(x1))))))) (90)
b0(d0(d1(c1(c2(x1))))) → b2(b2(b0(d0(d2(x1))))) (96)
b0(d0(d1(c1(c0(x1))))) → b2(b2(b0(d0(d0(x1))))) (97)
b0(d0(d1(c1(c1(x1))))) → b2(b2(b0(d0(d1(x1))))) (98)
d0(d0(d1(c1(c2(x1))))) → d2(b2(b0(d0(d2(x1))))) (100)
d0(d0(d1(c1(c0(x1))))) → d2(b2(b0(d0(d0(x1))))) (101)
d0(d0(d1(c1(c1(x1))))) → d2(b2(b0(d0(d1(x1))))) (102)
c0(d0(d1(c1(c2(x1))))) → c2(b2(b0(d0(d2(x1))))) (104)
c0(d0(d1(c1(c0(x1))))) → c2(b2(b0(d0(d0(x1))))) (105)
c0(d0(d1(c1(c1(x1))))) → c2(b2(b0(d0(d1(x1))))) (106)

1.1.2.2.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
0
[d1(x1)] = x1 +
3/2
[d2(x1)] = x1 +
1/2
[c0(x1)] = x1 +
0
[c1(x1)] = x1 +
3/2
[c2(x1)] = x1 +
1/2
[b0(x1)] = x1 +
3/2
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
1
all of the following rules can be deleted.
b2(b2(b0(d0(d2(b2(b2(x1))))))) → b1(c1(c0(d0(d2(b2(b2(x1))))))) (80)
b2(b2(b0(d0(d2(b2(b0(x1))))))) → b1(c1(c0(d0(d2(b2(b0(x1))))))) (81)
b2(b2(b0(d0(d2(b2(b1(x1))))))) → b1(c1(c0(d0(d2(b2(b1(x1))))))) (82)
b0(d0(d1(c1(c2(x1))))) → b2(b2(b0(d0(d2(x1))))) (96)
b0(d0(d1(c1(c0(x1))))) → b2(b2(b0(d0(d0(x1))))) (97)
b0(d0(d1(c1(c1(x1))))) → b2(b2(b0(d0(d1(x1))))) (98)

1.1.2.2.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[d0(x1)] =
2
· x1 +
1
[d1(x1)] =
2
· x1 +
1
[d2(x1)] =
2
· x1 +
1
[c0(x1)] =
1
· x1 +
1
[c1(x1)] =
1
· x1 +
1
[c2(x1)] =
1
· x1 +
1
[b0(x1)] =
1
· x1 +
1
[b1(x1)] =
2
· x1 +
1
[b2(x1)] =
1
· x1 +
1
all of the following rules can be deleted.
d0(d0(d1(c1(c2(x1))))) → d2(b2(b0(d0(d2(x1))))) (100)
d0(d0(d1(c1(c0(x1))))) → d2(b2(b0(d0(d0(x1))))) (101)
d0(d0(d1(c1(c1(x1))))) → d2(b2(b0(d0(d1(x1))))) (102)
c0(d0(d1(c1(c2(x1))))) → c2(b2(b0(d0(d2(x1))))) (104)
c0(d0(d1(c1(c0(x1))))) → c2(b2(b0(d0(d0(x1))))) (105)
c0(d0(d1(c1(c1(x1))))) → c2(b2(b0(d0(d1(x1))))) (106)

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
[d0(x1)] = x1 +
0
[d1(x1)] = x1 +
0
[d2(x1)] = x1 +
1
[c0(x1)] = x1 +
0
[c1(x1)] = x1 +
0
[c2(x1)] = x1 +
1
[b0(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
1
all of the following rules can be deleted.
d2(b2(b0(d0(d2(b2(b2(x1))))))) → d1(c1(c0(d0(d2(b2(b2(x1))))))) (84)
d2(b2(b0(d0(d2(b2(b0(x1))))))) → d1(c1(c0(d0(d2(b2(b0(x1))))))) (85)
d2(b2(b0(d0(d2(b2(b1(x1))))))) → d1(c1(c0(d0(d2(b2(b1(x1))))))) (86)
c2(b2(b0(d0(d2(b2(b2(x1))))))) → c1(c1(c0(d0(d2(b2(b2(x1))))))) (88)
c2(b2(b0(d0(d2(b2(b0(x1))))))) → c1(c1(c0(d0(d2(b2(b0(x1))))))) (89)
c2(b2(b0(d0(d2(b2(b1(x1))))))) → c1(c1(c0(d0(d2(b2(b1(x1))))))) (90)

1.1.2.2.1.1.1.1.1 R is empty

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