Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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

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

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 +
1
[c1(x1)] = x1 +
1/2
[c2(x1)] = x1 +
1
[b0(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
1/2
[a0(x1)] = x1 +
1/2
[a1(x1)] = x1 +
0
[a2(x1)] = x1 +
1/2
all of the following rules can be deleted.
a1(b2(a1(b2(x1)))) → a2(x1) (22)
a1(b2(a1(b1(x1)))) → a1(x1) (23)
b1(b2(a1(b2(x1)))) → b2(x1) (25)
b1(b2(a1(b1(x1)))) → b1(x1) (26)
b1(b2(a1(b0(x1)))) → b0(x1) (27)
c1(b2(a1(b2(x1)))) → c2(x1) (28)
c1(b2(a1(b1(x1)))) → c1(x1) (29)
a0(c0(c2(x1))) → a2(a2(a2(a1(b2(x1))))) (31)
a0(c0(c1(x1))) → a2(a2(a2(a1(b1(x1))))) (32)
a0(c0(c0(x1))) → a2(a2(a2(a1(b0(x1))))) (33)
b0(c0(c0(x1))) → b2(a2(a2(a1(b0(x1))))) (36)
c0(c0(c2(x1))) → c2(a2(a2(a1(b2(x1))))) (37)
c0(c0(c1(x1))) → c2(a2(a2(a1(b1(x1))))) (38)
c0(c0(c0(x1))) → c2(a2(a2(a1(b0(x1))))) (39)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c2#(a0(x1)) → c1#(b0(c0(x1))) (40)
c2#(a0(x1)) → b0#(c0(x1)) (41)
c2#(a1(x1)) → c1#(x1) (42)
c2#(a1(x1)) → c1#(b0(c1(x1))) (43)
c2#(a1(x1)) → b0#(c1(x1)) (44)
c2#(a2(x1)) → c1#(b0(c2(x1))) (45)
c2#(a2(x1)) → c2#(x1) (46)
c2#(a2(x1)) → b0#(c2(x1)) (47)
b0#(c0(c1(x1))) → b2#(a2(a2(a1(b1(x1))))) (48)
b0#(c0(c1(x1))) → a1#(b1(x1)) (49)
b0#(c0(c1(x1))) → a2#(a1(b1(x1))) (50)
b0#(c0(c1(x1))) → a2#(a2(a1(b1(x1)))) (51)
b0#(c0(c2(x1))) → b2#(x1) (52)
b0#(c0(c2(x1))) → b2#(a2(a2(a1(b2(x1))))) (53)
b0#(c0(c2(x1))) → a1#(b2(x1)) (54)
b0#(c0(c2(x1))) → a2#(a1(b2(x1))) (55)
b0#(c0(c2(x1))) → a2#(a2(a1(b2(x1)))) (56)
b2#(a0(x1)) → b0#(c0(x1)) (57)
b2#(a1(x1)) → c1#(x1) (58)
b2#(a1(x1)) → b0#(c1(x1)) (59)
b2#(a2(x1)) → c2#(x1) (60)
b2#(a2(x1)) → b0#(c2(x1)) (61)
a2#(a0(x1)) → b0#(c0(x1)) (62)
a2#(a0(x1)) → a1#(b0(c0(x1))) (63)
a2#(a1(x1)) → c1#(x1) (64)
a2#(a1(x1)) → b0#(c1(x1)) (65)
a2#(a1(x1)) → a1#(b0(c1(x1))) (66)
a2#(a2(x1)) → c2#(x1) (67)
a2#(a2(x1)) → b0#(c2(x1)) (68)
a2#(a2(x1)) → a1#(b0(c2(x1))) (69)

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 +
4
[c1(x1)] = x1 +
2
[c2(x1)] = x1 +
2
[b0(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[a0(x1)] = x1 +
4
[a1(x1)] = x1 +
2
[a2(x1)] = x1 +
2
[c1#(x1)] = x1 +
0
[c2#(x1)] = x1 +
5
[b0#(x1)] = x1 +
4
[b2#(x1)] = x1 +
4
[a1#(x1)] = x1 +
0
[a2#(x1)] = x1 +
5
together with the usable rules
a2(a2(x1)) → a1(b0(c2(x1))) (13)
a2(a1(x1)) → a1(b0(c1(x1))) (14)
a2(a0(x1)) → a1(b0(c0(x1))) (15)
b2(a2(x1)) → b1(b0(c2(x1))) (16)
b2(a1(x1)) → b1(b0(c1(x1))) (17)
b2(a0(x1)) → b1(b0(c0(x1))) (18)
c2(a2(x1)) → c1(b0(c2(x1))) (19)
c2(a1(x1)) → c1(b0(c1(x1))) (20)
c2(a0(x1)) → c1(b0(c0(x1))) (21)
a1(b2(a1(b0(x1)))) → a0(x1) (24)
c1(b2(a1(b0(x1)))) → c0(x1) (30)
b0(c0(c2(x1))) → b2(a2(a2(a1(b2(x1))))) (34)
b0(c0(c1(x1))) → b2(a2(a2(a1(b1(x1))))) (35)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
c2#(a0(x1)) → c1#(b0(c0(x1))) (40)
c2#(a0(x1)) → b0#(c0(x1)) (41)
c2#(a1(x1)) → c1#(x1) (42)
c2#(a1(x1)) → c1#(b0(c1(x1))) (43)
c2#(a1(x1)) → b0#(c1(x1)) (44)
c2#(a2(x1)) → c1#(b0(c2(x1))) (45)
c2#(a2(x1)) → c2#(x1) (46)
c2#(a2(x1)) → b0#(c2(x1)) (47)
b0#(c0(c1(x1))) → a1#(b1(x1)) (49)
b0#(c0(c1(x1))) → a2#(a1(b1(x1))) (50)
b0#(c0(c1(x1))) → a2#(a2(a1(b1(x1)))) (51)
b0#(c0(c2(x1))) → b2#(x1) (52)
b0#(c0(c2(x1))) → a1#(b2(x1)) (54)
b0#(c0(c2(x1))) → a2#(a1(b2(x1))) (55)
b0#(c0(c2(x1))) → a2#(a2(a1(b2(x1)))) (56)
b2#(a1(x1)) → c1#(x1) (58)
b2#(a2(x1)) → c2#(x1) (60)
a2#(a0(x1)) → b0#(c0(x1)) (62)
a2#(a0(x1)) → a1#(b0(c0(x1))) (63)
a2#(a1(x1)) → c1#(x1) (64)
a2#(a1(x1)) → b0#(c1(x1)) (65)
a2#(a1(x1)) → a1#(b0(c1(x1))) (66)
a2#(a2(x1)) → c2#(x1) (67)
a2#(a2(x1)) → b0#(c2(x1)) (68)
a2#(a2(x1)) → a1#(b0(c2(x1))) (69)
and no rules could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.