Generate the definition of the
(defarbrec-gen-fn-fn fn$ x1...xn$ body$ updates update-names$ terminates-name$ measure-name$ nonterminating$ k l measure-fn-natp-lemma-name measure-fn-end-lemma-name measure-fn-min-lemma-name wrld) → (mv local-event exported-event)
This is as described in the documentation. We wrap the body of the program-mode function into a check with the termination testing predicate.
This corresponds to the function
Function:
(defun defarbrec-gen-fn-fn (fn$ x1...xn$ body$ updates update-names$ terminates-name$ measure-name$ nonterminating$ k l measure-fn-natp-lemma-name measure-fn-end-lemma-name measure-fn-min-lemma-name wrld) (declare (xargs :guard (and (symbolp fn$) (symbol-listp x1...xn$) (pseudo-termp body$) (pseudo-term-listp updates) (symbol-listp update-names$) (symbolp terminates-name$) (symbolp measure-name$) (pseudo-termp nonterminating$) (symbolp k) (symbolp l) (symbolp measure-fn-natp-lemma-name) (symbolp measure-fn-end-lemma-name) (symbolp measure-fn-min-lemma-name) (plist-worldp wrld)))) (let ((__function__ 'defarbrec-gen-fn-fn)) (declare (ignorable __function__)) (b* ((measure (cons measure-name$ (append x1...xn$ '(0)))) (doublets (alist-to-doublets (pairlis$ x1...xn$ updates))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'o-p (cons 'o-finp (cons 'natp (cons 'o< (cons 'zp (cons 'nfix update-names$)))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons measure-fn-natp-lemma-name (cons (cons k '(0)) 'nil))) (cons (cons ':instance (cons measure-fn-natp-lemma-name (append doublets (cons (cons k '(0)) 'nil)))) (cons (cons ':instance (cons measure-fn-end-lemma-name (cons (cons k '(0)) 'nil))) (cons (cons ':instance (cons measure-fn-min-lemma-name (cons (cons l (cons (cons '1- (cons (cons measure-name$ (append x1...xn$ '(0))) 'nil)) 'nil)) (append doublets (cons (cons k '(0)) 'nil))))) 'nil)))) 'nil))))) 'nil)) (body (cons 'if (cons (cons terminates-name$ x1...xn$) (cons body$ (cons nonterminating$ 'nil))))) (body (untranslate body nil wrld)) (local-event (cons 'local (cons (cons 'defun (cons fn$ (cons x1...xn$ (cons (cons 'declare (cons (cons 'xargs (cons ':measure (cons measure (cons ':well-founded-relation (cons 'o< (cons ':hints (cons hints 'nil))))))) 'nil)) (cons body 'nil))))) 'nil))) (exported-event (cons 'defun (cons fn$ (cons x1...xn$ (cons (cons 'declare (cons (cons 'xargs (cons ':measure (cons measure '(:well-founded-relation o<)))) 'nil)) (cons body 'nil))))))) (mv local-event exported-event))))