Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(aa(x1)) → aa(x1) (17)
aa(ab(x1)) → ab(x1) (18)
aa(ac(x1)) → ac(x1) (19)
ba(aa(x1)) → ba(x1) (20)
ba(ab(x1)) → bb(x1) (21)
ba(ac(x1)) → bc(x1) (22)
ca(aa(x1)) → ca(x1) (23)
ca(ab(x1)) → cb(x1) (24)
ca(ac(x1)) → cc(x1) (25)
aa(ab(ba(x1))) → ac(cb(bc(cb(ba(aa(x1)))))) (26)
aa(ab(bb(x1))) → ac(cb(bc(cb(ba(ab(x1)))))) (27)
aa(ab(bc(x1))) → ac(cb(bc(cb(ba(ac(x1)))))) (28)
ba(ab(ba(x1))) → bc(cb(bc(cb(ba(aa(x1)))))) (29)
ba(ab(bb(x1))) → bc(cb(bc(cb(ba(ab(x1)))))) (30)
ba(ab(bc(x1))) → bc(cb(bc(cb(ba(ac(x1)))))) (31)
ca(ab(ba(x1))) → cc(cb(bc(cb(ba(aa(x1)))))) (32)
ca(ab(bb(x1))) → cc(cb(bc(cb(ba(ab(x1)))))) (33)
ca(ab(bc(x1))) → cc(cb(bc(cb(ba(ac(x1)))))) (34)
ab(ba(x1)) → aa(aa(x1)) (35)
ab(bb(x1)) → aa(ab(x1)) (36)
ab(bc(x1)) → aa(ac(x1)) (37)
bb(ba(x1)) → ba(aa(x1)) (38)
bb(bb(x1)) → ba(ab(x1)) (39)
bb(bc(x1)) → ba(ac(x1)) (40)
cb(ba(x1)) → ca(aa(x1)) (41)
cb(bb(x1)) → ca(ab(x1)) (42)
cb(bc(x1)) → ca(ac(x1)) (43)
ac(cc(ca(x1))) → aa(x1) (44)
ac(cc(cb(x1))) → ab(x1) (45)
ac(cc(cc(x1))) → ac(x1) (46)
bc(cc(ca(x1))) → ba(x1) (47)
bc(cc(cb(x1))) → bb(x1) (48)
bc(cc(cc(x1))) → bc(x1) (49)
cc(cc(ca(x1))) → ca(x1) (50)
cc(cc(cb(x1))) → cb(x1) (51)
cc(cc(cc(x1))) → cc(x1) (52)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1
[ab(x1)] = 1 · x1 + 2
[ac(x1)] = 1 · x1
[ba(x1)] = 1 · x1
[bb(x1)] = 1 · x1 + 2
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1 + 1
[cb(x1)] = 1 · x1 + 1
[cc(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
ca(ab(x1)) → cb(x1) (24)
ab(ba(x1)) → aa(aa(x1)) (35)
ab(bb(x1)) → aa(ab(x1)) (36)
ab(bc(x1)) → aa(ac(x1)) (37)
bb(ba(x1)) → ba(aa(x1)) (38)
bb(bb(x1)) → ba(ab(x1)) (39)
bb(bc(x1)) → ba(ac(x1)) (40)
ac(cc(ca(x1))) → aa(x1) (44)
ac(cc(cc(x1))) → ac(x1) (46)
bc(cc(ca(x1))) → ba(x1) (47)
bc(cc(cc(x1))) → bc(x1) (49)
cc(cc(ca(x1))) → ca(x1) (50)
cc(cc(cb(x1))) → cb(x1) (51)
cc(cc(cc(x1))) → cc(x1) (52)

1.1.1.1 Dependency Pair Transformation

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

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.