Quantification in tail-recursive function definitions
Sandip Kumar Ray · 2006
We investigate the logical issues behind axiomatizing equations that contain both recursive calls and quantifiers in ACL2. We identify a class of such equations, named extended tail-recursive equations, that can be uniformly introduced in the logic. We point out some potential benefits of this axiomatization, and discuss the logical impediments behind introducing more general quantified formulas.