Certification Problem

Input (TPDB TRS_Relative/INVY_15/ex6)

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

a → b (1)

and S is the following TRS.

d → c(a,d) (2)

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 = d
→S c(a,d)
→R c(b,d)
= t2
where t2 = C[t0] and C = c(b,☐)