Certification Problem

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

The rewrite relation of the following TRS is considered.

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

1.1.1 Dependency Pair Transformation

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

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.