Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup12)

The rewrite relation of the following TRS is considered.

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1)))))) (1)
b(b(a(a(c(c(x1)))))) → b(b(c(c(x1)))) (2)
a(a(d(d(x1)))) → d(d(c(c(x1)))) (3)
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1)))))) (4)
d(d(c(c(x1)))) → b(b(d(d(x1)))) (5)
d(d(c(c(x1)))) → d(d(b(b(d(d(x1)))))) (6)
d(d(a(a(c(c(x1)))))) → b(b(b(b(x1)))) (7)

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

1.1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
b(b(d(d(b(b(x1)))))) → b(b(d(d(c(c(x1)))))) (8)
c(c(a(a(b(b(x1)))))) → c(c(b(b(x1)))) (9)
b(d(d(a(a(x1))))) → b(c(c(d(d(x1))))) (15)
d(d(d(a(a(x1))))) → d(c(c(d(d(x1))))) (16)
c(d(d(a(a(x1))))) → c(c(c(d(d(x1))))) (17)
a(d(d(a(a(x1))))) → a(c(c(d(d(x1))))) (18)
b(b(b(b(b(b(b(x1))))))) → b(c(c(b(b(a(a(x1))))))) (19)
d(b(b(b(b(b(b(x1))))))) → d(c(c(b(b(a(a(x1))))))) (20)
c(b(b(b(b(b(b(x1))))))) → c(c(c(b(b(a(a(x1))))))) (21)
a(b(b(b(b(b(b(x1))))))) → a(c(c(b(b(a(a(x1))))))) (22)
b(c(c(d(d(x1))))) → b(d(d(b(b(x1))))) (23)
d(c(c(d(d(x1))))) → d(d(d(b(b(x1))))) (24)
c(c(c(d(d(x1))))) → c(d(d(b(b(x1))))) (25)
a(c(c(d(d(x1))))) → a(d(d(b(b(x1))))) (26)
b(c(c(d(d(x1))))) → b(d(d(b(b(d(d(x1))))))) (27)
d(c(c(d(d(x1))))) → d(d(d(b(b(d(d(x1))))))) (28)
c(c(c(d(d(x1))))) → c(d(d(b(b(d(d(x1))))))) (29)
a(c(c(d(d(x1))))) → a(d(d(b(b(d(d(x1))))))) (30)
b(c(c(a(a(d(d(x1))))))) → b(b(b(b(b(x1))))) (31)
d(c(c(a(a(d(d(x1))))))) → d(b(b(b(b(x1))))) (32)
c(c(c(a(a(d(d(x1))))))) → c(b(b(b(b(x1))))) (33)
a(c(c(a(a(d(d(x1))))))) → a(b(b(b(b(x1))))) (34)

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
bb(bd(dd(db(bb(bb(x1)))))) → bb(bd(dd(dc(cc(cb(x1)))))) (35)
bb(bd(dd(db(bb(bd(x1)))))) → bb(bd(dd(dc(cc(cd(x1)))))) (36)
bb(bd(dd(db(bb(bc(x1)))))) → bb(bd(dd(dc(cc(cc(x1)))))) (37)
bb(bd(dd(db(bb(ba(x1)))))) → bb(bd(dd(dc(cc(ca(x1)))))) (38)
cc(ca(aa(ab(bb(bb(x1)))))) → cc(cb(bb(bb(x1)))) (39)
cc(ca(aa(ab(bb(bd(x1)))))) → cc(cb(bb(bd(x1)))) (40)
cc(ca(aa(ab(bb(bc(x1)))))) → cc(cb(bb(bc(x1)))) (41)
cc(ca(aa(ab(bb(ba(x1)))))) → cc(cb(bb(ba(x1)))) (42)
bd(dd(da(aa(ab(x1))))) → bc(cc(cd(dd(db(x1))))) (43)
bd(dd(da(aa(ad(x1))))) → bc(cc(cd(dd(dd(x1))))) (44)
bd(dd(da(aa(ac(x1))))) → bc(cc(cd(dd(dc(x1))))) (45)
bd(dd(da(aa(aa(x1))))) → bc(cc(cd(dd(da(x1))))) (46)
dd(dd(da(aa(ab(x1))))) → dc(cc(cd(dd(db(x1))))) (47)
dd(dd(da(aa(ad(x1))))) → dc(cc(cd(dd(dd(x1))))) (48)
dd(dd(da(aa(ac(x1))))) → dc(cc(cd(dd(dc(x1))))) (49)
dd(dd(da(aa(aa(x1))))) → dc(cc(cd(dd(da(x1))))) (50)
cd(dd(da(aa(ab(x1))))) → cc(cc(cd(dd(db(x1))))) (51)
cd(dd(da(aa(ad(x1))))) → cc(cc(cd(dd(dd(x1))))) (52)
cd(dd(da(aa(ac(x1))))) → cc(cc(cd(dd(dc(x1))))) (53)
cd(dd(da(aa(aa(x1))))) → cc(cc(cd(dd(da(x1))))) (54)
ad(dd(da(aa(ab(x1))))) → ac(cc(cd(dd(db(x1))))) (55)
ad(dd(da(aa(ad(x1))))) → ac(cc(cd(dd(dd(x1))))) (56)
ad(dd(da(aa(ac(x1))))) → ac(cc(cd(dd(dc(x1))))) (57)
ad(dd(da(aa(aa(x1))))) → ac(cc(cd(dd(da(x1))))) (58)
bb(bb(bb(bb(bb(bb(bb(x1))))))) → bc(cc(cb(bb(ba(aa(ab(x1))))))) (59)
bb(bb(bb(bb(bb(bb(bd(x1))))))) → bc(cc(cb(bb(ba(aa(ad(x1))))))) (60)
bb(bb(bb(bb(bb(bb(bc(x1))))))) → bc(cc(cb(bb(ba(aa(ac(x1))))))) (61)
bb(bb(bb(bb(bb(bb(ba(x1))))))) → bc(cc(cb(bb(ba(aa(aa(x1))))))) (62)
db(bb(bb(bb(bb(bb(bb(x1))))))) → dc(cc(cb(bb(ba(aa(ab(x1))))))) (63)
db(bb(bb(bb(bb(bb(bd(x1))))))) → dc(cc(cb(bb(ba(aa(ad(x1))))))) (64)
db(bb(bb(bb(bb(bb(bc(x1))))))) → dc(cc(cb(bb(ba(aa(ac(x1))))))) (65)
db(bb(bb(bb(bb(bb(ba(x1))))))) → dc(cc(cb(bb(ba(aa(aa(x1))))))) (66)
cb(bb(bb(bb(bb(bb(bb(x1))))))) → cc(cc(cb(bb(ba(aa(ab(x1))))))) (67)
cb(bb(bb(bb(bb(bb(bd(x1))))))) → cc(cc(cb(bb(ba(aa(ad(x1))))))) (68)
cb(bb(bb(bb(bb(bb(bc(x1))))))) → cc(cc(cb(bb(ba(aa(ac(x1))))))) (69)
cb(bb(bb(bb(bb(bb(ba(x1))))))) → cc(cc(cb(bb(ba(aa(aa(x1))))))) (70)
ab(bb(bb(bb(bb(bb(bb(x1))))))) → ac(cc(cb(bb(ba(aa(ab(x1))))))) (71)
ab(bb(bb(bb(bb(bb(bd(x1))))))) → ac(cc(cb(bb(ba(aa(ad(x1))))))) (72)
ab(bb(bb(bb(bb(bb(bc(x1))))))) → ac(cc(cb(bb(ba(aa(ac(x1))))))) (73)
ab(bb(bb(bb(bb(bb(ba(x1))))))) → ac(cc(cb(bb(ba(aa(aa(x1))))))) (74)
bc(cc(cd(dd(db(x1))))) → bd(dd(db(bb(bb(x1))))) (75)
bc(cc(cd(dd(dd(x1))))) → bd(dd(db(bb(bd(x1))))) (76)
bc(cc(cd(dd(dc(x1))))) → bd(dd(db(bb(bc(x1))))) (77)
bc(cc(cd(dd(da(x1))))) → bd(dd(db(bb(ba(x1))))) (78)
dc(cc(cd(dd(db(x1))))) → dd(dd(db(bb(bb(x1))))) (79)
dc(cc(cd(dd(dd(x1))))) → dd(dd(db(bb(bd(x1))))) (80)
dc(cc(cd(dd(dc(x1))))) → dd(dd(db(bb(bc(x1))))) (81)
dc(cc(cd(dd(da(x1))))) → dd(dd(db(bb(ba(x1))))) (82)
cc(cc(cd(dd(db(x1))))) → cd(dd(db(bb(bb(x1))))) (83)
cc(cc(cd(dd(dd(x1))))) → cd(dd(db(bb(bd(x1))))) (84)
cc(cc(cd(dd(dc(x1))))) → cd(dd(db(bb(bc(x1))))) (85)
cc(cc(cd(dd(da(x1))))) → cd(dd(db(bb(ba(x1))))) (86)
ac(cc(cd(dd(db(x1))))) → ad(dd(db(bb(bb(x1))))) (87)
ac(cc(cd(dd(dd(x1))))) → ad(dd(db(bb(bd(x1))))) (88)
ac(cc(cd(dd(dc(x1))))) → ad(dd(db(bb(bc(x1))))) (89)
ac(cc(cd(dd(da(x1))))) → ad(dd(db(bb(ba(x1))))) (90)
bc(cc(cd(dd(db(x1))))) → bd(dd(db(bb(bd(dd(db(x1))))))) (91)
bc(cc(cd(dd(dd(x1))))) → bd(dd(db(bb(bd(dd(dd(x1))))))) (92)
bc(cc(cd(dd(dc(x1))))) → bd(dd(db(bb(bd(dd(dc(x1))))))) (93)
bc(cc(cd(dd(da(x1))))) → bd(dd(db(bb(bd(dd(da(x1))))))) (94)
dc(cc(cd(dd(db(x1))))) → dd(dd(db(bb(bd(dd(db(x1))))))) (95)
dc(cc(cd(dd(dd(x1))))) → dd(dd(db(bb(bd(dd(dd(x1))))))) (96)
dc(cc(cd(dd(dc(x1))))) → dd(dd(db(bb(bd(dd(dc(x1))))))) (97)
dc(cc(cd(dd(da(x1))))) → dd(dd(db(bb(bd(dd(da(x1))))))) (98)
cc(cc(cd(dd(db(x1))))) → cd(dd(db(bb(bd(dd(db(x1))))))) (99)
cc(cc(cd(dd(dd(x1))))) → cd(dd(db(bb(bd(dd(dd(x1))))))) (100)
cc(cc(cd(dd(dc(x1))))) → cd(dd(db(bb(bd(dd(dc(x1))))))) (101)
cc(cc(cd(dd(da(x1))))) → cd(dd(db(bb(bd(dd(da(x1))))))) (102)
ac(cc(cd(dd(db(x1))))) → ad(dd(db(bb(bd(dd(db(x1))))))) (103)
ac(cc(cd(dd(dd(x1))))) → ad(dd(db(bb(bd(dd(dd(x1))))))) (104)
ac(cc(cd(dd(dc(x1))))) → ad(dd(db(bb(bd(dd(dc(x1))))))) (105)
ac(cc(cd(dd(da(x1))))) → ad(dd(db(bb(bd(dd(da(x1))))))) (106)
bc(cc(ca(aa(ad(dd(db(x1))))))) → bb(bb(bb(bb(bb(x1))))) (107)
bc(cc(ca(aa(ad(dd(dd(x1))))))) → bb(bb(bb(bb(bd(x1))))) (108)
bc(cc(ca(aa(ad(dd(dc(x1))))))) → bb(bb(bb(bb(bc(x1))))) (109)
bc(cc(ca(aa(ad(dd(da(x1))))))) → bb(bb(bb(bb(ba(x1))))) (110)
dc(cc(ca(aa(ad(dd(db(x1))))))) → db(bb(bb(bb(bb(x1))))) (111)
dc(cc(ca(aa(ad(dd(dd(x1))))))) → db(bb(bb(bb(bd(x1))))) (112)
dc(cc(ca(aa(ad(dd(dc(x1))))))) → db(bb(bb(bb(bc(x1))))) (113)
dc(cc(ca(aa(ad(dd(da(x1))))))) → db(bb(bb(bb(ba(x1))))) (114)
cc(cc(ca(aa(ad(dd(db(x1))))))) → cb(bb(bb(bb(bb(x1))))) (115)
cc(cc(ca(aa(ad(dd(dd(x1))))))) → cb(bb(bb(bb(bd(x1))))) (116)
cc(cc(ca(aa(ad(dd(dc(x1))))))) → cb(bb(bb(bb(bc(x1))))) (117)
cc(cc(ca(aa(ad(dd(da(x1))))))) → cb(bb(bb(bb(ba(x1))))) (118)
ac(cc(ca(aa(ad(dd(db(x1))))))) → ab(bb(bb(bb(bb(x1))))) (119)
ac(cc(ca(aa(ad(dd(dd(x1))))))) → ab(bb(bb(bb(bd(x1))))) (120)
ac(cc(ca(aa(ad(dd(dc(x1))))))) → ab(bb(bb(bb(bc(x1))))) (121)
ac(cc(ca(aa(ad(dd(da(x1))))))) → ab(bb(bb(bb(ba(x1))))) (122)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[bb(x1)] = 1 · x1 + 1
[bd(x1)] = 1 · x1
[dd(x1)] = 1 · x1
[db(x1)] = 1 · x1 + 1
[dc(x1)] = 1 · x1
[cc(x1)] = 1 · x1 + 1
[cb(x1)] = 1 · x1
[cd(x1)] = 1 · x1 + 1
[bc(x1)] = 1 · x1
[ba(x1)] = 1 · x1
[ca(x1)] = 1 · x1 + 1
[aa(x1)] = 1 · x1 + 1
[ab(x1)] = 1 · x1 + 1
[da(x1)] = 1 · x1 + 2
[ad(x1)] = 1 · x1 + 1
[ac(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
bb(bd(dd(db(bb(bb(x1)))))) → bb(bd(dd(dc(cc(cb(x1)))))) (35)
cc(ca(aa(ab(bb(bb(x1)))))) → cc(cb(bb(bb(x1)))) (39)
cc(ca(aa(ab(bb(bd(x1)))))) → cc(cb(bb(bd(x1)))) (40)
cc(ca(aa(ab(bb(bc(x1)))))) → cc(cb(bb(bc(x1)))) (41)
cc(ca(aa(ab(bb(ba(x1)))))) → cc(cb(bb(ba(x1)))) (42)
bd(dd(da(aa(ab(x1))))) → bc(cc(cd(dd(db(x1))))) (43)
bd(dd(da(aa(ad(x1))))) → bc(cc(cd(dd(dd(x1))))) (44)
bd(dd(da(aa(ac(x1))))) → bc(cc(cd(dd(dc(x1))))) (45)
dd(dd(da(aa(ab(x1))))) → dc(cc(cd(dd(db(x1))))) (47)
dd(dd(da(aa(ad(x1))))) → dc(cc(cd(dd(dd(x1))))) (48)
dd(dd(da(aa(ac(x1))))) → dc(cc(cd(dd(dc(x1))))) (49)
cd(dd(da(aa(ab(x1))))) → cc(cc(cd(dd(db(x1))))) (51)
cd(dd(da(aa(ad(x1))))) → cc(cc(cd(dd(dd(x1))))) (52)
cd(dd(da(aa(ac(x1))))) → cc(cc(cd(dd(dc(x1))))) (53)
ad(dd(da(aa(ab(x1))))) → ac(cc(cd(dd(db(x1))))) (55)
ad(dd(da(aa(ad(x1))))) → ac(cc(cd(dd(dd(x1))))) (56)
ad(dd(da(aa(ac(x1))))) → ac(cc(cd(dd(dc(x1))))) (57)
bb(bb(bb(bb(bb(bb(bb(x1))))))) → bc(cc(cb(bb(ba(aa(ab(x1))))))) (59)
bb(bb(bb(bb(bb(bb(bd(x1))))))) → bc(cc(cb(bb(ba(aa(ad(x1))))))) (60)
bb(bb(bb(bb(bb(bb(bc(x1))))))) → bc(cc(cb(bb(ba(aa(ac(x1))))))) (61)
bb(bb(bb(bb(bb(bb(ba(x1))))))) → bc(cc(cb(bb(ba(aa(aa(x1))))))) (62)
db(bb(bb(bb(bb(bb(bb(x1))))))) → dc(cc(cb(bb(ba(aa(ab(x1))))))) (63)
db(bb(bb(bb(bb(bb(bd(x1))))))) → dc(cc(cb(bb(ba(aa(ad(x1))))))) (64)
db(bb(bb(bb(bb(bb(bc(x1))))))) → dc(cc(cb(bb(ba(aa(ac(x1))))))) (65)
db(bb(bb(bb(bb(bb(ba(x1))))))) → dc(cc(cb(bb(ba(aa(aa(x1))))))) (66)
cb(bb(bb(bb(bb(bb(bb(x1))))))) → cc(cc(cb(bb(ba(aa(ab(x1))))))) (67)
ab(bb(bb(bb(bb(bb(bb(x1))))))) → ac(cc(cb(bb(ba(aa(ab(x1))))))) (71)
ab(bb(bb(bb(bb(bb(bd(x1))))))) → ac(cc(cb(bb(ba(aa(ad(x1))))))) (72)
ab(bb(bb(bb(bb(bb(bc(x1))))))) → ac(cc(cb(bb(ba(aa(ac(x1))))))) (73)
ab(bb(bb(bb(bb(bb(ba(x1))))))) → ac(cc(cb(bb(ba(aa(aa(x1))))))) (74)
bc(cc(cd(dd(da(x1))))) → bd(dd(db(bb(ba(x1))))) (78)
dc(cc(cd(dd(da(x1))))) → dd(dd(db(bb(ba(x1))))) (82)
cc(cc(cd(dd(da(x1))))) → cd(dd(db(bb(ba(x1))))) (86)
ac(cc(cd(dd(da(x1))))) → ad(dd(db(bb(ba(x1))))) (90)
bc(cc(ca(aa(ad(dd(da(x1))))))) → bb(bb(bb(bb(ba(x1))))) (110)
dc(cc(ca(aa(ad(dd(da(x1))))))) → db(bb(bb(bb(ba(x1))))) (114)
cc(cc(ca(aa(ad(dd(db(x1))))))) → cb(bb(bb(bb(bb(x1))))) (115)
cc(cc(ca(aa(ad(dd(dd(x1))))))) → cb(bb(bb(bb(bd(x1))))) (116)
cc(cc(ca(aa(ad(dd(dc(x1))))))) → cb(bb(bb(bb(bc(x1))))) (117)
cc(cc(ca(aa(ad(dd(da(x1))))))) → cb(bb(bb(bb(ba(x1))))) (118)
ac(cc(ca(aa(ad(dd(db(x1))))))) → ab(bb(bb(bb(bb(x1))))) (119)
ac(cc(ca(aa(ad(dd(dd(x1))))))) → ab(bb(bb(bb(bd(x1))))) (120)
ac(cc(ca(aa(ad(dd(dc(x1))))))) → ab(bb(bb(bb(bc(x1))))) (121)
ac(cc(ca(aa(ad(dd(da(x1))))))) → ab(bb(bb(bb(ba(x1))))) (122)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

There are 186 ruless (increase limit for explicit display).

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.