Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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)) → a(c(x1)) (4)
c(c(x1)) → a(b(c(b(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(b(a(x1))) → a(a(c(x1))) (9)
b(b(a(x1))) → b(a(c(x1))) (10)
c(b(a(x1))) → c(a(c(x1))) (11)
a(c(c(x1))) → a(a(b(c(b(c(x1)))))) (12)
b(c(c(x1))) → b(a(b(c(b(c(x1)))))) (13)
c(c(c(x1))) → c(a(b(c(b(c(x1)))))) (14)

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(aa(x1)) → aa(x1) (15)
aa(ab(x1)) → ab(x1) (16)
aa(ac(x1)) → ac(x1) (17)
ba(aa(x1)) → ba(x1) (18)
ba(ab(x1)) → bb(x1) (19)
ba(ac(x1)) → bc(x1) (20)
ca(aa(x1)) → ca(x1) (21)
ca(ab(x1)) → cb(x1) (22)
ca(ac(x1)) → cc(x1) (23)
ab(ba(aa(x1))) → aa(ac(ca(x1))) (24)
ab(ba(ab(x1))) → aa(ac(cb(x1))) (25)
ab(ba(ac(x1))) → aa(ac(cc(x1))) (26)
bb(ba(aa(x1))) → ba(ac(ca(x1))) (27)
bb(ba(ab(x1))) → ba(ac(cb(x1))) (28)
bb(ba(ac(x1))) → ba(ac(cc(x1))) (29)
cb(ba(aa(x1))) → ca(ac(ca(x1))) (30)
cb(ba(ab(x1))) → ca(ac(cb(x1))) (31)
cb(ba(ac(x1))) → ca(ac(cc(x1))) (32)
ac(cc(ca(x1))) → aa(ab(bc(cb(bc(ca(x1)))))) (33)
ac(cc(cb(x1))) → aa(ab(bc(cb(bc(cb(x1)))))) (34)
ac(cc(cc(x1))) → aa(ab(bc(cb(bc(cc(x1)))))) (35)
bc(cc(ca(x1))) → ba(ab(bc(cb(bc(ca(x1)))))) (36)
bc(cc(cb(x1))) → ba(ab(bc(cb(bc(cb(x1)))))) (37)
bc(cc(cc(x1))) → ba(ab(bc(cb(bc(cc(x1)))))) (38)
cc(cc(ca(x1))) → ca(ab(bc(cb(bc(ca(x1)))))) (39)
cc(cc(cb(x1))) → ca(ab(bc(cb(bc(cb(x1)))))) (40)
cc(cc(cc(x1))) → ca(ab(bc(cb(bc(cc(x1)))))) (41)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1
[ab(x1)] = 1 · x1
[ac(x1)] = 1 · x1 + 1
[ba(x1)] = 1 · x1 + 1
[bb(x1)] = 1 · x1 + 1
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1
[cb(x1)] = 1 · x1
[cc(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
ba(ac(x1)) → bc(x1) (20)
ac(cc(ca(x1))) → aa(ab(bc(cb(bc(ca(x1)))))) (33)
ac(cc(cb(x1))) → aa(ab(bc(cb(bc(cb(x1)))))) (34)
ac(cc(cc(x1))) → aa(ab(bc(cb(bc(cc(x1)))))) (35)
cc(cc(ca(x1))) → ca(ab(bc(cb(bc(ca(x1)))))) (39)
cc(cc(cb(x1))) → ca(ab(bc(cb(bc(cb(x1)))))) (40)
cc(cc(cc(x1))) → ca(ab(bc(cb(bc(cc(x1)))))) (41)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ba#(aa(x1)) → ba#(x1) (42)
ba#(ab(x1)) → bb#(x1) (43)
ca#(aa(x1)) → ca#(x1) (44)
ca#(ab(x1)) → cb#(x1) (45)
ab#(ba(aa(x1))) → aa#(ac(ca(x1))) (46)
ab#(ba(aa(x1))) → ca#(x1) (47)
ab#(ba(ab(x1))) → aa#(ac(cb(x1))) (48)
ab#(ba(ab(x1))) → cb#(x1) (49)
ab#(ba(ac(x1))) → aa#(ac(cc(x1))) (50)
bb#(ba(aa(x1))) → ba#(ac(ca(x1))) (51)
bb#(ba(aa(x1))) → ca#(x1) (52)
bb#(ba(ab(x1))) → ba#(ac(cb(x1))) (53)
bb#(ba(ab(x1))) → cb#(x1) (54)
bb#(ba(ac(x1))) → ba#(ac(cc(x1))) (55)
cb#(ba(aa(x1))) → ca#(ac(ca(x1))) (56)
cb#(ba(aa(x1))) → ca#(x1) (57)
cb#(ba(ab(x1))) → ca#(ac(cb(x1))) (58)
cb#(ba(ab(x1))) → cb#(x1) (59)
cb#(ba(ac(x1))) → ca#(ac(cc(x1))) (60)
bc#(cc(ca(x1))) → ba#(ab(bc(cb(bc(ca(x1)))))) (61)
bc#(cc(ca(x1))) → ab#(bc(cb(bc(ca(x1))))) (62)
bc#(cc(ca(x1))) → bc#(cb(bc(ca(x1)))) (63)
bc#(cc(ca(x1))) → cb#(bc(ca(x1))) (64)
bc#(cc(ca(x1))) → bc#(ca(x1)) (65)
bc#(cc(cb(x1))) → ba#(ab(bc(cb(bc(cb(x1)))))) (66)
bc#(cc(cb(x1))) → ab#(bc(cb(bc(cb(x1))))) (67)
bc#(cc(cb(x1))) → bc#(cb(bc(cb(x1)))) (68)
bc#(cc(cb(x1))) → cb#(bc(cb(x1))) (69)
bc#(cc(cb(x1))) → bc#(cb(x1)) (70)
bc#(cc(cc(x1))) → ba#(ab(bc(cb(bc(cc(x1)))))) (71)
bc#(cc(cc(x1))) → ab#(bc(cb(bc(cc(x1))))) (72)
bc#(cc(cc(x1))) → bc#(cb(bc(cc(x1)))) (73)
bc#(cc(cc(x1))) → cb#(bc(cc(x1))) (74)
bc#(cc(cc(x1))) → bc#(cc(x1)) (75)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.