Email Gateway (Jul 17 2026 at 19:36): Email Gateway (Jul 17 2026 at 19:36):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Termination Restricted to Right-Forward Closures
Termination Restricted to Right-Forward Closures
René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze and Johannes Waldmann
In this AFP entry we formalize Dershowitz' theorem that termination of a term
rewrite system (TRS) starting from arbitrary terms is equivalent to termination
starting from terms in the right-forward closures of right-hand sides, provided
that the TRS is right-linear or orthogonal. Our proof deviates from the original
one in that no reorderings of steps in infinite derivations are required, making
it more precise in its argumentation. We also integrate a later result that one
can weaken orthogonality to locally confluent overlay TRSs.
In order to arrive at these statements, we had to formalize two further results:
Following Gramlich, we prove that for locally confluent overlay TRSs the notions
of termination and innermost termination coincide; and we verify that narrowing
with a right-linear TRS preserves linearity of terms.
For further details, we refer to our FSCD 2026 paper.
https://isa-afp.org/entries/Right_Forward_Closures.html
Enjoy more great TRS theory from the amazing René and his friends!
Last updated: Jul 22 2026 at 14:00 UTC