Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-546)

The rewrite relation of the following TRS is considered.

a(b(x1)) → x1 (1)
a(c(x1)) → b(b(x1)) (2)
c(b(x1)) → a(a(c(c(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

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

We obtain the transformed TRS
c(a(b(x1))) → c(x1) (4)
c(a(c(x1))) → c(b(b(x1))) (5)
c(c(b(x1))) → c(a(a(c(c(x1))))) (6)
b(a(b(x1))) → b(x1) (7)
b(a(c(x1))) → b(b(b(x1))) (8)
b(c(b(x1))) → b(a(a(c(c(x1))))) (9)
a(a(b(x1))) → a(x1) (10)
a(a(c(x1))) → a(b(b(x1))) (11)
a(c(b(x1))) → a(a(a(c(c(x1))))) (12)

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
c(c(a(b(x1)))) → c(c(x1)) (13)
c(c(a(c(x1)))) → c(c(b(b(x1)))) (14)
c(c(c(b(x1)))) → c(c(a(a(c(c(x1)))))) (15)
c(b(a(b(x1)))) → c(b(x1)) (16)
c(b(a(c(x1)))) → c(b(b(b(x1)))) (17)
c(b(c(b(x1)))) → c(b(a(a(c(c(x1)))))) (18)
c(a(a(b(x1)))) → c(a(x1)) (19)
c(a(a(c(x1)))) → c(a(b(b(x1)))) (20)
c(a(c(b(x1)))) → c(a(a(a(c(c(x1)))))) (21)
b(c(a(b(x1)))) → b(c(x1)) (22)
b(c(a(c(x1)))) → b(c(b(b(x1)))) (23)
b(c(c(b(x1)))) → b(c(a(a(c(c(x1)))))) (24)
b(b(a(b(x1)))) → b(b(x1)) (25)
b(b(a(c(x1)))) → b(b(b(b(x1)))) (26)
b(b(c(b(x1)))) → b(b(a(a(c(c(x1)))))) (27)
b(a(a(b(x1)))) → b(a(x1)) (28)
b(a(a(c(x1)))) → b(a(b(b(x1)))) (29)
b(a(c(b(x1)))) → b(a(a(a(c(c(x1)))))) (30)
a(c(a(b(x1)))) → a(c(x1)) (31)
a(c(a(c(x1)))) → a(c(b(b(x1)))) (32)
a(c(c(b(x1)))) → a(c(a(a(c(c(x1)))))) (33)
a(b(a(b(x1)))) → a(b(x1)) (34)
a(b(a(c(x1)))) → a(b(b(b(x1)))) (35)
a(b(c(b(x1)))) → a(b(a(a(c(c(x1)))))) (36)
a(a(a(b(x1)))) → a(a(x1)) (37)
a(a(a(c(x1)))) → a(a(b(b(x1)))) (38)
a(a(c(b(x1)))) → a(a(a(a(c(c(x1)))))) (39)

1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[c0(x1)] = x1 +
0
[c3(x1)] = x1 +
1
[c6(x1)] = x1 +
1
[c1(x1)] = x1 +
0
[c4(x1)] = x1 +
1
[c7(x1)] = x1 +
1
[c2(x1)] = x1 +
1
[c5(x1)] = x1 +
0
[c8(x1)] = x1 +
0
[b0(x1)] = x1 +
0
[b3(x1)] = x1 +
1
[b6(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b4(x1)] = x1 +
1
[b7(x1)] = x1 +
1
[b2(x1)] = x1 +
1
[b5(x1)] = x1 +
0
[b8(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a3(x1)] = x1 +
1
[a6(x1)] = x1 +
1
[a1(x1)] = x1 +
1/2
[a4(x1)] = x1 +
0
[a7(x1)] = x1 +
1
[a2(x1)] = x1 +
0
[a5(x1)] = x1 +
1/2
[a8(x1)] = x1 +
1/2
all of the following rules can be deleted.
a8(a5(a7(b8(x1)))) → a8(a8(x1)) (40)
a8(a5(a7(b5(x1)))) → a8(a5(x1)) (41)
a8(a5(a7(b2(x1)))) → a8(a2(x1)) (42)
a8(a5(a4(b7(x1)))) → a5(a7(x1)) (43)
a8(a5(a4(b4(x1)))) → a5(a4(x1)) (44)
a8(a5(a1(b6(x1)))) → a2(a6(x1)) (46)
a8(a5(a1(b3(x1)))) → a2(a3(x1)) (47)
a8(a5(a1(b0(x1)))) → a2(a0(x1)) (48)
a7(b5(a7(b8(x1)))) → a7(b8(x1)) (49)
a7(b5(a7(b5(x1)))) → a7(b5(x1)) (50)
a7(b5(a7(b2(x1)))) → a7(b2(x1)) (51)
a7(b5(a4(b7(x1)))) → a4(b7(x1)) (52)
a7(b5(a4(b4(x1)))) → a4(b4(x1)) (53)
a7(b5(a4(b1(x1)))) → a4(b1(x1)) (54)
a7(b5(a1(b6(x1)))) → a1(b6(x1)) (55)
a7(b5(a1(b3(x1)))) → a1(b3(x1)) (56)
a7(b5(a1(b0(x1)))) → a1(b0(x1)) (57)
a6(c5(a7(b8(x1)))) → a6(c8(x1)) (58)
a6(c5(a7(b5(x1)))) → a6(c5(x1)) (59)
a6(c5(a7(b2(x1)))) → a6(c2(x1)) (60)
a6(c5(a1(b6(x1)))) → a0(c6(x1)) (64)
a6(c5(a1(b3(x1)))) → a0(c3(x1)) (65)
a6(c5(a1(b0(x1)))) → a0(c0(x1)) (66)
b8(a5(a7(b8(x1)))) → b8(a8(x1)) (67)
b8(a5(a7(b5(x1)))) → b8(a5(x1)) (68)
b8(a5(a7(b2(x1)))) → b8(a2(x1)) (69)
b8(a5(a4(b7(x1)))) → b5(a7(x1)) (70)
b8(a5(a4(b4(x1)))) → b5(a4(x1)) (71)
b7(b5(a7(b8(x1)))) → b7(b8(x1)) (76)
b7(b5(a7(b5(x1)))) → b7(b5(x1)) (77)
b7(b5(a7(b2(x1)))) → b7(b2(x1)) (78)
b7(b5(a1(b6(x1)))) → b1(b6(x1)) (82)
b7(b5(a1(b3(x1)))) → b1(b3(x1)) (83)
b7(b5(a1(b0(x1)))) → b1(b0(x1)) (84)
b6(c5(a7(b8(x1)))) → b6(c8(x1)) (85)
b6(c5(a7(b5(x1)))) → b6(c5(x1)) (86)
b6(c5(a7(b2(x1)))) → b6(c2(x1)) (87)
b6(c5(a1(b6(x1)))) → b0(c6(x1)) (91)
b6(c5(a1(b3(x1)))) → b0(c3(x1)) (92)
b6(c5(a1(b0(x1)))) → b0(c0(x1)) (93)
c8(a5(a7(b8(x1)))) → c8(a8(x1)) (94)
c8(a5(a7(b5(x1)))) → c8(a5(x1)) (95)
c8(a5(a7(b2(x1)))) → c8(a2(x1)) (96)
c8(a5(a4(b7(x1)))) → c5(a7(x1)) (97)
c8(a5(a4(b4(x1)))) → c5(a4(x1)) (98)
c7(b5(a7(b8(x1)))) → c7(b8(x1)) (103)
c7(b5(a7(b5(x1)))) → c7(b5(x1)) (104)
c7(b5(a7(b2(x1)))) → c7(b2(x1)) (105)
c7(b5(a1(b6(x1)))) → c1(b6(x1)) (109)
c7(b5(a1(b3(x1)))) → c1(b3(x1)) (110)
c7(b5(a1(b0(x1)))) → c1(b0(x1)) (111)
c6(c5(a7(b8(x1)))) → c6(c8(x1)) (112)
c6(c5(a7(b5(x1)))) → c6(c5(x1)) (113)
c6(c5(a7(b2(x1)))) → c6(c2(x1)) (114)
c6(c5(a1(b6(x1)))) → c0(c6(x1)) (118)
c6(c5(a1(b3(x1)))) → c0(c3(x1)) (119)
c6(c5(a1(b0(x1)))) → c0(c0(x1)) (120)
a7(b2(a6(c8(x1)))) → a4(b4(b7(b8(x1)))) (130)
a7(b2(a6(c5(x1)))) → a4(b4(b7(b5(x1)))) (131)
a7(b2(a6(c2(x1)))) → a4(b4(b7(b2(x1)))) (132)
a7(b2(a3(c7(x1)))) → a4(b4(b4(b7(x1)))) (133)
a7(b2(a3(c4(x1)))) → a4(b4(b4(b4(x1)))) (134)
a7(b2(a3(c1(x1)))) → a4(b4(b4(b1(x1)))) (135)
a7(b2(a0(c6(x1)))) → a4(b4(b1(b6(x1)))) (136)
a7(b2(a0(c3(x1)))) → a4(b4(b1(b3(x1)))) (137)
a7(b2(a0(c0(x1)))) → a4(b4(b1(b0(x1)))) (138)
a1(b3(c7(b8(x1)))) → a7(b8(a2(a0(c6(c8(x1)))))) (211)
a1(b3(c7(b5(x1)))) → a7(b8(a2(a0(c6(c5(x1)))))) (212)
a1(b3(c7(b2(x1)))) → a7(b8(a2(a0(c6(c2(x1)))))) (213)
a1(b3(c4(b7(x1)))) → a7(b8(a2(a0(c3(c7(x1)))))) (214)
a1(b3(c4(b4(x1)))) → a7(b8(a2(a0(c3(c4(x1)))))) (215)
a1(b3(c4(b1(x1)))) → a7(b8(a2(a0(c3(c1(x1)))))) (216)
a1(b3(c1(b6(x1)))) → a7(b8(a2(a0(c0(c6(x1)))))) (217)
a1(b3(c1(b3(x1)))) → a7(b8(a2(a0(c0(c3(x1)))))) (218)
a1(b3(c1(b0(x1)))) → a7(b8(a2(a0(c0(c0(x1)))))) (219)
b2(a3(c7(b8(x1)))) → b8(a8(a2(a0(c6(c8(x1)))))) (229)
b2(a3(c7(b5(x1)))) → b8(a8(a2(a0(c6(c5(x1)))))) (230)
b2(a3(c7(b2(x1)))) → b8(a8(a2(a0(c6(c2(x1)))))) (231)
b2(a3(c4(b7(x1)))) → b8(a8(a2(a0(c3(c7(x1)))))) (232)
b2(a3(c4(b4(x1)))) → b8(a8(a2(a0(c3(c4(x1)))))) (233)
b2(a3(c4(b1(x1)))) → b8(a8(a2(a0(c3(c1(x1)))))) (234)
b2(a3(c1(b6(x1)))) → b8(a8(a2(a0(c0(c6(x1)))))) (235)
b2(a3(c1(b3(x1)))) → b8(a8(a2(a0(c0(c3(x1)))))) (236)
b2(a3(c1(b0(x1)))) → b8(a8(a2(a0(c0(c0(x1)))))) (237)
c2(a3(c7(b8(x1)))) → c8(a8(a2(a0(c6(c8(x1)))))) (256)
c2(a3(c7(b5(x1)))) → c8(a8(a2(a0(c6(c5(x1)))))) (257)
c2(a3(c7(b2(x1)))) → c8(a8(a2(a0(c6(c2(x1)))))) (258)
c2(a3(c4(b7(x1)))) → c8(a8(a2(a0(c3(c7(x1)))))) (259)
c2(a3(c4(b4(x1)))) → c8(a8(a2(a0(c3(c4(x1)))))) (260)
c2(a3(c4(b1(x1)))) → c8(a8(a2(a0(c3(c1(x1)))))) (261)
c2(a3(c1(b6(x1)))) → c8(a8(a2(a0(c0(c6(x1)))))) (262)
c2(a3(c1(b3(x1)))) → c8(a8(a2(a0(c0(c3(x1)))))) (263)
c2(a3(c1(b0(x1)))) → c8(a8(a2(a0(c0(c0(x1)))))) (264)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[c0(x1)] =
2
· x1 +
0
[c3(x1)] =
2
· x1 +
0
[c6(x1)] =
2
· x1 +
0
[c1(x1)] =
2
· x1 +
1
[c4(x1)] =
2
· x1 +
1
[c7(x1)] =
2
· x1 +
1
[c2(x1)] =
2
· x1 +
1
[c5(x1)] =
1
· x1 +
1
[c8(x1)] =
1
· x1 +
1
[b0(x1)] =
2
· x1 +
0
[b3(x1)] =
2
· x1 +
0
[b6(x1)] =
2
· x1 +
0
[b1(x1)] =
2
· x1 +
1
[b4(x1)] =
2
· x1 +
1
[b7(x1)] =
2
· x1 +
1
[b2(x1)] =
2
· x1 +
1
[b5(x1)] =
1
· x1 +
1
[b8(x1)] =
1
· x1 +
1
[a0(x1)] =
2
· x1 +
1
[a3(x1)] =
2
· x1 +
1
[a6(x1)] =
2
· x1 +
1
[a1(x1)] =
2
· x1 +
1
[a4(x1)] =
1
· x1 +
0
[a2(x1)] =
1
· x1 +
0
[a5(x1)] =
1
· x1 +
1
[a8(x1)] =
1
· x1 +
1
all of the following rules can be deleted.
a8(a5(a4(b1(x1)))) → a5(a1(x1)) (45)
a6(c5(a4(b7(x1)))) → a3(c7(x1)) (61)
a6(c5(a4(b4(x1)))) → a3(c4(x1)) (62)
a6(c5(a4(b1(x1)))) → a3(c1(x1)) (63)
b8(a5(a4(b1(x1)))) → b5(a1(x1)) (72)
b7(b5(a4(b7(x1)))) → b4(b7(x1)) (79)
b7(b5(a4(b4(x1)))) → b4(b4(x1)) (80)
b7(b5(a4(b1(x1)))) → b4(b1(x1)) (81)
b6(c5(a4(b7(x1)))) → b3(c7(x1)) (88)
b6(c5(a4(b4(x1)))) → b3(c4(x1)) (89)
b6(c5(a4(b1(x1)))) → b3(c1(x1)) (90)
c8(a5(a4(b1(x1)))) → c5(a1(x1)) (99)
c7(b5(a4(b7(x1)))) → c4(b7(x1)) (106)
c7(b5(a4(b4(x1)))) → c4(b4(x1)) (107)
c7(b5(a4(b1(x1)))) → c4(b1(x1)) (108)
c6(c5(a4(b7(x1)))) → c3(c7(x1)) (115)
c6(c5(a4(b4(x1)))) → c3(c4(x1)) (116)
c6(c5(a4(b1(x1)))) → c3(c1(x1)) (117)

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
[c0(x1)] = x1 +
14
[c3(x1)] = x1 +
1
[c6(x1)] = x1 +
5
[c1(x1)] = x1 +
47
[c4(x1)] = x1 +
52
[c7(x1)] = x1 +
47
[c2(x1)] = x1 +
61
[c5(x1)] = x1 +
0
[c8(x1)] = x1 +
1
[b0(x1)] = x1 +
5
[b3(x1)] = x1 +
0
[b6(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b4(x1)] = x1 +
14
[b7(x1)] = x1 +
0
[b2(x1)] = x1 +
47
[b5(x1)] = x1 +
0
[b8(x1)] = x1 +
0
[a0(x1)] = x1 +
1
[a3(x1)] = x1 +
5
[a6(x1)] = x1 +
1
[a1(x1)] = x1 +
66
[a4(x1)] = x1 +
0
[a2(x1)] = x1 +
1
[a5(x1)] = x1 +
0
[a8(x1)] = x1 +
1
all of the following rules can be deleted.

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

1.1.1.1.1.1.1 R is empty

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