Certification Problem

Input (TPDB SRS_Standard/Waldmann_19/random-443)

The rewrite relation of the following TRS is considered.

a(a(a(a(x1)))) → a(b(b(a(x1)))) (1)
b(b(b(a(x1)))) → a(a(b(a(x1)))) (2)
a(b(b(a(x1)))) → b(a(a(b(x1)))) (3)

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(a(a(x1))))) → b(a(b(b(a(x1))))) (4)
b(b(b(b(a(x1))))) → b(a(a(b(a(x1))))) (5)
b(a(b(b(a(x1))))) → b(b(a(a(b(x1))))) (6)
a(a(a(a(a(x1))))) → a(a(b(b(a(x1))))) (7)
a(b(b(b(a(x1))))) → a(a(a(b(a(x1))))) (8)
a(a(b(b(a(x1))))) → a(b(a(a(b(x1))))) (9)

1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(a(a(a(a(x1)))))) → b(b(a(b(b(a(x1)))))) (10)
b(b(b(b(b(a(x1)))))) → b(b(a(a(b(a(x1)))))) (11)
b(b(a(b(b(a(x1)))))) → b(b(b(a(a(b(x1)))))) (12)
b(a(a(a(a(a(x1)))))) → b(a(a(b(b(a(x1)))))) (13)
b(a(b(b(b(a(x1)))))) → b(a(a(a(b(a(x1)))))) (14)
b(a(a(b(b(a(x1)))))) → b(a(b(a(a(b(x1)))))) (15)
a(b(a(a(a(a(x1)))))) → a(b(a(b(b(a(x1)))))) (16)
a(b(b(b(b(a(x1)))))) → a(b(a(a(b(a(x1)))))) (17)
a(b(a(b(b(a(x1)))))) → a(b(b(a(a(b(x1)))))) (18)
a(a(a(a(a(a(x1)))))) → a(a(a(b(b(a(x1)))))) (19)
a(a(b(b(b(a(x1)))))) → a(a(a(a(b(a(x1)))))) (20)
a(a(a(b(b(a(x1)))))) → a(a(b(a(a(b(x1)))))) (21)

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

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

