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.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ 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)
L(x1) → n(L(x1)) (15)
R(x1) → R(n(x1)) (16)

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 8 · x1 + -∞
[o(x1)] = 1 · x1 + -∞
[n(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[l(x1)] = 0 · x1 + -∞
[r(x1)] = 0 · 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 linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[L(x1)] =
1 0 1
0 0 1
1 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[o(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[n(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[R(x1)] =
1 1 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[l(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[r(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
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 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers
[L(x1)] = 8 · x1 + -∞
[o(x1)] = 6 · x1 + -∞
[n(x1)] = 0 · x1 + -∞
[R(x1)] = 0 · x1 + -∞
[l(x1)] = 8 · x1 + -∞
[r(x1)] = 0 · 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.1 R is empty

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