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 AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRSs
c(b(a(x1))) → c(x1) (3)
and
c(x1) → a(b(c(x1))) (4)

1.1 Loop

The following loop proves that R/S is not relative terminating.

t0 = c(b(c(x1')))
→S c(b(a(b(c(x1')))))
→R c(b(c(x1')))
= t2
where t2 = t0σ and σ = {x1'/x1'}