Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z118)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
a(a(x1)) → a(g(d(x1))) (6)
g(a(x1)) → g(g(d(x1))) (7)
d(a(x1)) → d(g(d(x1))) (8)
b(a(x1)) → b(g(d(x1))) (9)
c(a(x1)) → c(g(d(x1))) (10)
a(b(b(b(x1)))) → a(c(d(c(x1)))) (11)
g(b(b(b(x1)))) → g(c(d(c(x1)))) (12)
d(b(b(b(x1)))) → d(c(d(c(x1)))) (13)
b(b(b(b(x1)))) → b(c(d(c(x1)))) (14)
c(b(b(b(x1)))) → c(c(d(c(x1)))) (15)
a(b(b(x1))) → a(a(g(g(x1)))) (16)
g(b(b(x1))) → g(a(g(g(x1)))) (17)
d(b(b(x1))) → d(a(g(g(x1)))) (18)
b(b(b(x1))) → b(a(g(g(x1)))) (19)
c(b(b(x1))) → c(a(g(g(x1)))) (20)
a(c(d(x1))) → a(g(g(x1))) (21)
g(c(d(x1))) → g(g(g(x1))) (22)
d(c(d(x1))) → d(g(g(x1))) (23)
b(c(d(x1))) → b(g(g(x1))) (24)
c(c(d(x1))) → c(g(g(x1))) (25)
a(g(g(g(x1)))) → a(b(b(x1))) (26)
g(g(g(g(x1)))) → g(b(b(x1))) (27)
d(g(g(g(x1)))) → d(b(b(x1))) (28)
b(g(g(g(x1)))) → b(b(b(x1))) (29)
c(g(g(g(x1)))) → c(b(b(x1))) (30)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1 + 21
[ag(x1)] = 1 · x1 + 38
[gd(x1)] = 1 · x1 + 2
[da(x1)] = 1 · x1
[dg(x1)] = 1 · x1 + 17
[ad(x1)] = 1 · x1 + 20
[dd(x1)] = 1 · x1
[ab(x1)] = 1 · x1 + 52
[db(x1)] = 1 · x1 + 31
[ac(x1)] = 1 · x1 + 70
[dc(x1)] = 1 · x1 + 50
[ga(x1)] = 1 · x1 + 7
[gg(x1)] = 1 · x1 + 24
[ba(x1)] = 1 · x1 + 4
[bg(x1)] = 1 · x1 + 22
[ca(x1)] = 1 · x1 + 4
[cg(x1)] = 1 · x1 + 22
[bb(x1)] = 1 · x1 + 35
[cd(x1)] = 1 · x1
[bd(x1)] = 1 · x1
[cb(x1)] = 1 · x1 + 35
[bc(x1)] = 1 · x1 + 54
[cc(x1)] = 1 · x1 + 54
[gb(x1)] = 1 · x1 + 38
[gc(x1)] = 1 · x1 + 57
all of the following rules can be deleted.

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[ba(x1)] = 1 · x1 + 1
[ad(x1)] = 1 · x1
[bg(x1)] = 1 · x1
[gd(x1)] = 1 · x1
[dd(x1)] = 1 · x1
[ac(x1)] = 1 · x1
[dc(x1)] = 1 · x1
[ca(x1)] = 1 · x1 + 1
[cg(x1)] = 1 · x1
all of the following rules can be deleted.
ba(ad(x1)) → bg(gd(dd(x1))) (48)
ba(ac(x1)) → bg(gd(dc(x1))) (50)
ca(ad(x1)) → cg(gd(dd(x1))) (53)
ca(ac(x1)) → cg(gd(dc(x1))) (55)

1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.