Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z003)

The rewrite relation of the following TRS is considered.

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

1.1 Closure Under Flat Contexts

Using the flat contexts

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

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

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(aa(x1)) → ab(bc(ca(aa(x1)))) (20)
aa(ab(x1)) → ab(bc(ca(ab(x1)))) (21)
aa(ac(x1)) → ab(bc(ca(ac(x1)))) (22)
aa(ad(x1)) → ab(bc(ca(ad(x1)))) (23)
aa(ac(cb(ba(x1)))) → ac(cb(ba(ab(ba(aa(x1)))))) (24)
aa(ac(cb(bb(x1)))) → ac(cb(ba(ab(ba(ab(x1)))))) (25)
aa(ac(cb(bc(x1)))) → ac(cb(ba(ab(ba(ac(x1)))))) (26)
aa(ac(cb(bd(x1)))) → ac(cb(ba(ab(ba(ad(x1)))))) (27)
ca(ac(cb(ba(x1)))) → cc(cb(ba(ab(ba(aa(x1)))))) (28)
ca(ac(cb(bb(x1)))) → cc(cb(ba(ab(ba(ab(x1)))))) (29)
ca(ac(cb(bc(x1)))) → cc(cb(ba(ab(ba(ac(x1)))))) (30)
ca(ac(cb(bd(x1)))) → cc(cb(ba(ab(ba(ad(x1)))))) (31)
ba(ac(cb(ba(x1)))) → bc(cb(ba(ab(ba(aa(x1)))))) (32)
ba(ac(cb(bb(x1)))) → bc(cb(ba(ab(ba(ab(x1)))))) (33)
ba(ac(cb(bc(x1)))) → bc(cb(ba(ab(ba(ac(x1)))))) (34)
ba(ac(cb(bd(x1)))) → bc(cb(ba(ab(ba(ad(x1)))))) (35)
da(ac(cb(ba(x1)))) → dc(cb(ba(ab(ba(aa(x1)))))) (36)
da(ac(cb(bb(x1)))) → dc(cb(ba(ab(ba(ab(x1)))))) (37)
da(ac(cb(bc(x1)))) → dc(cb(ba(ab(ba(ac(x1)))))) (38)
da(ac(cb(bd(x1)))) → dc(cb(ba(ab(ba(ad(x1)))))) (39)
ab(ba(x1)) → ac(cc(ca(x1))) (40)
ab(bb(x1)) → ac(cc(cb(x1))) (41)
ab(bc(x1)) → ac(cc(cc(x1))) (42)
ab(bd(x1)) → ac(cc(cd(x1))) (43)
cb(ba(x1)) → cc(cc(ca(x1))) (44)
cb(bb(x1)) → cc(cc(cb(x1))) (45)
cb(bc(x1)) → cc(cc(cc(x1))) (46)
cb(bd(x1)) → cc(cc(cd(x1))) (47)
bb(ba(x1)) → bc(cc(ca(x1))) (48)
bb(bb(x1)) → bc(cc(cb(x1))) (49)
bb(bc(x1)) → bc(cc(cc(x1))) (50)
bb(bd(x1)) → bc(cc(cd(x1))) (51)
db(ba(x1)) → dc(cc(ca(x1))) (52)
db(bb(x1)) → dc(cc(cb(x1))) (53)
db(bc(x1)) → dc(cc(cc(x1))) (54)
db(bd(x1)) → dc(cc(cd(x1))) (55)
ad(dc(ca(x1))) → aa(ac(cb(ba(aa(x1))))) (56)
ad(dc(cb(x1))) → aa(ac(cb(ba(ab(x1))))) (57)
ad(dc(cc(x1))) → aa(ac(cb(ba(ac(x1))))) (58)
ad(dc(cd(x1))) → aa(ac(cb(ba(ad(x1))))) (59)
cd(dc(ca(x1))) → ca(ac(cb(ba(aa(x1))))) (60)
cd(dc(cb(x1))) → ca(ac(cb(ba(ab(x1))))) (61)
cd(dc(cc(x1))) → ca(ac(cb(ba(ac(x1))))) (62)
cd(dc(cd(x1))) → ca(ac(cb(ba(ad(x1))))) (63)
bd(dc(ca(x1))) → ba(ac(cb(ba(aa(x1))))) (64)
bd(dc(cb(x1))) → ba(ac(cb(ba(ab(x1))))) (65)
bd(dc(cc(x1))) → ba(ac(cb(ba(ac(x1))))) (66)
bd(dc(cd(x1))) → ba(ac(cb(ba(ad(x1))))) (67)
dd(dc(ca(x1))) → da(ac(cb(ba(aa(x1))))) (68)
dd(dc(cb(x1))) → da(ac(cb(ba(ab(x1))))) (69)
dd(dc(cc(x1))) → da(ac(cb(ba(ac(x1))))) (70)
dd(dc(cd(x1))) → da(ac(cb(ba(ad(x1))))) (71)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1
[ab(x1)] = 1 · x1
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1
[ac(x1)] = 1 · x1
[ad(x1)] = 1 · x1 + 3
[cb(x1)] = 1 · x1
[ba(x1)] = 1 · x1
[bb(x1)] = 1 · x1
[bd(x1)] = 1 · x1 + 3
[cc(x1)] = 1 · x1
[da(x1)] = 1 · x1 + 1
[dc(x1)] = 1 · x1
[cd(x1)] = 1 · x1 + 2
[db(x1)] = 1 · x1 + 1
[dd(x1)] = 1 · x1 + 3
all of the following rules can be deleted.
da(ac(cb(ba(x1)))) → dc(cb(ba(ab(ba(aa(x1)))))) (36)
da(ac(cb(bb(x1)))) → dc(cb(ba(ab(ba(ab(x1)))))) (37)
da(ac(cb(bc(x1)))) → dc(cb(ba(ab(ba(ac(x1)))))) (38)
da(ac(cb(bd(x1)))) → dc(cb(ba(ab(ba(ad(x1)))))) (39)
ab(bd(x1)) → ac(cc(cd(x1))) (43)
cb(bd(x1)) → cc(cc(cd(x1))) (47)
bb(bd(x1)) → bc(cc(cd(x1))) (51)
db(ba(x1)) → dc(cc(ca(x1))) (52)
db(bb(x1)) → dc(cc(cb(x1))) (53)
db(bc(x1)) → dc(cc(cc(x1))) (54)
db(bd(x1)) → dc(cc(cd(x1))) (55)
ad(dc(ca(x1))) → aa(ac(cb(ba(aa(x1))))) (56)
ad(dc(cb(x1))) → aa(ac(cb(ba(ab(x1))))) (57)
ad(dc(cc(x1))) → aa(ac(cb(ba(ac(x1))))) (58)
ad(dc(cd(x1))) → aa(ac(cb(ba(ad(x1))))) (59)
cd(dc(ca(x1))) → ca(ac(cb(ba(aa(x1))))) (60)
cd(dc(cb(x1))) → ca(ac(cb(ba(ab(x1))))) (61)
cd(dc(cc(x1))) → ca(ac(cb(ba(ac(x1))))) (62)
cd(dc(cd(x1))) → ca(ac(cb(ba(ad(x1))))) (63)
bd(dc(ca(x1))) → ba(ac(cb(ba(aa(x1))))) (64)
bd(dc(cb(x1))) → ba(ac(cb(ba(ab(x1))))) (65)
bd(dc(cc(x1))) → ba(ac(cb(ba(ac(x1))))) (66)
bd(dc(cd(x1))) → ba(ac(cb(ba(ad(x1))))) (67)
dd(dc(ca(x1))) → da(ac(cb(ba(aa(x1))))) (68)
dd(dc(cb(x1))) → da(ac(cb(ba(ab(x1))))) (69)
dd(dc(cc(x1))) → da(ac(cb(ba(ac(x1))))) (70)
dd(dc(cd(x1))) → da(ac(cb(ba(ad(x1))))) (71)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1
[ab(x1)] = 1 · x1
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1
[ac(x1)] = 1 · x1
[ad(x1)] = 1 · x1
[cb(x1)] = 1 · x1
[ba(x1)] = 1 · x1
[bb(x1)] = 1 · x1
[bd(x1)] = 1 · x1 + 1
[cc(x1)] = 1 · x1
all of the following rules can be deleted.
aa(ac(cb(bd(x1)))) → ac(cb(ba(ab(ba(ad(x1)))))) (27)
ca(ac(cb(bd(x1)))) → cc(cb(ba(ab(ba(ad(x1)))))) (31)
ba(ac(cb(bd(x1)))) → bc(cb(ba(ab(ba(ad(x1)))))) (35)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1
[ab(x1)] = 1 · x1
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1
[ac(x1)] = 1 · x1
[ad(x1)] = 1 · x1
[cb(x1)] = 1 · x1 + 1
[ba(x1)] = 1 · x1
[bb(x1)] = 1 · x1 + 1
[cc(x1)] = 1 · x1
all of the following rules can be deleted.
aa(ac(cb(bb(x1)))) → ac(cb(ba(ab(ba(ab(x1)))))) (25)
ca(ac(cb(bb(x1)))) → cc(cb(ba(ab(ba(ab(x1)))))) (29)
ba(ac(cb(bb(x1)))) → bc(cb(ba(ab(ba(ab(x1)))))) (33)
cb(ba(x1)) → cc(cc(ca(x1))) (44)
cb(bb(x1)) → cc(cc(cb(x1))) (45)
cb(bc(x1)) → cc(cc(cc(x1))) (46)
bb(ba(x1)) → bc(cc(ca(x1))) (48)
bb(bb(x1)) → bc(cc(cb(x1))) (49)
bb(bc(x1)) → bc(cc(cc(x1))) (50)

