Certification Problem

Input (TPDB SRS_Relative/Waldmann_19/random-72)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

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

1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS
a2(a2(a2(a2(x1)))) → a1(b0(c1(b2(x1)))) (29)
a2(a2(a2(a1(x1)))) → a1(b0(c1(b1(x1)))) (30)
a2(a2(a2(a0(x1)))) → a1(b0(c1(b0(x1)))) (31)
b2(a2(a2(a2(x1)))) → b1(b0(c1(b2(x1)))) (32)
b2(a2(a2(a1(x1)))) → b1(b0(c1(b1(x1)))) (33)
b2(a2(a2(a0(x1)))) → b1(b0(c1(b0(x1)))) (34)
c2(a2(a2(a2(x1)))) → c1(b0(c1(b2(x1)))) (35)
c2(a2(a2(a1(x1)))) → c1(b0(c1(b1(x1)))) (36)
c2(a2(a2(a0(x1)))) → c1(b0(c1(b0(x1)))) (37)
a1(b1(b1(b2(x1)))) → a2(a2(a0(c2(x1)))) (38)
a1(b1(b1(b1(x1)))) → a2(a2(a0(c1(x1)))) (39)
a1(b1(b1(b0(x1)))) → a2(a2(a0(c0(x1)))) (40)
b1(b1(b1(b2(x1)))) → b2(a2(a0(c2(x1)))) (41)
b1(b1(b1(b1(x1)))) → b2(a2(a0(c1(x1)))) (42)
b1(b1(b1(b0(x1)))) → b2(a2(a0(c0(x1)))) (43)
c1(b1(b1(b2(x1)))) → c2(a2(a0(c2(x1)))) (44)
c1(b1(b1(b1(x1)))) → c2(a2(a0(c1(x1)))) (45)
c1(b1(b1(b0(x1)))) → c2(a2(a0(c0(x1)))) (46)
a2(a1(b0(c2(x1)))) → a2(a0(c2(a2(x1)))) (47)
a2(a1(b0(c1(x1)))) → a2(a0(c2(a1(x1)))) (48)
a2(a1(b0(c0(x1)))) → a2(a0(c2(a0(x1)))) (49)
b2(a1(b0(c2(x1)))) → b2(a0(c2(a2(x1)))) (50)
b2(a1(b0(c1(x1)))) → b2(a0(c2(a1(x1)))) (51)
b2(a1(b0(c0(x1)))) → b2(a0(c2(a0(x1)))) (52)
c2(a1(b0(c2(x1)))) → c2(a0(c2(a2(x1)))) (53)
c2(a1(b0(c1(x1)))) → c2(a0(c2(a1(x1)))) (54)
c2(a1(b0(c0(x1)))) → c2(a0(c2(a0(x1)))) (55)
a1(b2(a2(a2(x1)))) → a0(c2(a0(c2(x1)))) (56)
a1(b2(a2(a1(x1)))) → a0(c2(a0(c1(x1)))) (57)
a1(b2(a2(a0(x1)))) → a0(c2(a0(c0(x1)))) (58)
b1(b2(a2(a2(x1)))) → b0(c2(a0(c2(x1)))) (59)
b1(b2(a2(a1(x1)))) → b0(c2(a0(c1(x1)))) (60)
b1(b2(a2(a0(x1)))) → b0(c2(a0(c0(x1)))) (61)
c1(b2(a2(a2(x1)))) → c0(c2(a0(c2(x1)))) (62)
c1(b2(a2(a1(x1)))) → c0(c2(a0(c1(x1)))) (63)
c1(b2(a2(a0(x1)))) → c0(c2(a0(c0(x1)))) (64)
a0(c2(a1(b2(x1)))) → a0(c2(a0(c2(x1)))) (65)
a0(c2(a1(b1(x1)))) → a0(c2(a0(c1(x1)))) (66)
a0(c2(a1(b0(x1)))) → a0(c2(a0(c0(x1)))) (67)
b0(c2(a1(b2(x1)))) → b0(c2(a0(c2(x1)))) (68)
b0(c2(a1(b1(x1)))) → b0(c2(a0(c1(x1)))) (69)
b0(c2(a1(b0(x1)))) → b0(c2(a0(c0(x1)))) (70)
c0(c2(a1(b2(x1)))) → c0(c2(a0(c2(x1)))) (71)
c0(c2(a1(b1(x1)))) → c0(c2(a0(c1(x1)))) (72)
c0(c2(a1(b0(x1)))) → c0(c2(a0(c0(x1)))) (73)
a2(a0(c0(c2(x1)))) → a2(a2(a0(c2(x1)))) (74)
a2(a0(c0(c1(x1)))) → a2(a2(a0(c1(x1)))) (75)
a2(a0(c0(c0(x1)))) → a2(a2(a0(c0(x1)))) (76)
b2(a0(c0(c2(x1)))) → b2(a2(a0(c2(x1)))) (77)
b2(a0(c0(c1(x1)))) → b2(a2(a0(c1(x1)))) (78)
b2(a0(c0(c0(x1)))) → b2(a2(a0(c0(x1)))) (79)
c2(a0(c0(c2(x1)))) → c2(a2(a0(c2(x1)))) (80)
c2(a0(c0(c1(x1)))) → c2(a2(a0(c1(x1)))) (81)
c2(a0(c0(c0(x1)))) → c2(a2(a0(c0(x1)))) (82)
a1(b2(a0(c2(x1)))) → a2(a2(a1(b2(x1)))) (83)
a1(b2(a0(c1(x1)))) → a2(a2(a1(b1(x1)))) (84)
a1(b2(a0(c0(x1)))) → a2(a2(a1(b0(x1)))) (85)
b1(b2(a0(c2(x1)))) → b2(a2(a1(b2(x1)))) (86)
b1(b2(a0(c1(x1)))) → b2(a2(a1(b1(x1)))) (87)
b1(b2(a0(c0(x1)))) → b2(a2(a1(b0(x1)))) (88)
c1(b2(a0(c2(x1)))) → c2(a2(a1(b2(x1)))) (89)
c1(b2(a0(c1(x1)))) → c2(a2(a1(b1(x1)))) (90)
c1(b2(a0(c0(x1)))) → c2(a2(a1(b0(x1)))) (91)

