		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-termination-hints

Generate the hints to prove the termination of the new function, if recursive.

Signature
(isodata-gen-new-fn-termination-hints appcond-thm-names old$ arg-isomaps wrld) → hints
Arguments: appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; wrld — Guard (plist-worldp wrld).
Returns: hints — A true-listp.

Definitions and Theorems

Function: isodata-gen-new-fn-termination-hints

(defun isodata-gen-new-fn-termination-hints
       (appcond-thm-names old$ arg-isomaps wrld)
 (declare
      (xargs :guard (and (symbol-symbol-alistp appcond-thm-names)
                         (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (plist-worldp wrld))))
 (let ((__function__ 'isodata-gen-new-fn-termination-hints))
  (declare (ignorable __function__))
  (b*
   ((rec-calls (recursive-calls old$ wrld))
    (oldp-of-rec-call-args
         (cdr (assoc-eq :oldp-of-rec-call-args appcond-thm-names)))
    (instance-termination-thm-old (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
                                       (cons ':termination-theorem
                                             (cons old$ 'nil))
                                       old$ arg-isomaps wrld))
    (instances-back-image
     (isodata-gen-back-image-instances-to-x1...xn arg-isomaps wrld))
    (instance-oldp-of-rec-call-args (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
                                         oldp-of-rec-call-args
                                         old$ arg-isomaps wrld))
    (instances-back-of-forth (isodata-gen-all-back-of-forth-instances-to-terms-back
                                  rec-calls old$ arg-isomaps wrld)))
   (cons
    (cons
     '"Goal"
     (cons
      ':in-theory
      (cons
       'nil
       (cons
            ':use
            (cons (cons instance-termination-thm-old
                        (append instances-back-image
                                (cons instance-oldp-of-rec-call-args
                                      instances-back-of-forth)))
                  'nil)))))
    'nil))))