Certification Problem

Input (TPDB SRS_Relative/Zantema_06_relative/rel13)

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

o(l(x1)) → r(x1) (1)
n(l(o(x1))) → r(o(x1)) (2)
L(l(o(x1))) → L(r(o(x1))) (3)
r(o(x1)) → l(x1) (4)
o(r(n(x1))) → o(l(x1)) (5)
o(r(R(x1))) → o(l(R(x1))) (6)

and S is the following TRS.

R(x1) → n(R(x1)) (7)
L(x1) → L(n(x1)) (8)

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
l(o(x1)) → r(x1) (9)
o(l(n(x1))) → o(r(x1)) (10)
o(l(L(x1))) → o(r(L(x1))) (11)
o(r(x1)) → l(x1) (12)
n(r(o(x1))) → l(o(x1)) (13)
R(r(o(x1))) → R(l(o(x1))) (14)
R(x1) → R(n(x1)) (15)
L(x1) → n(L(x1)) (16)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[l(x1)] = 1 · x1
[o(x1)] = 1 + 1 · x1
[r(x1)] = 1 · x1
[n(x1)] = 1 · x1
[L(x1)] = 1 · x1
[R(x1)] = 1 · x1
all of the following rules can be deleted.
l(o(x1)) → r(x1) (9)
o(r(x1)) → l(x1) (12)

1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[o(x1)] =
0
0
+
1 0
0 0
· x1
[l(x1)] =
2
0
+
1 0
0 0
· x1
[n(x1)] =
0
0
+
1 1
0 0
· x1
[r(x1)] =
1
1
+
1 0
2 0
· x1
[L(x1)] =
0
0
+
1 0
0 0
· x1
[R(x1)] =
0
2
+
1 1
0 2
· x1
all of the following rules can be deleted.
o(l(n(x1))) → o(r(x1)) (10)
o(l(L(x1))) → o(r(L(x1))) (11)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[n(x1)] = 1 · x1
[r(x1)] = 1 + 1 · x1
[o(x1)] = 1 · x1
[l(x1)] = 1 · x1
[R(x1)] = 1 · x1
[L(x1)] = 1 · x1
all of the following rules can be deleted.
n(r(o(x1))) → l(o(x1)) (13)
R(r(o(x1))) → R(l(o(x1))) (14)

1.1.1.1.1 R is empty

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