Certification Problem

Input (TPDB TRS_Relative/Relative_05/rt2-7)

The relative rewrite relation R/S is considered where R is the following TRS

f(g(f(x))) → f(g(g(g(f(x))))) (1)

and S is the following TRS.

g(x) → g(g(x)) (2)

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
f(g(f(x))) → f(g(g(g(f(x))))) (1)
g(x) → g(g(x)) (2)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
fg(gf(ff(x))) → fg(gg(gg(gf(ff(x))))) (3)
fg(gf(fg(x))) → fg(gg(gg(gf(fg(x))))) (4)
gf(x) → gg(gf(x)) (5)
gg(x) → gg(gg(x)) (6)

1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fg(x1)] =
0
0
+
2 2
2 2
· x1
[gf(x1)] =
0
0
+
2 2
2 2
· x1
[ff(x1)] =
2
2
+
1 0
0 0
· x1
[gg(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
fg(gf(ff(x))) → fg(gg(gg(gf(ff(x))))) (3)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fg(x1)] =
0
0
+
2 2
0 0
· x1
[gf(x1)] =
2
2
+
1 0
0 0
· x1
[gg(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
fg(gf(fg(x))) → fg(gg(gg(gf(fg(x))))) (4)

1.1.1.1.1 R is empty

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