Certification Problem

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

The rewrite relation of the following TRS is considered.

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

1.1.1 String Reversal

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

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c0#(c0(a0(c2(x1)))) → c0#(x1) (66)
c0#(c0(a0(c2(x1)))) → c1#(c0(x1)) (67)
c0#(c0(a0(c2(x1)))) → c2#(a0(b2(c1(c0(x1))))) (68)
c0#(c0(a0(c2(x1)))) → b2#(c1(c0(x1))) (69)
c0#(c0(a0(c2(x1)))) → a0#(c2(a0(b2(c1(c0(x1)))))) (70)
c0#(c0(a0(c2(x1)))) → a0#(b2(c1(c0(x1)))) (71)
c0#(c0(a0(b2(x1)))) → c1#(b0(x1)) (72)
c0#(c0(a0(b2(x1)))) → c2#(a0(b2(c1(b0(x1))))) (73)
c0#(c0(a0(b2(x1)))) → b0#(x1) (74)
c0#(c0(a0(b2(x1)))) → b2#(c1(b0(x1))) (75)
c0#(c0(a0(b2(x1)))) → a0#(c2(a0(b2(c1(b0(x1)))))) (76)
c0#(c0(a0(b2(x1)))) → a0#(b2(c1(b0(x1)))) (77)
c0#(c0(a0(a2(x1)))) → c1#(a0(x1)) (78)
c0#(c0(a0(a2(x1)))) → c2#(a0(b2(c1(a0(x1))))) (79)
c0#(c0(a0(a2(x1)))) → b2#(c1(a0(x1))) (80)
c0#(c0(a0(a2(x1)))) → a0#(x1) (81)
c0#(c0(a0(a2(x1)))) → a0#(c2(a0(b2(c1(a0(x1)))))) (82)
c0#(c0(a0(a2(x1)))) → a0#(b2(c1(a0(x1)))) (83)
c1#(c0(a0(c2(x1)))) → c0#(x1) (84)
c1#(c0(a0(c2(x1)))) → c1#(c0(x1)) (85)
c1#(c0(a0(c2(x1)))) → c2#(a0(b2(c1(c0(x1))))) (86)
c1#(c0(a0(c2(x1)))) → b2#(c1(c0(x1))) (87)
c1#(c0(a0(c2(x1)))) → a0#(b2(c1(c0(x1)))) (88)
c1#(c0(a0(c2(x1)))) → a1#(c2(a0(b2(c1(c0(x1)))))) (89)
c1#(c0(a0(b2(x1)))) → c1#(b0(x1)) (90)
c1#(c0(a0(b2(x1)))) → c2#(a0(b2(c1(b0(x1))))) (91)
c1#(c0(a0(b2(x1)))) → b0#(x1) (92)
c1#(c0(a0(b2(x1)))) → b2#(c1(b0(x1))) (93)
c1#(c0(a0(b2(x1)))) → a0#(b2(c1(b0(x1)))) (94)
c1#(c0(a0(b2(x1)))) → a1#(c2(a0(b2(c1(b0(x1)))))) (95)
c1#(c0(a0(a2(x1)))) → c1#(a0(x1)) (96)
c1#(c0(a0(a2(x1)))) → c2#(a0(b2(c1(a0(x1))))) (97)
c1#(c0(a0(a2(x1)))) → b2#(c1(a0(x1))) (98)
c1#(c0(a0(a2(x1)))) → a0#(x1) (99)
c1#(c0(a0(a2(x1)))) → a0#(b2(c1(a0(x1)))) (100)
c1#(c0(a0(a2(x1)))) → a1#(c2(a0(b2(c1(a0(x1)))))) (101)
c2#(c0(a0(c2(x1)))) → c0#(x1) (102)
c2#(c0(a0(c2(x1)))) → c1#(c0(x1)) (103)
c2#(c0(a0(c2(x1)))) → c2#(a0(b2(c1(c0(x1))))) (104)
c2#(c0(a0(c2(x1)))) → b2#(c1(c0(x1))) (105)
c2#(c0(a0(c2(x1)))) → a0#(b2(c1(c0(x1)))) (106)
c2#(c0(a0(c2(x1)))) → a2#(c2(a0(b2(c1(c0(x1)))))) (107)
c2#(c0(a0(b2(x1)))) → c1#(b0(x1)) (108)
c2#(c0(a0(b2(x1)))) → c2#(a0(b2(c1(b0(x1))))) (109)
c2#(c0(a0(b2(x1)))) → b0#(x1) (110)
c2#(c0(a0(b2(x1)))) → b2#(c1(b0(x1))) (111)
c2#(c0(a0(b2(x1)))) → a0#(b2(c1(b0(x1)))) (112)
c2#(c0(a0(b2(x1)))) → a2#(c2(a0(b2(c1(b0(x1)))))) (113)
c2#(c0(a0(a2(x1)))) → c1#(a0(x1)) (114)
c2#(c0(a0(a2(x1)))) → c2#(a0(b2(c1(a0(x1))))) (115)
c2#(c0(a0(a2(x1)))) → b2#(c1(a0(x1))) (116)
c2#(c0(a0(a2(x1)))) → a0#(x1) (117)
c2#(c0(a0(a2(x1)))) → a0#(b2(c1(a0(x1)))) (118)
c2#(c0(a0(a2(x1)))) → a2#(c2(a0(b2(c1(a0(x1)))))) (119)
b0#(a1(c2(x1))) → c0#(x1) (120)
b0#(a1(c2(x1))) → c0#(c0(x1)) (121)
b0#(a1(b2(x1))) → c0#(b0(x1)) (122)
b0#(a1(b2(x1))) → b0#(x1) (123)
b0#(a1(a2(x1))) → c0#(a0(x1)) (124)
b0#(a1(a2(x1))) → a0#(x1) (125)
b1#(a1(c2(x1))) → c0#(x1) (126)
b1#(a1(c2(x1))) → c1#(c0(x1)) (127)
b1#(a1(b2(x1))) → c1#(b0(x1)) (128)
b1#(a1(b2(x1))) → b0#(x1) (129)
b1#(a1(a2(x1))) → c1#(a0(x1)) (130)
b1#(a1(a2(x1))) → a0#(x1) (131)
b2#(a1(c2(x1))) → c0#(x1) (132)
b2#(a1(c2(x1))) → c2#(c0(x1)) (133)
b2#(a1(b2(x1))) → c2#(b0(x1)) (134)
b2#(a1(b2(x1))) → b0#(x1) (135)
b2#(a1(a2(x1))) → c2#(a0(x1)) (136)
b2#(a1(a2(x1))) → a0#(x1) (137)
a0#(c2(x1)) → c0#(x1) (138)
a0#(b2(x1)) → b0#(x1) (139)
a0#(a2(x1)) → a0#(x1) (140)
a1#(c2(x1)) → c1#(x1) (141)
a1#(b2(x1)) → b1#(x1) (142)
a1#(a2(x1)) → a1#(x1) (143)

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

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.