Certification Problem

Input (TPDB TRS_Relative/INVY_15/ex1)

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

a → b (1)

and S is the following TRS.

b → a (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 = a
→R b
→S a
= t2
where t2 = t0