1.1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
aa#(aa(x1)) → ab#(bc(ca(aa(x1)))) (72)
aa#(aa(x1)) → ca#(aa(x1)) (73)
aa#(ab(x1)) → ab#(bc(ca(ab(x1)))) (74)
aa#(ab(x1)) → ca#(ab(x1)) (75)
aa#(ac(x1)) → ab#(bc(ca(ac(x1)))) (76)
aa#(ac(x1)) → ca#(ac(x1)) (77)
aa#(ad(x1)) → ab#(bc(ca(ad(x1)))) (78)
aa#(ad(x1)) → ca#(ad(x1)) (79)
aa#(ac(cb(ba(x1)))) → ba#(ab(ba(aa(x1)))) (80)
aa#(ac(cb(ba(x1)))) → ab#(ba(aa(x1))) (81)
aa#(ac(cb(ba(x1)))) → ba#(aa(x1)) (82)
aa#(ac(cb(ba(x1)))) → aa#(x1) (83)
aa#(ac(cb(bc(x1)))) → ba#(ab(ba(ac(x1)))) (84)
aa#(ac(cb(bc(x1)))) → ab#(ba(ac(x1))) (85)
aa#(ac(cb(bc(x1)))) → ba#(ac(x1)) (86)
ca#(ac(cb(ba(x1)))) → ba#(ab(ba(aa(x1)))) (87)
ca#(ac(cb(ba(x1)))) → ab#(ba(aa(x1))) (88)
ca#(ac(cb(ba(x1)))) → ba#(aa(x1)) (89)
ca#(ac(cb(ba(x1)))) → aa#(x1) (90)
ca#(ac(cb(bc(x1)))) → ba#(ab(ba(ac(x1)))) (91)
ca#(ac(cb(bc(x1)))) → ab#(ba(ac(x1))) (92)
ca#(ac(cb(bc(x1)))) → ba#(ac(x1)) (93)
ba#(ac(cb(ba(x1)))) → ba#(ab(ba(aa(x1)))) (94)
ba#(ac(cb(ba(x1)))) → ab#(ba(aa(x1))) (95)
ba#(ac(cb(ba(x1)))) → ba#(aa(x1)) (96)
ba#(ac(cb(ba(x1)))) → aa#(x1) (97)
ba#(ac(cb(bc(x1)))) → ba#(ab(ba(ac(x1)))) (98)
ba#(ac(cb(bc(x1)))) → ab#(ba(ac(x1))) (99)
ba#(ac(cb(bc(x1)))) → ba#(ac(x1)) (100)
ab#(ba(x1)) → ca#(x1) (101)

1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.