Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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

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

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(a1(b2(x1))) → a2(x1) (13)
a2(a1(b1(x1))) → a1(x1) (14)
a2(a1(b0(x1))) → a0(x1) (15)
b2(a1(b2(x1))) → b2(x1) (16)
b2(a1(b1(x1))) → b1(x1) (17)
b2(a1(b0(x1))) → b0(x1) (18)
c2(a1(b2(x1))) → c2(x1) (19)
c2(a1(b1(x1))) → c1(x1) (20)
c2(a1(b0(x1))) → c0(x1) (21)
a2(a0(c2(x1))) → a1(b0(c0(c2(a2(x1))))) (22)
a2(a0(c1(x1))) → a1(b0(c0(c2(a1(x1))))) (23)
a2(a0(c0(x1))) → a1(b0(c0(c2(a0(x1))))) (24)
b2(a0(c2(x1))) → b1(b0(c0(c2(a2(x1))))) (25)
b2(a0(c1(x1))) → b1(b0(c0(c2(a1(x1))))) (26)
b2(a0(c0(x1))) → b1(b0(c0(c2(a0(x1))))) (27)
c2(a0(c2(x1))) → c1(b0(c0(c2(a2(x1))))) (28)
c2(a0(c1(x1))) → c1(b0(c0(c2(a1(x1))))) (29)
c2(a0(c0(x1))) → c1(b0(c0(c2(a0(x1))))) (30)
a1(b0(c2(x1))) → a2(a1(b2(x1))) (31)
a1(b0(c1(x1))) → a2(a1(b1(x1))) (32)
a1(b0(c0(x1))) → a2(a1(b0(x1))) (33)
b1(b0(c2(x1))) → b2(a1(b2(x1))) (34)
b1(b0(c1(x1))) → b2(a1(b1(x1))) (35)
b1(b0(c0(x1))) → b2(a1(b0(x1))) (36)
c1(b0(c2(x1))) → c2(a1(b2(x1))) (37)
c1(b0(c1(x1))) → c2(a1(b1(x1))) (38)
c1(b0(c0(x1))) → c2(a1(b0(x1))) (39)

