A Precise Characterization of Extended Tail-recursive
Technical Report TR-08-47, Department of Computer Sciences, University
of Texas at Austin, November 2008.
Extended tail-recursive definitional equations are definitional
equations involving quantification and tail-recursion that can be
introduced in the logic of the ACL2 theorem prover. This paper
corrects a previous mistake by the author in the characterization of
extended tail-recursive definitions, and provides a precise
characterization of such definitions.