1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a2(a2(a2(a2(x1)))) → b2(c1(b0(a1(x1)))) (92)
a1(a2(a2(a2(x1)))) → b1(c1(b0(a1(x1)))) (93)
a0(a2(a2(a2(x1)))) → b0(c1(b0(a1(x1)))) (94)
a2(a2(a2(b2(x1)))) → b2(c1(b0(b1(x1)))) (95)
a1(a2(a2(b2(x1)))) → b1(c1(b0(b1(x1)))) (96)
a0(a2(a2(b2(x1)))) → b0(c1(b0(b1(x1)))) (97)
a2(a2(a2(c2(x1)))) → b2(c1(b0(c1(x1)))) (98)
a1(a2(a2(c2(x1)))) → b1(c1(b0(c1(x1)))) (99)
a0(a2(a2(c2(x1)))) → b0(c1(b0(c1(x1)))) (100)
b2(b1(b1(a1(x1)))) → c2(a0(a2(a2(x1)))) (101)
b1(b1(b1(a1(x1)))) → c1(a0(a2(a2(x1)))) (102)
b0(b1(b1(a1(x1)))) → c0(a0(a2(a2(x1)))) (103)
b2(b1(b1(b1(x1)))) → c2(a0(a2(b2(x1)))) (104)
b1(b1(b1(b1(x1)))) → c1(a0(a2(b2(x1)))) (105)
b0(b1(b1(b1(x1)))) → c0(a0(a2(b2(x1)))) (106)
b2(b1(b1(c1(x1)))) → c2(a0(a2(c2(x1)))) (107)
b1(b1(b1(c1(x1)))) → c1(a0(a2(c2(x1)))) (108)
b0(b1(b1(c1(x1)))) → c0(a0(a2(c2(x1)))) (109)
c2(b0(a1(a2(x1)))) → a2(c2(a0(a2(x1)))) (110)
c1(b0(a1(a2(x1)))) → a1(c2(a0(a2(x1)))) (111)
c0(b0(a1(a2(x1)))) → a0(c2(a0(a2(x1)))) (112)
c2(b0(a1(b2(x1)))) → a2(c2(a0(b2(x1)))) (113)
c1(b0(a1(b2(x1)))) → a1(c2(a0(b2(x1)))) (114)
c0(b0(a1(b2(x1)))) → a0(c2(a0(b2(x1)))) (115)
c2(b0(a1(c2(x1)))) → a2(c2(a0(c2(x1)))) (116)
c1(b0(a1(c2(x1)))) → a1(c2(a0(c2(x1)))) (117)
c0(b0(a1(c2(x1)))) → a0(c2(a0(c2(x1)))) (118)
a2(a2(b2(a1(x1)))) → c2(a0(c2(a0(x1)))) (119)
a1(a2(b2(a1(x1)))) → c1(a0(c2(a0(x1)))) (120)
a0(a2(b2(a1(x1)))) → c0(a0(c2(a0(x1)))) (121)
a2(a2(b2(b1(x1)))) → c2(a0(c2(b0(x1)))) (122)
a1(a2(b2(b1(x1)))) → c1(a0(c2(b0(x1)))) (123)
a0(a2(b2(b1(x1)))) → c0(a0(c2(b0(x1)))) (124)
a2(a2(b2(c1(x1)))) → c2(a0(c2(c0(x1)))) (125)
a1(a2(b2(c1(x1)))) → c1(a0(c2(c0(x1)))) (126)
a0(a2(b2(c1(x1)))) → c0(a0(c2(c0(x1)))) (127)
b2(a1(c2(a0(x1)))) → c2(a0(c2(a0(x1)))) (128)
b1(a1(c2(a0(x1)))) → c1(a0(c2(a0(x1)))) (129)
b0(a1(c2(a0(x1)))) → c0(a0(c2(a0(x1)))) (130)
b2(a1(c2(b0(x1)))) → c2(a0(c2(b0(x1)))) (131)
b1(a1(c2(b0(x1)))) → c1(a0(c2(b0(x1)))) (132)
b0(a1(c2(b0(x1)))) → c0(a0(c2(b0(x1)))) (133)
b2(a1(c2(c0(x1)))) → c2(a0(c2(c0(x1)))) (134)
b1(a1(c2(c0(x1)))) → c1(a0(c2(c0(x1)))) (135)
b0(a1(c2(c0(x1)))) → c0(a0(c2(c0(x1)))) (136)
c2(c0(a0(a2(x1)))) → c2(a0(a2(a2(x1)))) (137)
c1(c0(a0(a2(x1)))) → c1(a0(a2(a2(x1)))) (138)
c0(c0(a0(a2(x1)))) → c0(a0(a2(a2(x1)))) (139)
c2(c0(a0(b2(x1)))) → c2(a0(a2(b2(x1)))) (140)
c1(c0(a0(b2(x1)))) → c1(a0(a2(b2(x1)))) (141)
c0(c0(a0(b2(x1)))) → c0(a0(a2(b2(x1)))) (142)
c2(c0(a0(c2(x1)))) → c2(a0(a2(c2(x1)))) (143)
c1(c0(a0(c2(x1)))) → c1(a0(a2(c2(x1)))) (144)
c0(c0(a0(c2(x1)))) → c0(a0(a2(c2(x1)))) (145)
c2(a0(b2(a1(x1)))) → b2(a1(a2(a2(x1)))) (146)
c1(a0(b2(a1(x1)))) → b1(a1(a2(a2(x1)))) (147)
c0(a0(b2(a1(x1)))) → b0(a1(a2(a2(x1)))) (148)
c2(a0(b2(b1(x1)))) → b2(a1(a2(b2(x1)))) (149)
c1(a0(b2(b1(x1)))) → b1(a1(a2(b2(x1)))) (150)
c0(a0(b2(b1(x1)))) → b0(a1(a2(b2(x1)))) (151)
c2(a0(b2(c1(x1)))) → b2(a1(a2(c2(x1)))) (152)
c1(a0(b2(c1(x1)))) → b1(a1(a2(c2(x1)))) (153)
c0(a0(b2(c1(x1)))) → b0(a1(a2(c2(x1)))) (154)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

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
[c0(x1)] = x1 +
2
[c1(x1)] = x1 +
2
[c2(x1)] = x1 +
2
[b0(x1)] = x1 +
2
[b1(x1)] = x1 +
2
[b2(x1)] = x1 +
2
[a0(x1)] = x1 +
2
[a1(x1)] = x1 +
2
[a2(x1)] = x1 +
2
[c0#(x1)] = x1 +
1
[c1#(x1)] = x1 +
1
[c2#(x1)] = x1 +
1
[b0#(x1)] = x1 +
1
[b1#(x1)] = x1 +
1
[b2#(x1)] = x1 +
1
[a0#(x1)] = x1 +
1
[a1#(x1)] = x1 +
1
[a2#(x1)] = x1 +
1
together with the usable rules
a2(a2(a2(a2(x1)))) → b2(c1(b0(a1(x1)))) (92)
a1(a2(a2(a2(x1)))) → b1(c1(b0(a1(x1)))) (93)
a0(a2(a2(a2(x1)))) → b0(c1(b0(a1(x1)))) (94)
a2(a2(a2(b2(x1)))) → b2(c1(b0(b1(x1)))) (95)
a1(a2(a2(b2(x1)))) → b1(c1(b0(b1(x1)))) (96)
a0(a2(a2(b2(x1)))) → b0(c1(b0(b1(x1)))) (97)
a2(a2(a2(c2(x1)))) → b2(c1(b0(c1(x1)))) (98)
a1(a2(a2(c2(x1)))) → b1(c1(b0(c1(x1)))) (99)
a0(a2(a2(c2(x1)))) → b0(c1(b0(c1(x1)))) (100)
b2(b1(b1(a1(x1)))) → c2(a0(a2(a2(x1)))) (101)
b1(b1(b1(a1(x1)))) → c1(a0(a2(a2(x1)))) (102)
b0(b1(b1(a1(x1)))) → c0(a0(a2(a2(x1)))) (103)
b2(b1(b1(b1(x1)))) → c2(a0(a2(b2(x1)))) (104)
b1(b1(b1(b1(x1)))) → c1(a0(a2(b2(x1)))) (105)
b0(b1(b1(b1(x1)))) → c0(a0(a2(b2(x1)))) (106)
b2(b1(b1(c1(x1)))) → c2(a0(a2(c2(x1)))) (107)
b1(b1(b1(c1(x1)))) → c1(a0(a2(c2(x1)))) (108)
b0(b1(b1(c1(x1)))) → c0(a0(a2(c2(x1)))) (109)
c2(b0(a1(a2(x1)))) → a2(c2(a0(a2(x1)))) (110)
c1(b0(a1(a2(x1)))) → a1(c2(a0(a2(x1)))) (111)
c0(b0(a1(a2(x1)))) → a0(c2(a0(a2(x1)))) (112)
c2(b0(a1(b2(x1)))) → a2(c2(a0(b2(x1)))) (113)
c1(b0(a1(b2(x1)))) → a1(c2(a0(b2(x1)))) (114)
c0(b0(a1(b2(x1)))) → a0(c2(a0(b2(x1)))) (115)
c2(b0(a1(c2(x1)))) → a2(c2(a0(c2(x1)))) (116)
c1(b0(a1(c2(x1)))) → a1(c2(a0(c2(x1)))) (117)
c0(b0(a1(c2(x1)))) → a0(c2(a0(c2(x1)))) (118)
a2(a2(b2(a1(x1)))) → c2(a0(c2(a0(x1)))) (119)
a1(a2(b2(a1(x1)))) → c1(a0(c2(a0(x1)))) (120)
a0(a2(b2(a1(x1)))) → c0(a0(c2(a0(x1)))) (121)
a2(a2(b2(b1(x1)))) → c2(a0(c2(b0(x1)))) (122)
a1(a2(b2(b1(x1)))) → c1(a0(c2(b0(x1)))) (123)
a0(a2(b2(b1(x1)))) → c0(a0(c2(b0(x1)))) (124)
a2(a2(b2(c1(x1)))) → c2(a0(c2(c0(x1)))) (125)
a1(a2(b2(c1(x1)))) → c1(a0(c2(c0(x1)))) (126)
a0(a2(b2(c1(x1)))) → c0(a0(c2(c0(x1)))) (127)
b2(a1(c2(a0(x1)))) → c2(a0(c2(a0(x1)))) (128)
b1(a1(c2(a0(x1)))) → c1(a0(c2(a0(x1)))) (129)
b0(a1(c2(a0(x1)))) → c0(a0(c2(a0(x1)))) (130)
b2(a1(c2(b0(x1)))) → c2(a0(c2(b0(x1)))) (131)
b1(a1(c2(b0(x1)))) → c1(a0(c2(b0(x1)))) (132)
b0(a1(c2(b0(x1)))) → c0(a0(c2(b0(x1)))) (133)
b2(a1(c2(c0(x1)))) → c2(a0(c2(c0(x1)))) (134)
b1(a1(c2(c0(x1)))) → c1(a0(c2(c0(x1)))) (135)
b0(a1(c2(c0(x1)))) → c0(a0(c2(c0(x1)))) (136)
c2(c0(a0(a2(x1)))) → c2(a0(a2(a2(x1)))) (137)
c1(c0(a0(a2(x1)))) → c1(a0(a2(a2(x1)))) (138)
c0(c0(a0(a2(x1)))) → c0(a0(a2(a2(x1)))) (139)
c2(c0(a0(b2(x1)))) → c2(a0(a2(b2(x1)))) (140)
c1(c0(a0(b2(x1)))) → c1(a0(a2(b2(x1)))) (141)
c0(c0(a0(b2(x1)))) → c0(a0(a2(b2(x1)))) (142)
c2(c0(a0(c2(x1)))) → c2(a0(a2(c2(x1)))) (143)
c1(c0(a0(c2(x1)))) → c1(a0(a2(c2(x1)))) (144)
c0(c0(a0(c2(x1)))) → c0(a0(a2(c2(x1)))) (145)
c2(a0(b2(a1(x1)))) → b2(a1(a2(a2(x1)))) (146)
c1(a0(b2(a1(x1)))) → b1(a1(a2(a2(x1)))) (147)
c0(a0(b2(a1(x1)))) → b0(a1(a2(a2(x1)))) (148)
c2(a0(b2(b1(x1)))) → b2(a1(a2(b2(x1)))) (149)
c1(a0(b2(b1(x1)))) → b1(a1(a2(b2(x1)))) (150)
c0(a0(b2(b1(x1)))) → b0(a1(a2(b2(x1)))) (151)
c2(a0(b2(c1(x1)))) → b2(a1(a2(c2(x1)))) (152)
c1(a0(b2(c1(x1)))) → b1(a1(a2(c2(x1)))) (153)
c0(a0(b2(c1(x1)))) → b0(a1(a2(c2(x1)))) (154)
(w.r.t. the implicit argument filter of the reduction pair), the pairs

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

and no rules could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.