1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
b2(a1(a2(x1))) → a2(x1) (40)
b1(a1(a2(x1))) → a1(x1) (41)
b0(a1(a2(x1))) → a0(x1) (42)
b2(a1(b2(x1))) → b2(x1) (16)
b1(a1(b2(x1))) → b1(x1) (43)
b0(a1(b2(x1))) → b0(x1) (44)
b2(a1(c2(x1))) → c2(x1) (45)
b1(a1(c2(x1))) → c1(x1) (46)
b0(a1(c2(x1))) → c0(x1) (47)
c2(a0(a2(x1))) → a2(c2(c0(b0(a1(x1))))) (48)
c1(a0(a2(x1))) → a1(c2(c0(b0(a1(x1))))) (49)
c0(a0(a2(x1))) → a0(c2(c0(b0(a1(x1))))) (50)
c2(a0(b2(x1))) → a2(c2(c0(b0(b1(x1))))) (51)
c1(a0(b2(x1))) → a1(c2(c0(b0(b1(x1))))) (52)
c0(a0(b2(x1))) → a0(c2(c0(b0(b1(x1))))) (53)
c2(a0(c2(x1))) → a2(c2(c0(b0(c1(x1))))) (54)
c1(a0(c2(x1))) → a1(c2(c0(b0(c1(x1))))) (55)
c0(a0(c2(x1))) → a0(c2(c0(b0(c1(x1))))) (56)
c2(b0(a1(x1))) → b2(a1(a2(x1))) (57)
c1(b0(a1(x1))) → b1(a1(a2(x1))) (58)
c0(b0(a1(x1))) → b0(a1(a2(x1))) (59)
c2(b0(b1(x1))) → b2(a1(b2(x1))) (60)
c1(b0(b1(x1))) → b1(a1(b2(x1))) (61)
c0(b0(b1(x1))) → b0(a1(b2(x1))) (62)
c2(b0(c1(x1))) → b2(a1(c2(x1))) (63)
c1(b0(c1(x1))) → b1(a1(c2(x1))) (64)
c0(b0(c1(x1))) → b0(a1(c2(x1))) (65)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c0#(b0(c1(x1))) → c2#(x1) (66)
c0#(b0(c1(x1))) → b0#(a1(c2(x1))) (67)
c0#(b0(b1(x1))) → b0#(a1(b2(x1))) (68)
c0#(b0(b1(x1))) → b2#(x1) (69)
c0#(b0(a1(x1))) → b0#(a1(a2(x1))) (70)
c0#(a0(c2(x1))) → c0#(b0(c1(x1))) (71)
c0#(a0(c2(x1))) → c1#(x1) (72)
c0#(a0(c2(x1))) → c2#(c0(b0(c1(x1)))) (73)
c0#(a0(c2(x1))) → b0#(c1(x1)) (74)
c0#(a0(b2(x1))) → c0#(b0(b1(x1))) (75)
c0#(a0(b2(x1))) → c2#(c0(b0(b1(x1)))) (76)
c0#(a0(b2(x1))) → b0#(b1(x1)) (77)
c0#(a0(b2(x1))) → b1#(x1) (78)
c0#(a0(a2(x1))) → c0#(b0(a1(x1))) (79)
c0#(a0(a2(x1))) → c2#(c0(b0(a1(x1)))) (80)
c0#(a0(a2(x1))) → b0#(a1(x1)) (81)
c1#(b0(c1(x1))) → c2#(x1) (82)
c1#(b0(c1(x1))) → b1#(a1(c2(x1))) (83)
c1#(b0(b1(x1))) → b1#(a1(b2(x1))) (84)
c1#(b0(b1(x1))) → b2#(x1) (85)
c1#(b0(a1(x1))) → b1#(a1(a2(x1))) (86)
c1#(a0(c2(x1))) → c0#(b0(c1(x1))) (87)
c1#(a0(c2(x1))) → c1#(x1) (88)
c1#(a0(c2(x1))) → c2#(c0(b0(c1(x1)))) (89)
c1#(a0(c2(x1))) → b0#(c1(x1)) (90)
c1#(a0(b2(x1))) → c0#(b0(b1(x1))) (91)
c1#(a0(b2(x1))) → c2#(c0(b0(b1(x1)))) (92)
c1#(a0(b2(x1))) → b0#(b1(x1)) (93)
c1#(a0(b2(x1))) → b1#(x1) (94)
c1#(a0(a2(x1))) → c0#(b0(a1(x1))) (95)
c1#(a0(a2(x1))) → c2#(c0(b0(a1(x1)))) (96)
c1#(a0(a2(x1))) → b0#(a1(x1)) (97)
c2#(b0(c1(x1))) → c2#(x1) (98)
c2#(b0(c1(x1))) → b2#(a1(c2(x1))) (99)
c2#(b0(b1(x1))) → b2#(x1) (100)
c2#(b0(b1(x1))) → b2#(a1(b2(x1))) (101)
c2#(b0(a1(x1))) → b2#(a1(a2(x1))) (102)
c2#(a0(c2(x1))) → c0#(b0(c1(x1))) (103)
c2#(a0(c2(x1))) → c1#(x1) (104)
c2#(a0(c2(x1))) → c2#(c0(b0(c1(x1)))) (105)
c2#(a0(c2(x1))) → b0#(c1(x1)) (106)
c2#(a0(b2(x1))) → c0#(b0(b1(x1))) (107)
c2#(a0(b2(x1))) → c2#(c0(b0(b1(x1)))) (108)
c2#(a0(b2(x1))) → b0#(b1(x1)) (109)
c2#(a0(b2(x1))) → b1#(x1) (110)
c2#(a0(a2(x1))) → c0#(b0(a1(x1))) (111)
c2#(a0(a2(x1))) → c2#(c0(b0(a1(x1)))) (112)
c2#(a0(a2(x1))) → b0#(a1(x1)) (113)
b0#(a1(c2(x1))) → c0#(x1) (114)
b0#(a1(b2(x1))) → b0#(x1) (115)
b1#(a1(c2(x1))) → c1#(x1) (116)
b1#(a1(b2(x1))) → b1#(x1) (117)

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 +
0
[c1(x1)] = x1 +
0
[c2(x1)] = x1 +
0
[b0(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a1(x1)] = x1 +
0
[a2(x1)] = x1 +
0
[c0#(x1)] = x1 +
1
[c1#(x1)] = x1 +
1
[c2#(x1)] = x1 +
1
[b0#(x1)] = x1 +
1
[b1#(x1)] = x1 +
1
[b2#(x1)] = x1 +
0
together with the usable rules
b2(a1(a2(x1))) → a2(x1) (40)
b1(a1(a2(x1))) → a1(x1) (41)
b0(a1(a2(x1))) → a0(x1) (42)
b2(a1(b2(x1))) → b2(x1) (16)
b1(a1(b2(x1))) → b1(x1) (43)
b0(a1(b2(x1))) → b0(x1) (44)
b2(a1(c2(x1))) → c2(x1) (45)
b1(a1(c2(x1))) → c1(x1) (46)
b0(a1(c2(x1))) → c0(x1) (47)
c2(a0(a2(x1))) → a2(c2(c0(b0(a1(x1))))) (48)
c1(a0(a2(x1))) → a1(c2(c0(b0(a1(x1))))) (49)
c0(a0(a2(x1))) → a0(c2(c0(b0(a1(x1))))) (50)
c2(a0(b2(x1))) → a2(c2(c0(b0(b1(x1))))) (51)
c1(a0(b2(x1))) → a1(c2(c0(b0(b1(x1))))) (52)
c0(a0(b2(x1))) → a0(c2(c0(b0(b1(x1))))) (53)
c2(a0(c2(x1))) → a2(c2(c0(b0(c1(x1))))) (54)
c1(a0(c2(x1))) → a1(c2(c0(b0(c1(x1))))) (55)
c0(a0(c2(x1))) → a0(c2(c0(b0(c1(x1))))) (56)
c2(b0(a1(x1))) → b2(a1(a2(x1))) (57)
c1(b0(a1(x1))) → b1(a1(a2(x1))) (58)
c0(b0(a1(x1))) → b0(a1(a2(x1))) (59)
c2(b0(b1(x1))) → b2(a1(b2(x1))) (60)
c1(b0(b1(x1))) → b1(a1(b2(x1))) (61)
c0(b0(b1(x1))) → b0(a1(b2(x1))) (62)
c2(b0(c1(x1))) → b2(a1(c2(x1))) (63)
c1(b0(c1(x1))) → b1(a1(c2(x1))) (64)
c0(b0(c1(x1))) → b0(a1(c2(x1))) (65)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
c0#(b0(b1(x1))) → b2#(x1) (69)
c1#(b0(b1(x1))) → b2#(x1) (85)
c2#(b0(c1(x1))) → b2#(a1(c2(x1))) (99)
c2#(b0(b1(x1))) → b2#(x1) (100)
c2#(b0(b1(x1))) → b2#(a1(b2(x1))) (101)
c2#(b0(a1(x1))) → b2#(a1(a2(x1))) (102)
and no rules could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.