Certification Problem

Input (TPDB SRS_Relative/Mixed_relative_SRS/zr13)

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

a(b(c(x1))) → c(x1) (1)

and S is the following TRS.

c(x1) → c(b(a(x1))) (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 = c(b(c(x9)))
→S c(b(a(b(c(x9)))))
→R c(b(c(x9)))
= t2
where t2 = t0σ and σ = {x9/x9}