Cyclic proofs and size-change termination

A cyclic proof is a regular infinite proof tree with a global condition, and it is known that, under arithmetic, cyclic proofs with inductive definitions are equivalent to proofs with induction. A way to show this equivalence is by constructing a well-founded relation on tuples of natural numbers and then transforming a cyclic proof into a proof by well-founded induction with the relation. In this paper, we see the connection between cyclic proofs and size-change termination (SCT) of programs, and it provides a new well-founded relation for proof transformation.