Certification Problem
Input (TPDB TRS_Relative/Relative_05/rt3-6)
The relative rewrite relation R/S is considered where R is the following TRS
and S is the following TRS.
|
b(x) |
→ |
b(b(x)) |
(2) |
|
a(x) |
→ |
a(a(x)) |
(3) |
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by AProVE @ termCOMP 2023)
1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRSs
and
|
b(x) |
→ |
b(b(x)) |
(2) |
|
a(x) |
→ |
a(a(x)) |
(3) |
1.1 Loop
The following loop proves that R/S is not relative terminating.
| t0
|
= |
a(b(x')) |
|
→S
|
a(b(b(x'))) |
|
→R
|
b(a(b(x'))) |
|
= |
t2
|
where t2 =
C[t0σ]
and
σ =
{x'/x'}
and
C = b(☐)