Certification Problem

Input (TPDB TRS_Standard/SK90/4.35)

The rewrite relation of the following TRS is considered.

a(b(x)) a(c(b(x))) (1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 1. This is shown by the following automaton.