Generate the theorem asserting that
the recursion exit test succeeds on the result of
(tailrec-gen-test-of-alpha-thm old$ test alpha-name names-to-avoid wrld) → (mv event name updated-names-to-avoid)
The theorem's formula is
The hints follow the proof in the design notes.
Since the theorem involves nth applied to cons,
we enable the built-in theorems
This theorem is local, because it is just a lemma used to prove other theorems.
Function:
(defun tailrec-gen-test-of-alpha-thm (old$ test alpha-name names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp test) (symbolp alpha-name) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-test-of-alpha-thm)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'test-of-alpha nil names-to-avoid wrld)) (formals (formals old$ wrld)) (alpha-component-terms (tailrec-gen-alpha-component-terms alpha-name old$ wrld)) (formula (subcor-var formals alpha-component-terms test)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons alpha-name '(nth-0-cons nth-add1)) 'nil)) (cons ':induct (cons (cons alpha-name formals) 'nil))))) 'nil)) (event (cons 'local (cons (cons 'defthm (cons name (cons formula (cons ':rule-classes (cons 'nil (cons ':hints (cons hints 'nil))))))) 'nil)))) (mv event name names-to-avoid))))