Certification Problem

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

The rewrite relation of the following TRS is considered.

a(b(x1)) → x1 (1)
a(c(x1)) → c(c(b(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(c(c(b(a(x1))))) (5)
c(b(c(x1))) → c(a(b(x1))) (6)
b(a(b(x1))) → b(x1) (7)
b(a(c(x1))) → b(c(c(b(a(x1))))) (8)
b(b(c(x1))) → b(a(b(x1))) (9)
a(a(b(x1))) → a(x1) (10)
a(a(c(x1))) → a(c(c(b(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))) → a0(c0(c1(b2(a2(x1))))) (22)
a2(a0(c1(x1))) → a0(c0(c1(b2(a1(x1))))) (23)
a2(a0(c0(x1))) → a0(c0(c1(b2(a0(x1))))) (24)
b2(a0(c2(x1))) → b0(c0(c1(b2(a2(x1))))) (25)
b2(a0(c1(x1))) → b0(c0(c1(b2(a1(x1))))) (26)
b2(a0(c0(x1))) → b0(c0(c1(b2(a0(x1))))) (27)
c2(a0(c2(x1))) → c0(c0(c1(b2(a2(x1))))) (28)
c2(a0(c1(x1))) → c0(c0(c1(b2(a1(x1))))) (29)
c2(a0(c0(x1))) → c0(c0(c1(b2(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 Dependency Pair Transformation

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

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.