We obtain the labeled TRS
a3(a3(a3(a3(a3(a3(x1)))))) → a3(a1(a0(b2(b3(a3(x1)))))) (22)
a3(a3(a3(a3(a3(a1(x1)))))) → a3(a1(a0(b2(b3(a1(x1)))))) (23)
a3(a3(a3(a3(a1(a2(x1)))))) → a3(a1(a0(b2(b1(a2(x1)))))) (24)
a3(a3(a3(a3(a1(a0(x1)))))) → a3(a1(a0(b2(b1(a0(x1)))))) (25)
a2(b3(a3(a3(a3(a3(x1)))))) → a2(b1(a0(b2(b3(a3(x1)))))) (26)
a2(b3(a3(a3(a3(a1(x1)))))) → a2(b1(a0(b2(b3(a1(x1)))))) (27)
a2(b3(a3(a3(a1(a2(x1)))))) → a2(b1(a0(b2(b1(a2(x1)))))) (28)
a2(b3(a3(a3(a1(a0(x1)))))) → a2(b1(a0(b2(b1(a0(x1)))))) (29)
b3(a3(a3(a3(a3(a3(x1)))))) → b3(a1(a0(b2(b3(a3(x1)))))) (30)
b3(a3(a3(a3(a3(a1(x1)))))) → b3(a1(a0(b2(b3(a1(x1)))))) (31)
b3(a3(a3(a3(a1(a2(x1)))))) → b3(a1(a0(b2(b1(a2(x1)))))) (32)
b3(a3(a3(a3(a1(a0(x1)))))) → b3(a1(a0(b2(b1(a0(x1)))))) (33)
b2(b3(a3(a3(a3(a3(x1)))))) → b2(b1(a0(b2(b3(a3(x1)))))) (34)
b2(b3(a3(a3(a3(a1(x1)))))) → b2(b1(a0(b2(b3(a1(x1)))))) (35)
b2(b3(a3(a3(a1(a2(x1)))))) → b2(b1(a0(b2(b1(a2(x1)))))) (36)
b2(b3(a3(a3(a1(a0(x1)))))) → b2(b1(a0(b2(b1(a0(x1)))))) (37)
a1(a0(b0(b2(b3(a3(x1)))))) → a3(a3(a1(a2(b3(a3(x1)))))) (38)
a1(a0(b0(b2(b3(a1(x1)))))) → a3(a3(a1(a2(b3(a1(x1)))))) (39)
a1(a0(b0(b2(b1(a2(x1)))))) → a3(a3(a1(a2(b1(a2(x1)))))) (40)
a1(a0(b0(b2(b1(a0(x1)))))) → a3(a3(a1(a2(b1(a0(x1)))))) (41)
a0(b0(b0(b2(b3(a3(x1)))))) → a2(b3(a1(a2(b3(a3(x1)))))) (42)
a0(b0(b0(b2(b3(a1(x1)))))) → a2(b3(a1(a2(b3(a1(x1)))))) (43)
a0(b0(b0(b2(b1(a2(x1)))))) → a2(b3(a1(a2(b1(a2(x1)))))) (44)
a0(b0(b0(b2(b1(a0(x1)))))) → a2(b3(a1(a2(b1(a0(x1)))))) (45)
b1(a0(b0(b2(b3(a3(x1)))))) → b3(a3(a1(a2(b3(a3(x1)))))) (46)
b1(a0(b0(b2(b3(a1(x1)))))) → b3(a3(a1(a2(b3(a1(x1)))))) (47)
b1(a0(b0(b2(b1(a2(x1)))))) → b3(a3(a1(a2(b1(a2(x1)))))) (48)
b1(a0(b0(b2(b1(a0(x1)))))) → b3(a3(a1(a2(b1(a0(x1)))))) (49)
b0(b0(b0(b2(b3(a3(x1)))))) → b2(b3(a1(a2(b3(a3(x1)))))) (50)
b0(b0(b0(b2(b3(a1(x1)))))) → b2(b3(a1(a2(b3(a1(x1)))))) (51)
b0(b0(b0(b2(b1(a2(x1)))))) → b2(b3(a1(a2(b1(a2(x1)))))) (52)
b0(b0(b0(b2(b1(a0(x1)))))) → b2(b3(a1(a2(b1(a0(x1)))))) (53)
a3(a1(a0(b2(b3(a3(x1)))))) → a1(a2(b3(a1(a2(b3(x1)))))) (54)
a3(a1(a0(b2(b3(a1(x1)))))) → a1(a2(b3(a1(a2(b1(x1)))))) (55)
a3(a1(a0(b2(b1(a2(x1)))))) → a1(a2(b3(a1(a0(b2(x1)))))) (56)
a3(a1(a0(b2(b1(a0(x1)))))) → a1(a2(b3(a1(a0(b0(x1)))))) (57)
a2(b1(a0(b2(b3(a3(x1)))))) → a0(b2(b3(a1(a2(b3(x1)))))) (58)
a2(b1(a0(b2(b3(a1(x1)))))) → a0(b2(b3(a1(a2(b1(x1)))))) (59)
a2(b1(a0(b2(b1(a2(x1)))))) → a0(b2(b3(a1(a0(b2(x1)))))) (60)
a2(b1(a0(b2(b1(a0(x1)))))) → a0(b2(b3(a1(a0(b0(x1)))))) (61)
b3(a1(a0(b2(b3(a3(x1)))))) → b1(a2(b3(a1(a2(b3(x1)))))) (62)
b3(a1(a0(b2(b3(a1(x1)))))) → b1(a2(b3(a1(a2(b1(x1)))))) (63)
b3(a1(a0(b2(b1(a2(x1)))))) → b1(a2(b3(a1(a0(b2(x1)))))) (64)
b3(a1(a0(b2(b1(a0(x1)))))) → b1(a2(b3(a1(a0(b0(x1)))))) (65)
b2(b1(a0(b2(b3(a3(x1)))))) → b0(b2(b3(a1(a2(b3(x1)))))) (66)
b2(b1(a0(b2(b3(a1(x1)))))) → b0(b2(b3(a1(a2(b1(x1)))))) (67)
b2(b1(a0(b2(b1(a2(x1)))))) → b0(b2(b3(a1(a0(b2(x1)))))) (68)
b2(b1(a0(b2(b1(a0(x1)))))) → b0(b2(b3(a1(a0(b0(x1)))))) (69)

