		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-terminates-fn

Generate the termination testing predicate definition.

Signature
(defarbrec-gen-terminates-fn x1...xn$ test update-names$ terminates-name$ terminates-witness-name$ terminates-rewrite-name$ k wrld) → event
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; test — Guard (pseudo-termp test).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; terminates-witness-name$ — Guard (symbolp terminates-witness-name$).; terminates-rewrite-name$ — Guard (symbolp terminates-rewrite-name$).; k — Guard (symbolp k).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.

This is the predicate terminates in the documentation. It corresponds to the function tt in the template.

The names of the witness and rewrite rule calculated by defarbrec-process-terminates-name are the same as the defun-sk default ones. But by setting them explicitly, we make them easier to change in the future.

We set :quant-ok to t, in case.

Definitions and Theorems

Function: defarbrec-gen-terminates-fn

(defun defarbrec-gen-terminates-fn
       (x1...xn$ test update-names$ terminates-name$
                 terminates-witness-name$
                 terminates-rewrite-name$ k wrld)
 (declare (xargs :guard (and (symbol-listp x1...xn$)
                             (pseudo-termp test)
                             (symbol-listp update-names$)
                             (symbolp terminates-name$)
                             (symbolp terminates-witness-name$)
                             (symbolp terminates-rewrite-name$)
                             (symbolp k)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-terminates-fn))
  (declare (ignorable __function__))
  (b* ((test-of-updates-k (defarbrec-gen-test-of-updates-term
                               x1...xn$ test update-names$ k))
       (test-of-updates-k (untranslate test-of-updates-k nil wrld)))
   (cons
    'defun-sk
    (cons
       terminates-name$
       (cons x1...xn$
             (cons (cons 'exists
                         (cons k (cons test-of-updates-k 'nil)))
                   (cons ':skolem-name
                         (cons terminates-witness-name$
                               (cons ':thm-name
                                     (cons terminates-rewrite-name$
                                           '(:quant-ok t))))))))))))