Certification Problem

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

The rewrite relation of the following TRS is considered.

a(x1) → x1 (1)
a(b(x1)) → b(a(c(b(a(c(x1)))))) (2)
b(x1) → x1 (3)
c(c(x1)) → x1 (4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(x1) → x1 (1)
b(a(x1)) → c(a(b(c(a(b(x1)))))) (5)
b(x1) → x1 (3)
c(c(x1)) → x1 (4)

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
a(a(x1)) → a(x1) (6)
b(a(x1)) → b(x1) (7)
c(a(x1)) → c(x1) (8)
a(b(a(x1))) → a(c(a(b(c(a(b(x1))))))) (9)
b(b(a(x1))) → b(c(a(b(c(a(b(x1))))))) (10)
c(b(a(x1))) → c(c(a(b(c(a(b(x1))))))) (11)
a(b(x1)) → a(x1) (12)
b(b(x1)) → b(x1) (13)
c(b(x1)) → c(x1) (14)
a(c(c(x1))) → a(x1) (15)
b(c(c(x1))) → b(x1) (16)
c(c(c(x1))) → c(x1) (17)

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(aa(x1)) → aa(x1) (18)
aa(ab(x1)) → ab(x1) (19)
aa(ac(x1)) → ac(x1) (20)
ba(aa(x1)) → ba(x1) (21)
ba(ab(x1)) → bb(x1) (22)
ba(ac(x1)) → bc(x1) (23)
ca(aa(x1)) → ca(x1) (24)
ca(ab(x1)) → cb(x1) (25)
ca(ac(x1)) → cc(x1) (26)
ab(ba(aa(x1))) → ac(ca(ab(bc(ca(ab(ba(x1))))))) (27)
ab(ba(ab(x1))) → ac(ca(ab(bc(ca(ab(bb(x1))))))) (28)
ab(ba(ac(x1))) → ac(ca(ab(bc(ca(ab(bc(x1))))))) (29)
bb(ba(aa(x1))) → bc(ca(ab(bc(ca(ab(ba(x1))))))) (30)
bb(ba(ab(x1))) → bc(ca(ab(bc(ca(ab(bb(x1))))))) (31)
bb(ba(ac(x1))) → bc(ca(ab(bc(ca(ab(bc(x1))))))) (32)
cb(ba(aa(x1))) → cc(ca(ab(bc(ca(ab(ba(x1))))))) (33)
cb(ba(ab(x1))) → cc(ca(ab(bc(ca(ab(bb(x1))))))) (34)
cb(ba(ac(x1))) → cc(ca(ab(bc(ca(ab(bc(x1))))))) (35)
ab(ba(x1)) → aa(x1) (36)
ab(bb(x1)) → ab(x1) (37)
ab(bc(x1)) → ac(x1) (38)
bb(ba(x1)) → ba(x1) (39)
bb(bb(x1)) → bb(x1) (40)
bb(bc(x1)) → bc(x1) (41)
cb(ba(x1)) → ca(x1) (42)
cb(bb(x1)) → cb(x1) (43)
cb(bc(x1)) → cc(x1) (44)
ac(cc(ca(x1))) → aa(x1) (45)
ac(cc(cb(x1))) → ab(x1) (46)
ac(cc(cc(x1))) → ac(x1) (47)
bc(cc(ca(x1))) → ba(x1) (48)
bc(cc(cb(x1))) → bb(x1) (49)
bc(cc(cc(x1))) → bc(x1) (50)
cc(cc(ca(x1))) → ca(x1) (51)
cc(cc(cb(x1))) → cb(x1) (52)
cc(cc(cc(x1))) → cc(x1) (53)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1 + 2
[ab(x1)] = 1 · x1
[ac(x1)] = 1 · x1 + 1
[ba(x1)] = 1 · x1 + 2
[bb(x1)] = 1 · x1
[bc(x1)] = 1 · x1 + 1
[ca(x1)] = 1 · x1
[cb(x1)] = 1 · x1
[cc(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
aa(aa(x1)) → aa(x1) (18)
aa(ab(x1)) → ab(x1) (19)
aa(ac(x1)) → ac(x1) (20)
ba(aa(x1)) → ba(x1) (21)
ba(ab(x1)) → bb(x1) (22)
ba(ac(x1)) → bc(x1) (23)
ca(aa(x1)) → ca(x1) (24)
cb(ba(x1)) → ca(x1) (42)
ac(cc(cb(x1))) → ab(x1) (46)
ac(cc(cc(x1))) → ac(x1) (47)
bc(cc(cb(x1))) → bb(x1) (49)
bc(cc(cc(x1))) → bc(x1) (50)
cc(cc(ca(x1))) → ca(x1) (51)
cc(cc(cb(x1))) → cb(x1) (52)
cc(cc(cc(x1))) → cc(x1) (53)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ca#(ab(x1)) → cb#(x1) (54)
ab#(ba(aa(x1))) → ac#(ca(ab(bc(ca(ab(ba(x1))))))) (55)
ab#(ba(aa(x1))) → ca#(ab(bc(ca(ab(ba(x1)))))) (56)
ab#(ba(aa(x1))) → ab#(bc(ca(ab(ba(x1))))) (57)
ab#(ba(aa(x1))) → bc#(ca(ab(ba(x1)))) (58)
ab#(ba(aa(x1))) → ca#(ab(ba(x1))) (59)
ab#(ba(aa(x1))) → ab#(ba(x1)) (60)
ab#(ba(ab(x1))) → ac#(ca(ab(bc(ca(ab(bb(x1))))))) (61)
ab#(ba(ab(x1))) → ca#(ab(bc(ca(ab(bb(x1)))))) (62)
ab#(ba(ab(x1))) → ab#(bc(ca(ab(bb(x1))))) (63)
ab#(ba(ab(x1))) → bc#(ca(ab(bb(x1)))) (64)
ab#(ba(ab(x1))) → ca#(ab(bb(x1))) (65)
ab#(ba(ab(x1))) → ab#(bb(x1)) (66)
ab#(ba(ab(x1))) → bb#(x1) (67)
ab#(ba(ac(x1))) → ac#(ca(ab(bc(ca(ab(bc(x1))))))) (68)
ab#(ba(ac(x1))) → ca#(ab(bc(ca(ab(bc(x1)))))) (69)
ab#(ba(ac(x1))) → ab#(bc(ca(ab(bc(x1))))) (70)
ab#(ba(ac(x1))) → bc#(ca(ab(bc(x1)))) (71)
ab#(ba(ac(x1))) → ca#(ab(bc(x1))) (72)
ab#(ba(ac(x1))) → ab#(bc(x1)) (73)
ab#(ba(ac(x1))) → bc#(x1) (74)
bb#(ba(aa(x1))) → bc#(ca(ab(bc(ca(ab(ba(x1))))))) (75)
bb#(ba(aa(x1))) → ca#(ab(bc(ca(ab(ba(x1)))))) (76)
bb#(ba(aa(x1))) → ab#(bc(ca(ab(ba(x1))))) (77)
bb#(ba(aa(x1))) → bc#(ca(ab(ba(x1)))) (78)
bb#(ba(aa(x1))) → ca#(ab(ba(x1))) (79)
bb#(ba(aa(x1))) → ab#(ba(x1)) (80)
bb#(ba(ab(x1))) → bc#(ca(ab(bc(ca(ab(bb(x1))))))) (81)
bb#(ba(ab(x1))) → ca#(ab(bc(ca(ab(bb(x1)))))) (82)
bb#(ba(ab(x1))) → ab#(bc(ca(ab(bb(x1))))) (83)
bb#(ba(ab(x1))) → bc#(ca(ab(bb(x1)))) (84)
bb#(ba(ab(x1))) → ca#(ab(bb(x1))) (85)
bb#(ba(ab(x1))) → ab#(bb(x1)) (86)
bb#(ba(ab(x1))) → bb#(x1) (87)
bb#(ba(ac(x1))) → bc#(ca(ab(bc(ca(ab(bc(x1))))))) (88)
bb#(ba(ac(x1))) → ca#(ab(bc(ca(ab(bc(x1)))))) (89)
bb#(ba(ac(x1))) → ab#(bc(ca(ab(bc(x1))))) (90)
bb#(ba(ac(x1))) → bc#(ca(ab(bc(x1)))) (91)
bb#(ba(ac(x1))) → ca#(ab(bc(x1))) (92)
bb#(ba(ac(x1))) → ab#(bc(x1)) (93)
bb#(ba(ac(x1))) → bc#(x1) (94)
cb#(ba(aa(x1))) → ca#(ab(bc(ca(ab(ba(x1)))))) (95)
cb#(ba(aa(x1))) → ab#(bc(ca(ab(ba(x1))))) (96)
cb#(ba(aa(x1))) → bc#(ca(ab(ba(x1)))) (97)
cb#(ba(aa(x1))) → ca#(ab(ba(x1))) (98)
cb#(ba(aa(x1))) → ab#(ba(x1)) (99)
cb#(ba(ab(x1))) → ca#(ab(bc(ca(ab(bb(x1)))))) (100)
cb#(ba(ab(x1))) → ab#(bc(ca(ab(bb(x1))))) (101)
cb#(ba(ab(x1))) → bc#(ca(ab(bb(x1)))) (102)
cb#(ba(ab(x1))) → ca#(ab(bb(x1))) (103)
cb#(ba(ab(x1))) → ab#(bb(x1)) (104)
cb#(ba(ab(x1))) → bb#(x1) (105)
cb#(ba(ac(x1))) → ca#(ab(bc(ca(ab(bc(x1)))))) (106)
cb#(ba(ac(x1))) → ab#(bc(ca(ab(bc(x1))))) (107)
cb#(ba(ac(x1))) → bc#(ca(ab(bc(x1)))) (108)
cb#(ba(ac(x1))) → ca#(ab(bc(x1))) (109)
cb#(ba(ac(x1))) → ab#(bc(x1)) (110)
cb#(ba(ac(x1))) → bc#(x1) (111)
ab#(bb(x1)) → ab#(x1) (112)
ab#(bc(x1)) → ac#(x1) (113)
cb#(bb(x1)) → cb#(x1) (114)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.