Backhouse, R., & Doornbos, H. (2008). Datatype-generic termination proofs. Theory of Computing Systems, 43(3-4), https://doi.org/10.1007/s00224-007-9056-z