Consider the following statement that appeared in Lee's Ranking functions for size-change termination.
Let $G$ satisfy the SCT condition.
There is an effective procedure to construct a $G$-ranking function expressed using only min, max and lexicographic tuples of program parameters and constants.
I'm interested mostly in the computational side of it. Has this been implemented before? If so in which systems?
In fact, Lee's preliminar algorithm was made more practical by subsequent revisions in joint work with Ben-Amram and Codish. There remains the question of whether their claim complexity is aceptable in current verifiers and whether it has been tested in practice yet.