Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z023)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
a(a(a(b(x1)))) → a(b(a(b(x1)))) (4)
b(a(a(b(x1)))) → b(b(a(b(x1)))) (5)
c(a(a(b(x1)))) → c(b(a(b(x1)))) (6)
a(b(a(x1))) → a(a(b(b(x1)))) (7)
b(b(a(x1))) → b(a(b(b(x1)))) (8)
c(b(a(x1))) → c(a(b(b(x1)))) (9)
a(b(c(a(x1)))) → a(c(c(a(a(b(x1)))))) (10)
b(b(c(a(x1)))) → b(c(c(a(a(b(x1)))))) (11)
c(b(c(a(x1)))) → c(c(c(a(a(b(x1)))))) (12)

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Rule Removal

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

1.1.1.1 Dependency Pair Transformation

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

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals
[aa#(x1)] = 1 · x1
[aa(x1)] = 1 + 1 · x1
[ab(x1)] = 1 · x1
[ba(x1)] = 1 + 1 · x1
[ab#(x1)] = 1 · x1
[ba#(x1)] = 1 + 1 · x1
[bb(x1)] = 1 · x1
[bc(x1)] = 1 + 1 · x1
[bb#(x1)] = 1 · x1
[ca#(x1)] = 1 · x1
[cb#(x1)] = 1 · x1
[ac(x1)] = 1 + 1 · x1
[ca(x1)] = 1 · x1
[cc(x1)] = 0
[cb(x1)] = 0
together with the usable rules
bb(ba(aa(x1))) → ba(ab(bb(ba(x1)))) (25)
ba(aa(ab(ba(x1)))) → bb(ba(ab(ba(x1)))) (16)
bb(ba(ab(x1))) → ba(ab(bb(bb(x1)))) (26)
ba(aa(ab(bb(x1)))) → bb(ba(ab(bb(x1)))) (17)
bb(ba(ac(x1))) → ba(ab(bb(bc(x1)))) (27)
ba(aa(ab(bc(x1)))) → bb(ba(ab(bc(x1)))) (18)
ab(ba(aa(x1))) → aa(ab(bb(ba(x1)))) (22)
aa(aa(ab(ba(x1)))) → ab(ba(ab(ba(x1)))) (13)
ab(ba(ab(x1))) → aa(ab(bb(bb(x1)))) (23)
aa(aa(ab(bb(x1)))) → ab(ba(ab(bb(x1)))) (14)
ab(ba(ac(x1))) → aa(ab(bb(bc(x1)))) (24)
aa(aa(ab(bc(x1)))) → ab(ba(ab(bc(x1)))) (15)
ab(bc(ca(aa(x1)))) → ac(cc(ca(aa(ab(ba(x1)))))) (31)
ab(bc(ca(ab(x1)))) → ac(cc(ca(aa(ab(bb(x1)))))) (32)
ab(bc(ca(ac(x1)))) → ac(cc(ca(aa(ab(bc(x1)))))) (33)
bb(bc(ca(aa(x1)))) → bc(cc(ca(aa(ab(ba(x1)))))) (34)
bb(bc(ca(ab(x1)))) → bc(cc(ca(aa(ab(bb(x1)))))) (35)
bb(bc(ca(ac(x1)))) → bc(cc(ca(aa(ab(bc(x1)))))) (36)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
ba#(aa(ab(ba(x1)))) → bb#(ba(ab(ba(x1)))) (46)
ba#(aa(ab(ba(x1)))) → ba#(ab(ba(x1))) (47)
ba#(aa(ab(bb(x1)))) → bb#(ba(ab(bb(x1)))) (48)
ba#(aa(ab(bb(x1)))) → ba#(ab(bb(x1))) (49)
ba#(aa(ab(bc(x1)))) → bb#(ba(ab(bc(x1)))) (50)
ba#(aa(ab(bc(x1)))) → ba#(ab(bc(x1))) (51)
ab#(ba(aa(x1))) → aa#(ab(bb(ba(x1)))) (58)
ab#(ba(aa(x1))) → ab#(bb(ba(x1))) (59)
ab#(ba(aa(x1))) → bb#(ba(x1)) (60)
ab#(ba(aa(x1))) → ba#(x1) (61)
ab#(ba(ab(x1))) → aa#(ab(bb(bb(x1)))) (62)
ab#(ba(ab(x1))) → ab#(bb(bb(x1))) (63)
ab#(ba(ab(x1))) → bb#(bb(x1)) (64)
ab#(ba(ab(x1))) → bb#(x1) (65)
ab#(ba(ac(x1))) → aa#(ab(bb(bc(x1)))) (66)
ab#(ba(ac(x1))) → ab#(bb(bc(x1))) (67)
ab#(ba(ac(x1))) → bb#(bc(x1)) (68)
bb#(ba(aa(x1))) → ab#(bb(ba(x1))) (70)
bb#(ba(aa(x1))) → bb#(ba(x1)) (71)
bb#(ba(aa(x1))) → ba#(x1) (72)
bb#(ba(ab(x1))) → ab#(bb(bb(x1))) (74)
bb#(ba(ab(x1))) → bb#(bb(x1)) (75)
bb#(ba(ab(x1))) → bb#(x1) (76)
bb#(ba(ac(x1))) → ab#(bb(bc(x1))) (78)
bb#(ba(ac(x1))) → bb#(bc(x1)) (79)
cb#(ba(aa(x1))) → ca#(ab(bb(ba(x1)))) (80)
cb#(ba(aa(x1))) → ab#(bb(ba(x1))) (81)
cb#(ba(aa(x1))) → bb#(ba(x1)) (82)
cb#(ba(aa(x1))) → ba#(x1) (83)
cb#(ba(ab(x1))) → ca#(ab(bb(bb(x1)))) (84)
cb#(ba(ab(x1))) → ab#(bb(bb(x1))) (85)
cb#(ba(ab(x1))) → bb#(bb(x1)) (86)
cb#(ba(ab(x1))) → bb#(x1) (87)
cb#(ba(ac(x1))) → ca#(ab(bb(bc(x1)))) (88)
cb#(ba(ac(x1))) → ab#(bb(bc(x1))) (89)
cb#(ba(ac(x1))) → bb#(bc(x1)) (90)
ab#(bc(ca(aa(x1)))) → aa#(ab(ba(x1))) (92)
ab#(bc(ca(aa(x1)))) → ab#(ba(x1)) (93)
ab#(bc(ca(aa(x1)))) → ba#(x1) (94)
ab#(bc(ca(ab(x1)))) → aa#(ab(bb(x1))) (96)
ab#(bc(ca(ab(x1)))) → ab#(bb(x1)) (97)
ab#(bc(ca(ab(x1)))) → bb#(x1) (98)
ab#(bc(ca(ac(x1)))) → aa#(ab(bc(x1))) (100)
ab#(bc(ca(ac(x1)))) → ab#(bc(x1)) (101)
bb#(bc(ca(aa(x1)))) → aa#(ab(ba(x1))) (103)
bb#(bc(ca(aa(x1)))) → ab#(ba(x1)) (104)
bb#(bc(ca(aa(x1)))) → ba#(x1) (105)
bb#(bc(ca(ab(x1)))) → aa#(ab(bb(x1))) (107)
bb#(bc(ca(ab(x1)))) → ab#(bb(x1)) (108)
bb#(bc(ca(ab(x1)))) → bb#(x1) (109)
bb#(bc(ca(ac(x1)))) → aa#(ab(bc(x1))) (111)
bb#(bc(ca(ac(x1)))) → ab#(bc(x1)) (112)
could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.