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.
|
a(x) |
→ |
a(a(x)) |
(2) |
|
b(x) |
→ |
b(b(x)) |
(3) |
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by ttt2 @ termCOMP 2023)
1 Loop
The following loop proves that R/S is not relative terminating.
| t0
|
= |
b(a(x18)) |
|
→S
|
b(b(a(x18))) |
|
→R
|
b(a(b(x18))) |
|
= |
t2
|
where t2 =
t0σ
and
σ =
{x18/b(x18)}