Proving termination with transition invariants of height omega

Stefano Berardi, Paulo Oliva, Silvia Steila

The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose trans…