  This paper shows how to use Lee, Jones and Ben Amram's size-change principle
to check correctness of arbitrary recursive definitions in an ML / Haskell like
programming language with inductive and coinductive types.Naively using the
size-change principle to check productivity and termination is straightforward
but unsound when inductive and coinductive types arenested. We can however
adapt the size-change principle to check ``totality'', which corresponds
exactly to correctness with respect to the corresponding (co)inductive type.
