Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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(a(a(x1))) → a(b(x1)) (9)
b(a(a(x1))) → b(b(x1)) (10)
c(a(a(x1))) → c(b(x1)) (11)
a(b(x1)) → a(x1) (12)
b(b(x1)) → b(x1) (13)
c(b(x1)) → c(x1) (14)
a(c(b(x1))) → a(a(b(c(c(c(x1)))))) (15)
b(c(b(x1))) → b(a(b(c(c(c(x1)))))) (16)
c(c(b(x1))) → c(a(b(c(c(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)
aa(aa(aa(x1))) → ab(ba(x1)) (27)
aa(aa(ab(x1))) → ab(bb(x1)) (28)
aa(aa(ac(x1))) → ab(bc(x1)) (29)
ba(aa(aa(x1))) → bb(ba(x1)) (30)
ba(aa(ab(x1))) → bb(bb(x1)) (31)
ba(aa(ac(x1))) → bb(bc(x1)) (32)
ca(aa(aa(x1))) → cb(ba(x1)) (33)
ca(aa(ab(x1))) → cb(bb(x1)) (34)
ca(aa(ac(x1))) → cb(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(cb(ba(x1))) → aa(ab(bc(cc(cc(ca(x1)))))) (45)
ac(cb(bb(x1))) → aa(ab(bc(cc(cc(cb(x1)))))) (46)
ac(cb(bc(x1))) → aa(ab(bc(cc(cc(cc(x1)))))) (47)
bc(cb(ba(x1))) → ba(ab(bc(cc(cc(ca(x1)))))) (48)
bc(cb(bb(x1))) → ba(ab(bc(cc(cc(cb(x1)))))) (49)
bc(cb(bc(x1))) → ba(ab(bc(cc(cc(cc(x1)))))) (50)
cc(cb(ba(x1))) → ca(ab(bc(cc(cc(ca(x1)))))) (51)
cc(cb(bb(x1))) → ca(ab(bc(cc(cc(cb(x1)))))) (52)
cc(cb(bc(x1))) → ca(ab(bc(cc(cc(cc(x1)))))) (53)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1 + 1
[ab(x1)] = 1 · x1
[ac(x1)] = 1 · x1 + 1
[ba(x1)] = 1 · x1 + 1
[bb(x1)] = 1 · x1 + 1
[bc(x1)] = 1 · x1 + 1
[ca(x1)] = 1 · x1
[cb(x1)] = 1 · x1
[cc(x1)] = 1 · x1
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(ac(x1)) → bc(x1) (23)
ca(aa(x1)) → ca(x1) (24)
ca(ac(x1)) → cc(x1) (26)
aa(aa(aa(x1))) → ab(ba(x1)) (27)
aa(aa(ab(x1))) → ab(bb(x1)) (28)
aa(aa(ac(x1))) → ab(bc(x1)) (29)
ba(aa(aa(x1))) → bb(ba(x1)) (30)
ba(aa(ac(x1))) → bb(bc(x1)) (32)
ca(aa(aa(x1))) → cb(ba(x1)) (33)
ca(aa(ac(x1))) → cb(bc(x1)) (35)
ab(bb(x1)) → ab(x1) (37)
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)

1.1.1.1.1 Dependency Pair Transformation

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

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.