Certification Problem

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

The rewrite relation of the following TRS is considered.

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

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c2#(a0(c0(x1))) → c1#(b0(c0(c2(a2(a1(b0(x1))))))) (40)
c2#(a0(c0(x1))) → c2#(a2(a1(b0(x1)))) (41)
c2#(a0(c0(x1))) → a1#(b0(x1)) (42)
c2#(a0(c0(x1))) → a2#(a1(b0(x1))) (43)
c2#(a0(c1(x1))) → c1#(b0(c0(c2(a2(a1(b1(x1))))))) (44)
c2#(a0(c1(x1))) → c2#(a2(a1(b1(x1)))) (45)
c2#(a0(c1(x1))) → b1#(x1) (46)
c2#(a0(c1(x1))) → a1#(b1(x1)) (47)
c2#(a0(c1(x1))) → a2#(a1(b1(x1))) (48)
c2#(a0(c2(x1))) → c1#(b0(c0(c2(a2(a1(b2(x1))))))) (49)
c2#(a0(c2(x1))) → c2#(a2(a1(b2(x1)))) (50)
c2#(a0(c2(x1))) → b2#(x1) (51)
c2#(a0(c2(x1))) → a1#(b2(x1)) (52)
c2#(a0(c2(x1))) → a2#(a1(b2(x1))) (53)
c2#(a1(b1(x1))) → c1#(x1) (54)
c2#(a1(b2(x1))) → c2#(x1) (55)
b1#(b0(c1(x1))) → b1#(x1) (56)
b1#(b0(c2(x1))) → b2#(x1) (57)
b2#(a0(c0(x1))) → c2#(a2(a1(b0(x1)))) (58)
b2#(a0(c0(x1))) → b1#(b0(c0(c2(a2(a1(b0(x1))))))) (59)
b2#(a0(c0(x1))) → a1#(b0(x1)) (60)
b2#(a0(c0(x1))) → a2#(a1(b0(x1))) (61)
b2#(a0(c1(x1))) → c2#(a2(a1(b1(x1)))) (62)
b2#(a0(c1(x1))) → b1#(x1) (63)
b2#(a0(c1(x1))) → b1#(b0(c0(c2(a2(a1(b1(x1))))))) (64)
b2#(a0(c1(x1))) → a1#(b1(x1)) (65)
b2#(a0(c1(x1))) → a2#(a1(b1(x1))) (66)
b2#(a0(c2(x1))) → c2#(a2(a1(b2(x1)))) (67)
b2#(a0(c2(x1))) → b1#(b0(c0(c2(a2(a1(b2(x1))))))) (68)
b2#(a0(c2(x1))) → b2#(x1) (69)
b2#(a0(c2(x1))) → a1#(b2(x1)) (70)
b2#(a0(c2(x1))) → a2#(a1(b2(x1))) (71)
a1#(b0(c1(x1))) → a1#(x1) (72)
a1#(b0(c2(x1))) → a2#(x1) (73)
a2#(a0(c0(x1))) → c2#(a2(a1(b0(x1)))) (74)
a2#(a0(c0(x1))) → a1#(b0(x1)) (75)
a2#(a0(c0(x1))) → a1#(b0(c0(c2(a2(a1(b0(x1))))))) (76)
a2#(a0(c0(x1))) → a2#(a1(b0(x1))) (77)
a2#(a0(c1(x1))) → c2#(a2(a1(b1(x1)))) (78)
a2#(a0(c1(x1))) → b1#(x1) (79)
a2#(a0(c1(x1))) → a1#(b0(c0(c2(a2(a1(b1(x1))))))) (80)
a2#(a0(c1(x1))) → a1#(b1(x1)) (81)
a2#(a0(c1(x1))) → a2#(a1(b1(x1))) (82)
a2#(a0(c2(x1))) → c2#(a2(a1(b2(x1)))) (83)
a2#(a0(c2(x1))) → b2#(x1) (84)
a2#(a0(c2(x1))) → a1#(b0(c0(c2(a2(a1(b2(x1))))))) (85)
a2#(a0(c2(x1))) → a1#(b2(x1)) (86)
a2#(a0(c2(x1))) → a2#(a1(b2(x1))) (87)
a2#(a1(b1(x1))) → a1#(x1) (88)
a2#(a1(b2(x1))) → a2#(x1) (89)

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
[c1#(x1)] = x1 +
0
[c2#(x1)] = x1 +
1
[b1#(x1)] = x1 +
1
[b2#(x1)] = x1 +
1
[a1#(x1)] = x1 +
1
[a2#(x1)] = x1 +
1
together with the usable rules
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(a1(b2(x1))))))) (22)
a2(a0(c1(x1))) → a1(b0(c0(c2(a2(a1(b1(x1))))))) (23)
a2(a0(c0(x1))) → a1(b0(c0(c2(a2(a1(b0(x1))))))) (24)
b2(a0(c2(x1))) → b1(b0(c0(c2(a2(a1(b2(x1))))))) (25)
b2(a0(c1(x1))) → b1(b0(c0(c2(a2(a1(b1(x1))))))) (26)
b2(a0(c0(x1))) → b1(b0(c0(c2(a2(a1(b0(x1))))))) (27)
c2(a0(c2(x1))) → c1(b0(c0(c2(a2(a1(b2(x1))))))) (28)
c2(a0(c1(x1))) → c1(b0(c0(c2(a2(a1(b1(x1))))))) (29)
c2(a0(c0(x1))) → c1(b0(c0(c2(a2(a1(b0(x1))))))) (30)
a1(b0(c2(x1))) → a2(x1) (31)
a1(b0(c1(x1))) → a1(x1) (32)
a1(b0(c0(x1))) → a0(x1) (33)
b1(b0(c2(x1))) → b2(x1) (34)
b1(b0(c1(x1))) → b1(x1) (35)
b1(b0(c0(x1))) → b0(x1) (36)
c1(b0(c2(x1))) → c2(x1) (37)
c1(b0(c1(x1))) → c1(x1) (38)
c1(b0(c0(x1))) → c0(x1) (39)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
c2#(a0(c0(x1))) → c1#(b0(c0(c2(a2(a1(b0(x1))))))) (40)
c2#(a0(c1(x1))) → c1#(b0(c0(c2(a2(a1(b1(x1))))))) (44)
c2#(a0(c2(x1))) → c1#(b0(c0(c2(a2(a1(b2(x1))))))) (49)
c2#(a1(b1(x1))) → c1#(x1) (54)
and no rules could be deleted.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.