1.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 +
1
[b2(x1)] = x1 +
1
[b1(x1)] = x1 +
1/2
[b3(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a2(x1)] = x1 +
0
[a1(x1)] = x1 +
0
[a3(x1)] = x1 +
1
all of the following rules can be deleted.
a3(a3(a3(a3(a3(a3(x1)))))) → a3(a1(a0(b2(b3(a3(x1)))))) (22)
a3(a3(a3(a3(a3(a1(x1)))))) → a3(a1(a0(b2(b3(a1(x1)))))) (23)
a3(a3(a3(a3(a1(a2(x1)))))) → a3(a1(a0(b2(b1(a2(x1)))))) (24)
a3(a3(a3(a3(a1(a0(x1)))))) → a3(a1(a0(b2(b1(a0(x1)))))) (25)
a2(b3(a3(a3(a3(a3(x1)))))) → a2(b1(a0(b2(b3(a3(x1)))))) (26)
a2(b3(a3(a3(a3(a1(x1)))))) → a2(b1(a0(b2(b3(a1(x1)))))) (27)
b3(a3(a3(a3(a3(a3(x1)))))) → b3(a1(a0(b2(b3(a3(x1)))))) (30)
b3(a3(a3(a3(a3(a1(x1)))))) → b3(a1(a0(b2(b3(a1(x1)))))) (31)
b3(a3(a3(a3(a1(a2(x1)))))) → b3(a1(a0(b2(b1(a2(x1)))))) (32)
b3(a3(a3(a3(a1(a0(x1)))))) → b3(a1(a0(b2(b1(a0(x1)))))) (33)
b2(b3(a3(a3(a3(a3(x1)))))) → b2(b1(a0(b2(b3(a3(x1)))))) (34)
b2(b3(a3(a3(a3(a1(x1)))))) → b2(b1(a0(b2(b3(a1(x1)))))) (35)
a0(b0(b0(b2(b3(a3(x1)))))) → a2(b3(a1(a2(b3(a3(x1)))))) (42)
a0(b0(b0(b2(b3(a1(x1)))))) → a2(b3(a1(a2(b3(a1(x1)))))) (43)
a0(b0(b0(b2(b1(a2(x1)))))) → a2(b3(a1(a2(b1(a2(x1)))))) (44)
a0(b0(b0(b2(b1(a0(x1)))))) → a2(b3(a1(a2(b1(a0(x1)))))) (45)
b1(a0(b0(b2(b3(a3(x1)))))) → b3(a3(a1(a2(b3(a3(x1)))))) (46)
b1(a0(b0(b2(b3(a1(x1)))))) → b3(a3(a1(a2(b3(a1(x1)))))) (47)
b1(a0(b0(b2(b1(a2(x1)))))) → b3(a3(a1(a2(b1(a2(x1)))))) (48)
b1(a0(b0(b2(b1(a0(x1)))))) → b3(a3(a1(a2(b1(a0(x1)))))) (49)
b0(b0(b0(b2(b3(a3(x1)))))) → b2(b3(a1(a2(b3(a3(x1)))))) (50)
b0(b0(b0(b2(b3(a1(x1)))))) → b2(b3(a1(a2(b3(a1(x1)))))) (51)
b0(b0(b0(b2(b1(a2(x1)))))) → b2(b3(a1(a2(b1(a2(x1)))))) (52)
b0(b0(b0(b2(b1(a0(x1)))))) → b2(b3(a1(a2(b1(a0(x1)))))) (53)
a3(a1(a0(b2(b3(a3(x1)))))) → a1(a2(b3(a1(a2(b3(x1)))))) (54)
a3(a1(a0(b2(b3(a1(x1)))))) → a1(a2(b3(a1(a2(b1(x1)))))) (55)
a3(a1(a0(b2(b1(a2(x1)))))) → a1(a2(b3(a1(a0(b2(x1)))))) (56)
a3(a1(a0(b2(b1(a0(x1)))))) → a1(a2(b3(a1(a0(b0(x1)))))) (57)
a2(b1(a0(b2(b3(a3(x1)))))) → a0(b2(b3(a1(a2(b3(x1)))))) (58)
b3(a1(a0(b2(b3(a3(x1)))))) → b1(a2(b3(a1(a2(b3(x1)))))) (62)
b2(b1(a0(b2(b3(a3(x1)))))) → b0(b2(b3(a1(a2(b3(x1)))))) (66)

1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a2(a1(a3(a3(b3(a2(x1)))))) → a2(b1(b2(a0(b1(a2(x1)))))) (70)
a0(a1(a3(a3(b3(a2(x1)))))) → a0(b1(b2(a0(b1(a2(x1)))))) (71)
a2(a1(a3(a3(b3(b2(x1)))))) → a2(b1(b2(a0(b1(b2(x1)))))) (72)
a0(a1(a3(a3(b3(b2(x1)))))) → a0(b1(b2(a0(b1(b2(x1)))))) (73)
a3(b3(b2(b0(a0(a1(x1)))))) → a3(b3(a2(a1(a3(a3(x1)))))) (74)
a1(b3(b2(b0(a0(a1(x1)))))) → a1(b3(a2(a1(a3(a3(x1)))))) (75)
a2(b1(b2(b0(a0(a1(x1)))))) → a2(b1(a2(a1(a3(a3(x1)))))) (76)
a0(b1(b2(b0(a0(a1(x1)))))) → a0(b1(a2(a1(a3(a3(x1)))))) (77)
a1(b3(b2(a0(b1(a2(x1)))))) → b1(a2(a1(b3(b2(a0(x1)))))) (78)
a2(b1(b2(a0(b1(a2(x1)))))) → b2(a0(a1(b3(b2(a0(x1)))))) (79)
a0(b1(b2(a0(b1(a2(x1)))))) → b0(a0(a1(b3(b2(a0(x1)))))) (80)
a1(b3(b2(a0(a1(b3(x1)))))) → b1(a2(a1(b3(a2(b1(x1)))))) (81)
a2(b1(b2(a0(a1(b3(x1)))))) → b2(a0(a1(b3(a2(b1(x1)))))) (82)
a0(b1(b2(a0(a1(b3(x1)))))) → b0(a0(a1(b3(a2(b1(x1)))))) (83)
a1(b3(b2(a0(b1(b2(x1)))))) → b1(a2(a1(b3(b2(b0(x1)))))) (84)
a2(b1(b2(a0(b1(b2(x1)))))) → b2(a0(a1(b3(b2(b0(x1)))))) (85)
a0(b1(b2(a0(b1(b2(x1)))))) → b0(a0(a1(b3(b2(b0(x1)))))) (86)

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[b0(x1)] =
2
· x1 +
0
[b2(x1)] =
2
· x1 +
0
[b1(x1)] =
1
· x1 +
1
[b3(x1)] =
1
· x1 +
1
[a0(x1)] =
2
· x1 +
0
[a2(x1)] =
2
· x1 +
0
[a1(x1)] =
1
· x1 +
1
[a3(x1)] =
2
· x1 +
1
all of the following rules can be deleted.
a2(a1(a3(a3(b3(a2(x1)))))) → a2(b1(b2(a0(b1(a2(x1)))))) (70)
a0(a1(a3(a3(b3(a2(x1)))))) → a0(b1(b2(a0(b1(a2(x1)))))) (71)
a2(a1(a3(a3(b3(b2(x1)))))) → a2(b1(b2(a0(b1(b2(x1)))))) (72)
a0(a1(a3(a3(b3(b2(x1)))))) → a0(b1(b2(a0(b1(b2(x1)))))) (73)
a1(b3(b2(a0(b1(a2(x1)))))) → b1(a2(a1(b3(b2(a0(x1)))))) (78)
a2(b1(b2(a0(b1(a2(x1)))))) → b2(a0(a1(b3(b2(a0(x1)))))) (79)
a0(b1(b2(a0(b1(a2(x1)))))) → b0(a0(a1(b3(b2(a0(x1)))))) (80)
a1(b3(b2(a0(a1(b3(x1)))))) → b1(a2(a1(b3(a2(b1(x1)))))) (81)
a2(b1(b2(a0(a1(b3(x1)))))) → b2(a0(a1(b3(a2(b1(x1)))))) (82)
a0(b1(b2(a0(a1(b3(x1)))))) → b0(a0(a1(b3(a2(b1(x1)))))) (83)
a1(b3(b2(a0(b1(b2(x1)))))) → b1(a2(a1(b3(b2(b0(x1)))))) (84)
a2(b1(b2(a0(b1(b2(x1)))))) → b2(a0(a1(b3(b2(b0(x1)))))) (85)
a0(b1(b2(a0(b1(b2(x1)))))) → b0(a0(a1(b3(b2(b0(x1)))))) (86)

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
[b0(x1)] = x1 +
1
[b2(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b3(x1)] = x1 +
0
[a0(x1)] = x1 +
1
[a2(x1)] = x1 +
0
[a1(x1)] = x1 +
0
[a3(x1)] = x1 +
0
all of the following rules can be deleted.
a3(b3(b2(b0(a0(a1(x1)))))) → a3(b3(a2(a1(a3(a3(x1)))))) (74)
a1(b3(b2(b0(a0(a1(x1)))))) → a1(b3(a2(a1(a3(a3(x1)))))) (75)
a2(b1(b2(b0(a0(a1(x1)))))) → a2(b1(a2(a1(a3(a3(x1)))))) (76)
a0(b1(b2(b0(a0(a1(x1)))))) → a0(b1(a2(a1(a3(a3(x1)))))) (77)

1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

There are no rules.

1.1.1.1.1.1.1.1.1 R is empty

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