Certification Problem
Input (TPDB TRS_Relative/Relative_05/rt3-3)
The relative rewrite relation R/S is considered where R is the following TRS
|
p(0,y) |
→ |
y |
(1) |
|
p(s(x),y) |
→ |
s(p(x,y)) |
(2) |
and S is the following TRS.
Property / Task
Prove or disprove termination.Answer / Result
No.Proof (by AProVE @ termCOMP 2023)
1 Loop
The following loop proves that R/S is not relative terminating.
| t0
|
= |
p(p(x',y'),y) |
|
→S
|
p(s(p(x',y')),y) |
|
→R
|
s(p(p(x',y'),y)) |
|
= |
t2
|
where t2 =
C[t0]
and
C = s(☐)