defuns

(defun cert-data-pair
  (fn cert-data-entry)
  (and cert-data-entry (hons-get fn cert-data-entry)))

(defun cert-data-val
  (fn cert-data-entry)
  (let ((pair (and cert-data-entry (hons-get fn cert-data-entry))))
    (cdr pair)))

(defun cert-data-entry-pair
  (key state)
  (let ((cert-data (f-get-global 'cert-data state)))
    (and cert-data (assoc-eq key cert-data))))

(defun cert-data-entry
  (key state)
  (let ((cert-data (f-get-global 'cert-data state)))
    (and cert-data
      (not (f-get-global 'in-local-flg state))
      (int= (f-get-global 'make-event-debug-depth state) 0)
      (cdr (assoc-eq key cert-data)))))

(defun store-cert-data
  (listp val wrld state)
  (and (f-get-global 'certify-book-info state)
    (not (f-get-global 'in-local-flg state))
    (not (global-val 'include-book-path wrld))
    (not (and (in-encapsulatep (global-val 'embedded-event-lst wrld) nil)
        (not (eq (ld-skip-proofsp state) 'include-book))))
    (not (if listp
        (contains-lambda-object-listp val)
        (contains-lambda-objectp val)))
    (< (cons-count-bounded val) (fn-count-evg-max-val))))

(defun update-translate-cert-data-fn
  (name installed-wrld wrld type inputs value fns vars)
  (let* ((old-translate-cert-data (global-val 'translate-cert-data installed-wrld)) (new (make translate-cert-data-record
          :type type
          :inputs inputs
          :value value
          :fns fns
          :vars vars))
      (old-lst (cdr (assoc-eq name old-translate-cert-data))))
    (global-set 'translate-cert-data
      (acons name (cons new old-lst) old-translate-cert-data)
      wrld)))

(defun translate-bodies1
  (non-executablep names
    bodies
    bindings
    arglists
    stobjs-in-lst
    ctx
    wrld
    state-vars)
  (cond ((null bodies) (trans-value nil))
    (t (mv-let (erp x bindings2)
        (translate1-cmp+ (car bodies)
          (if non-executablep
            t
            (car names))
          (if non-executablep
            nil
            bindings)
          (collect-non-*-df (car stobjs-in-lst))
          (collect-by-position '(:df)
            (car stobjs-in-lst)
            (car arglists))
          (if (and (consp ctx)
              (equal (car ctx) *mutual-recursion-ctx-string*))
            (msg "( MUTUAL-RECURSION ... ( DEFUN ~x0 ...) ~
                                      ...)"
              (car names))
            ctx)
          wrld
          state-vars)
        (cond ((and erp (eq bindings2 :unknown-bindings)) (trans-er-let* ((y (translate-bodies1 non-executablep
                   (cdr names)
                   (cdr bodies)
                   bindings
                   (cdr arglists)
                   (cdr stobjs-in-lst)
                   ctx
                   wrld
                   state-vars)) (x (translate1-cmp+ (car bodies)
                    (if non-executablep
                      t
                      (car names))
                    (if non-executablep
                      nil
                      bindings)
                    (collect-non-*-df (car stobjs-in-lst))
                    (collect-by-position '(:df)
                      (car stobjs-in-lst)
                      (car arglists))
                    (if (and (consp ctx)
                        (equal (car ctx) *mutual-recursion-ctx-string*))
                      (msg "( MUTUAL-RECURSION ... ( DEFUN ~x0 ...) ~
                                      ...)"
                        (car names))
                      ctx)
                    wrld
                    state-vars)))
              (trans-value (cons x y))))
          (erp (mv erp x bindings2))
          (t (let ((bindings bindings2))
              (trans-er-let* ((y (translate-bodies1 non-executablep
                     (cdr names)
                     (cdr bodies)
                     bindings
                     (cdr arglists)
                     (cdr stobjs-in-lst)
                     ctx
                     wrld
                     state-vars)))
                (trans-value (cons x y))))))))))

(defun chk-non-executable-bodies
  (names arglists bodies non-executablep mut-rec-p ctx state)
  (cond ((endp bodies) (value nil))
    (t (let ((name (car names)) (body (car bodies))
          (formals (car arglists)))
        (cond ((throw-nonexec-error-p body
             (and (not (eq non-executablep :program)) name)
             formals) (chk-non-executable-bodies (cdr names)
              (cdr arglists)
              (cdr bodies)
              non-executablep
              mut-rec-p
              ctx
              state))
          (t (er soft
              ctx
              "The body of a defun that is marked :non-executable ~
                           (perhaps implicitly, by the use of defun-nx~@1) must ~
                           be of the form (prog2$ (throw-nonexec-error ...) ~
                           ...)~@2.  The definition of ~x0 is thus illegal.  ~
                           See :DOC defun-nx."
              (car names)
              (if mut-rec-p
                " in some definition under the mutual-recursion"
                "")
              (if (eq non-executablep :program)
                ""
                ", as is laid down by defun-nx"))))))))

(defun collect-untouchable-fns
  (syms state)
  (let ((temp-touchable-fns (f-get-global 'temp-touchable-fns state)))
    (cond ((eq temp-touchable-fns t) nil)
      (t (let* ((wrld (w state)) (untouchable-fns (global-val 'untouchable-fns wrld))
            (int (intersection-eq syms untouchable-fns)))
          (cond (temp-touchable-fns (set-difference-eq int temp-touchable-fns))
            (t int)))))))

(defun collect-untouchable-vars
  (syms state)
  (let ((temp-touchable-vars (f-get-global 'temp-touchable-vars state)))
    (cond ((eq temp-touchable-vars t) nil)
      (t (let* ((wrld (w state)) (untouchable-vars (global-val 'untouchable-vars wrld))
            (int (and syms (intersection-eq syms untouchable-vars))))
          (cond (temp-touchable-vars (set-difference-eq int temp-touchable-vars))
            (t int)))))))

(defun get-translate-cert-data-record
  (type lst state)
  (cond ((endp lst) nil)
    ((eq type
       (access translate-cert-data-record (car lst) :type)) (cond ((or (get-translate-cert-data-record type (cdr lst) state)
           (collect-untouchable-fns (access translate-cert-data-record (car lst) :fns)
             state)
           (collect-untouchable-vars (access translate-cert-data-record (car lst) :vars)
             state)) nil)
        (t (car lst))))
    (t (get-translate-cert-data-record type (cdr lst) state))))

(defun get-translate-bodies
  (names cert-data-entry state)
  (cond ((null names) nil)
    (t (let ((lst (cert-data-val (car names) cert-data-entry)))
        (cond ((null lst) nil)
          (t (let ((val (get-translate-cert-data-record :translate-bodies lst state)))
              (and val
                (assert$ (equal (access translate-cert-data-record val :inputs)
                    names)
                  (access translate-cert-data-record val :value))))))))))

(defun translate-bodies
  (non-executablep names
    arglists
    bodies
    bindings0
    stobjs-in-lst
    reclassifying-all-programp
    ctx
    wrld
    state)
  (declare (xargs :guard (true-listp bodies)))
  (let ((cert-data-entry (cert-data-entry :translate state)))
    (let ((cert-data-tbodies-and-bindings (if cert-data-entry
           (get-translate-bodies names cert-data-entry state)
           nil)))
      (cond (cert-data-tbodies-and-bindings (value cert-data-tbodies-and-bindings))
        (t (mv-let (erp lst bindings)
            (translate-bodies1 (eq non-executablep t)
              names
              bodies
              bindings0
              arglists
              stobjs-in-lst
              ctx
              wrld
              (default-state-vars t
                :temp-touchable-fns (or reclassifying-all-programp
                  (f-get-global 'temp-touchable-fns state))
                :temp-touchable-vars (or reclassifying-all-programp
                  (f-get-global 'temp-touchable-vars state))))
            (er-progn (cond (erp (er-soft erp "Translate" "~@0" lst))
                (non-executablep (chk-non-executable-bodies names
                    arglists
                    lst
                    non-executablep
                    (cdr names)
                    ctx
                    state))
                (t (value nil)))
              (value (cons lst
                  (cond ((eq non-executablep t) (pairlis-x2 names '(nil)))
                    (t bindings)))))))))))

(defun chk-mutual-recursion-bad-names
  (lst names bodies)
  (cond ((null lst) nil)
    ((ffnnamesp names (car bodies)) (chk-mutual-recursion-bad-names (cdr lst)
        names
        (cdr bodies)))
    (t (cons (car lst)
        (chk-mutual-recursion-bad-names (cdr lst)
          names
          (cdr bodies))))))

(defun chk-mutual-recursion1
  (names bodies warnp ctx state)
  (cond ((and warnp (warning-disabled-p "mutual-recursion")) (value nil))
    (t (let ((bad (chk-mutual-recursion-bad-names names names bodies)))
        (cond ((null bad) (value nil))
          (warnp (pprogn (warning$ ctx
                ("mutual-recursion")
                *chk-mutual-recursion-string*
                (if (consp (cdr bad))
                  1
                  0)
                bad)
              (value nil)))
          (t (er soft
              ctx
              *chk-mutual-recursion-string*
              (if (consp (cdr bad))
                1
                0)
              bad)))))))

(defun chk-mutual-recursion
  (names bodies ctx state)
  (cond ((null names) (er soft
        ctx
        "It is illegal to use MUTUAL-RECURSION to define no functions."))
    ((null (cdr names)) (value nil))
    (t (let ((bogus-mutual-recursion-ok (cdr (assoc-eq :bogus-mutual-recursion-ok (table-alist 'acl2-defaults-table (w state))))))
        (if (eq bogus-mutual-recursion-ok t)
          (value nil)
          (chk-mutual-recursion1 names
            bodies
            (eq bogus-mutual-recursion-ok :warn)
            ctx
            state))))))

(defun putprop-recursivep-lst
  (loop$-recursion-checkedp loop$-recursion names bodies wrld)
  (prog2$ (choke-on-loop$-recursion loop$-recursion-checkedp
      names
      bodies
      'putprop-recursivep-lst)
    (cond (loop$-recursion (putprop (car names) 'recursivep names wrld))
      ((int= (length names) 1) (cond ((ffnnamep-mod-mbe (car names) (car bodies)) (putprop (car names) 'recursivep names wrld))
          (t wrld)))
      (t (putprop-x-lst1 names 'recursivep names wrld)))))

(defun proper-dumb-occur-as-output
  (x y)
  (cond ((equal x y) nil)
    ((variablep y) nil)
    ((fquotep y) nil)
    ((eq (ffn-symb y) 'if) (and (proper-dumb-occur-as-output x (fargn y 2))
        (proper-dumb-occur-as-output x (fargn y 3))))
    (t (dumb-occur-lst x (fargs y)))))

(defun always-tested-and-changedp
  (var pos t-machine)
  (cond ((null t-machine) t)
    ((and (dumb-occur-lst var
         (access tests-and-call (car t-machine) :tests))
       (let ((argn (nth pos
              (fargs (access tests-and-call (car t-machine) :call)))))
         (and argn (proper-dumb-occur-as-output var argn)))) (always-tested-and-changedp var pos (cdr t-machine)))
    (t nil)))

(defun guess-measure
  (name defun-flg args pos t-machine ctx wrld state)
  (cond ((null args) (cond ((null t-machine) (value (mcons-term* (default-measure-function wrld) *0*)))
        (t (er soft
            ctx
            "No ~#0~[:MEASURE~/:CONTROLLER-ALIST~] was supplied with the ~
                ~#0~[definition of~/proposed :DEFINITION rule for~] ~x1.  Our ~
                heuristics for guessing one have not made any suggestions.  ~
                No argument of the function is tested along every branch of ~
                the relevant IF structure and occurs as a proper subterm at ~
                the same argument position in every recursive call.  You must ~
                specify a ~#0~[:MEASURE.  See :DOC defun.~/:CONTROLLER-ALIST. ~
                ~ See :DOC definition.~@2~]  Also see :DOC ruler-extenders ~
                for how to affect how much of the IF structure is explored by ~
                our heuristics."
            (if defun-flg
              0
              1)
            name
            (cond (defun-flg "")
              (t "  In some cases you may wish to use the :CONTROLLER-ALIST ~
                    from the original (or any previous) definition; this may ~
                    be seen by using :PR."))))))
    ((always-tested-and-changedp (car args) pos t-machine) (value (mcons-term* (default-measure-function wrld) (car args))))
    (t (guess-measure name
        defun-flg
        (cdr args)
        (1+ pos)
        t-machine
        ctx
        wrld
        state))))

(defun guess-measure-alist
  (names arglists measures t-machines ctx wrld state)
  (cond ((null names) (value nil))
    ((equal (car measures) *no-measure*) (er-let* ((m (guess-measure (car names)
             t
             (car arglists)
             0
             (car t-machines)
             ctx
             wrld
             state)))
        (er-let* ((alist (guess-measure-alist (cdr names)
               (cdr arglists)
               (cdr measures)
               (cdr t-machines)
               ctx
               wrld
               state)))
          (value (cons (cons (car names) m) alist)))))
    (t (er-let* ((alist (guess-measure-alist (cdr names)
             (cdr arglists)
             (cdr measures)
             (cdr t-machines)
             ctx
             wrld
             state)))
        (value (cons (cons (car names) (car measures)) alist))))))

(defun tilde-*-measure-phrase1
  (alist wrld)
  (cond ((null alist) nil)
    (t (cons (msg (cond ((null (cdr alist)) "~p1 for ~x0.") (t "~p1 for ~x0"))
          (caar alist)
          (untranslate (cdar alist) nil wrld))
        (tilde-*-measure-phrase1 (cdr alist) wrld)))))

(defun tilde-*-measure-phrase
  (alist wrld)
  (list* ""
    "~@*"
    "~@* and "
    "~@*, "
    (cond ((null (cdr alist)) (list (cons "~p1."
            (list (cons #\1 (untranslate (cdar alist) nil wrld))))))
      (t (tilde-*-measure-phrase1 alist wrld)))
    nil))

(defun find-?-measure
  (measure-alist)
  (cond ((endp measure-alist) nil)
    ((let* ((entry (car measure-alist)) (measure (cdr entry)))
       (and (consp measure) (eq (car measure) :?) entry)))
    (t (find-?-measure (cdr measure-alist)))))

(defun prove-termination
  (names t-machines
    measure-alist
    mp
    rel
    hints
    otf-flg
    bodies
    measure-debug
    ctx
    ens
    wrld
    state
    ttree)
  (mv-let (cl-set cl-set-ttree)
    (cond ((and (not (ld-skip-proofsp state)) t-machines) (clean-up-clause-set (measure-clauses-for-clique names
            t-machines
            measure-alist
            mp
            rel
            measure-debug
            wrld)
          ens
          wrld
          ttree
          state))
      (t (mv nil ttree)))
    (cond ((and (not (ld-skip-proofsp state))
         (find-?-measure measure-alist)) (let* ((entry (find-?-measure measure-alist)) (fn (car entry))
            (measure (cdr entry)))
          (er soft
            ctx
            "A :measure of the form (:? v1 ... vk) is only legal when the ~
            defun is redundant (see :DOC redundant-events) or when skipping ~
            proofs (see :DOC ld-skip-proofsp).  The :measure ~x0 supplied for ~
            function symbol ~x1 is thus illegal."
            measure
            fn)))
      (t (er-let* ((cl-set-ttree (accumulate-ttree-and-step-limit-into-state cl-set-ttree
               :skip state)))
          (pprogn (increment-timer 'other-time state)
            (let ((displayed-goal (prettyify-clause-set cl-set (let*-abstractionp state) wrld)) (simp-phrase (tilde-*-simp-phrase cl-set-ttree)))
              (mv-let (col state)
                (cond ((ld-skip-proofsp state) (mv 0 state))
                  ((null t-machines) (io? event
                      nil
                      (mv col state)
                      (names)
                      (fmt "Since ~&0 is non-recursive, its admission is trivial."
                        (list (cons #\0 names))
                        (proofs-co state)
                        state
                        nil)
                      :default-bindings ((col 0))))
                  ((null cl-set) (io? event
                      nil
                      (mv col state)
                      (measure-alist wrld rel names)
                      (fmt "The admission of ~&0 ~#0~[is~/are~] trivial, using ~@1 ~
                       and the measure ~*2"
                        (list (cons #\0 names)
                          (cons #\1 (tilde-@-well-founded-relation-phrase rel wrld))
                          (cons #\2 (tilde-*-measure-phrase measure-alist wrld)))
                        (proofs-co state)
                        state
                        (term-evisc-tuple nil state))
                      :default-bindings ((col 0))))
                  (t (io? event
                      nil
                      (mv col state)
                      (cl-set-ttree displayed-goal
                        simp-phrase
                        measure-alist
                        wrld
                        rel
                        names)
                      (fmt "For the admission of ~&0 we will use ~@1 and the ~
                       measure ~*2  The non-trivial part of the measure ~
                       conjecture~#3~[~/, given ~*4,~] is~@5~%~%Goal~%~Q67."
                        (list (cons #\0 names)
                          (cons #\1 (tilde-@-well-founded-relation-phrase rel wrld))
                          (cons #\2 (tilde-*-measure-phrase measure-alist wrld))
                          (cons #\3
                            (if (nth 4 simp-phrase)
                              1
                              0))
                          (cons #\4 simp-phrase)
                          (cons #\5
                            (if (tagged-objectsp 'sr-limit cl-set-ttree)
                              " as follows (where the ~
                                           subsumption/replacement limit ~
                                           affected this analysis; see :DOC ~
                                           case-split-limitations)."
                              ""))
                          (cons #\6 displayed-goal)
                          (cons #\7 (term-evisc-tuple nil state)))
                        (proofs-co state)
                        state
                        nil)
                      :default-bindings ((col 0)))))
                (pprogn (increment-timer 'print-time state)
                  (cond ((null cl-set) (value (cons (or col 0) cl-set-ttree)))
                    (t (mv-let (erp ttree state)
                        (prove (termify-clause-set cl-set)
                          (make-pspv ens
                            wrld
                            state
                            :displayed-goal displayed-goal
                            :otf-flg otf-flg)
                          hints
                          ens
                          wrld
                          ctx
                          state)
                        (cond (erp (let ((erp-msg (cond ((subsetp-eq '(summary error)
                                      (f-get-global 'inhibit-output-lst state)) nil)
                                   (t (msg "The proof of the measure conjecture for ~&0 ~
                                has failed.~@1"
                                       names
                                       (if (equal t-machines
                                           (termination-machines t
                                             (if (cdr names)
                                               nil
                                               (getpropc (car names) 'loop$-recursion nil wrld))
                                             names
                                             (if (cdr names)
                                               nil
                                               (list (formals (car names) wrld)))
                                             bodies
                                             (make-list (length names) :initial-element :all)))
                                         ""
                                         (msg "~|**NOTE**:  The use of declaration ~
                                       ~x0 would change the measure ~
                                       conjecture, perhaps making it easier ~
                                       to prove.  See :DOC ruler-extenders."
                                           '(xargs :ruler-extenders :all))))))))
                              (mv-let (erp val state)
                                (er soft ctx "~@0~|" erp-msg)
                                (declare (ignore erp val))
                                (mv (msg "~@0  " erp-msg) nil state))))
                          (t (mv-let (col state)
                              (io? event
                                nil
                                (mv col state)
                                (names)
                                (fmt "That completes the proof of the ~
                                        measure theorem for ~&1.  Thus, we ~
                                        admit ~#1~[this function~/these ~
                                        functions~] under the principle of ~
                                        definition."
                                  (list (cons #\1 names))
                                  (proofs-co state)
                                  state
                                  nil)
                                :default-bindings ((col 0)))
                              (pprogn (increment-timer 'print-time state)
                                (value (cons (or col 0) (cons-tag-trees cl-set-ttree ttree)))))))))))))))))))

(defun putprop-justification-lst
  (measure-alist subset-lst
    mp
    rel
    ruler-extenders-lst
    subversive-p
    wrld)
  (cond ((null measure-alist) wrld)
    (t (putprop-justification-lst (cdr measure-alist)
        (cdr subset-lst)
        mp
        rel
        (cdr ruler-extenders-lst)
        subversive-p
        (putprop (caar measure-alist)
          'justification
          (make justification
            :subset (car subset-lst)
            :subversive-p subversive-p
            :mp mp
            :rel rel
            :measure (cdar measure-alist)
            :ruler-extenders (car ruler-extenders-lst))
          wrld)))))

(defun clean-up-nots
  (p)
  (case-match p
    (('if ('if q ''nil ''t) ''nil ''t) q)
    (('not ('if q ''nil ''t)) q)
    (('if ('not q) ''nil ''t) q)
    (('not ('not q)) q)
    (('if q ''nil ''t) `(not ,Q))
    (& p)))

(defun clean-up-nots-lst
  (lst ans)
  (cond ((endp lst) ans)
    (t (clean-up-nots-lst (cdr lst)
        (cons (clean-up-nots (car lst)) ans)))))

(defun clean-up-conjunction1
  (lst ans)
  (cond ((endp lst) ans)
    ((member-complement-term (car lst) (cdr lst)) :contradiction)
    ((member-equal (car lst) (cdr lst)) (clean-up-conjunction1 (cdr lst) ans))
    (t (clean-up-conjunction1 (cdr lst) (cons (car lst) ans)))))

(defun clean-up-conjunction
  (lst)
  (clean-up-conjunction1 (clean-up-nots-lst lst nil) nil))

(defun clean-up-loop$-recursion-induction-machine
  (tc-list)
  (cond ((endp tc-list) nil)
    (t (let ((tests (clean-up-conjunction (access tests-and-calls (car tc-list) :tests))))
        (cond ((eq tests :contradiction) (clean-up-loop$-recursion-induction-machine (cdr tc-list)))
          (t (cons (make tests-and-calls
                :tests tests
                :calls (access tests-and-calls (car tc-list) :calls))
              (clean-up-loop$-recursion-induction-machine (cdr tc-list)))))))))

(defun induction-machines
  (loop$-recursion names
    arglists
    measure-alist
    bodies
    ruler-extenders-lst
    wrld)
  (declare (ignore arglists measure-alist wrld))
  (cond ((null (cdr names)) (if loop$-recursion
        nil
        (list (induction-machine-for-fn names
            (car bodies)
            (car ruler-extenders-lst)))))
    (t nil)))

(defun putprop-induction-machine-lst
  (loop$-recursion names
    arglists
    measure-alist
    bodies
    ruler-extenders-lst
    subversive-p
    wrld)
  (cond ((cdr names) wrld)
    (subversive-p wrld)
    (t (putprop (car names)
        'induction-machine
        (car (induction-machines loop$-recursion
            names
            arglists
            measure-alist
            bodies
            ruler-extenders-lst
            wrld))
        wrld))))

(defun putprop-quick-block-info-lst
  (names t-machines wrld)
  (cond ((null (cdr names)) (putprop (car names)
        'quick-block-info
        (quick-block-info (car names)
          (formals (car names) wrld)
          (car t-machines))
        wrld))
    (t wrld)))

(defun get-sig-fns1
  (ee-lst)
  (cond ((endp ee-lst) nil)
    (t (let ((ee-entry (car ee-lst)))
        (cond ((and (eq (car ee-entry) 'encapsulate) (cddr ee-entry)) (append (get-sig-fns1 (cdr ee-lst))
              (strip-cars (cadr ee-entry))))
          (t (get-sig-fns1 (cdr ee-lst))))))))

(defun get-sig-fns
  (wrld)
  (get-sig-fns1 (global-val 'embedded-event-lst wrld)))

(defun selected-all-fnnames-lst
  (formals subset actuals acc)
  (cond ((endp formals) acc)
    (t (selected-all-fnnames-lst (cdr formals)
        subset
        (cdr actuals)
        (if (member-eq (car formals) subset)
          (all-fnnames1 nil (car actuals) acc)
          acc)))))

(defun subversivep
  (fns t-machine formals-and-subset-alist wrld)
  (cond ((endp t-machine) nil)
    (t (or (intersectp-eq fns
          (instantiable-ancestors (all-fnnames-lst (access tests-and-call (car t-machine) :tests))
            wrld
            nil))
        (let* ((call (access tests-and-call (car t-machine) :call)) (entry (assoc-eq (ffn-symb call) formals-and-subset-alist))
            (formals (assert$ entry (cadr entry)))
            (subset (cddr entry))
            (measured-call-args-ancestors (instantiable-ancestors (selected-all-fnnames-lst formals subset (fargs call) nil)
                wrld
                nil)))
          (intersectp-eq fns measured-call-args-ancestors))
        (subversivep fns
          (cdr t-machine)
          formals-and-subset-alist
          wrld)))))

(defun subversive-cliquep
  (fns t-machines formals-and-subset-alist wrld)
  (cond ((endp t-machines) nil)
    (t (or (subversivep fns
          (car t-machines)
          formals-and-subset-alist
          wrld)
        (subversive-cliquep fns
          (cdr t-machines)
          formals-and-subset-alist
          wrld)))))

(defun prove-termination-non-recursive
  (names bodies
    mp
    rel
    hints
    otf-flg
    big-mutrec
    ctx
    ens
    wrld
    state)
  (er-progn (cond (hints (let ((bogus-defun-hints-ok (cdr (assoc-eq :bogus-defun-hints-ok (table-alist 'acl2-defaults-table (w state))))))
          (cond ((eq bogus-defun-hints-ok :warn) (pprogn (warning$ ctx
                  "Non-rec"
                  "Since ~x0 is non-recursive your supplied :hints will be ~
                     ignored (as these are used only during termination ~
                     proofs).  Perhaps either you meant to supply ~
                     :guard-hints or the body of the definition is incorrect."
                  (car names))
                (value nil)))
            (bogus-defun-hints-ok (value nil))
            (t (er soft
                ctx
                "Since ~x0 is non-recursive it is odd that you have supplied ~
              :hints (which are used only during termination proofs).  We ~
              suspect something is amiss, e.g., you meant to supply ~
              :guard-hints or the body of the definition is incorrect.  To ~
              avoid this error, see :DOC set-bogus-defun-hints-ok."
                (car names))))))
      (t (value nil)))
    (er-let* ((wrld1 (update-w big-mutrec wrld)) (pair (prove-termination names
            nil
            nil
            mp
            rel
            nil
            otf-flg
            bodies
            nil
            ctx
            ens
            wrld1
            state
            nil)))
      (value (list (car pair) wrld1 (cdr pair))))))

(defun prove-termination-recursive
  (names arglists
    measures
    t-machines
    mp
    rel
    hints
    otf-flg
    bodies
    measure-debug
    ctx
    ens
    wrld
    state)
  (er-let* ((measure-alist (guess-measure-alist names
         arglists
         measures
         t-machines
         ctx
         wrld
         state)) (hints (cond ((member-eq (ld-skip-proofsp state)
             '(include-book include-book-with-locals initialize-acl2)) (value nil))
          (hints (value hints))
          (t (let ((default-hints (default-hints wrld)))
              (if default-hints
                (translate-hints (cons "Measure Lemma for" (car names))
                  default-hints
                  ctx
                  wrld
                  state)
                (value hints))))))
      (pair (prove-termination names
          t-machines
          measure-alist
          mp
          rel
          hints
          otf-flg
          bodies
          measure-debug
          ctx
          ens
          wrld
          state
          nil)))
    (value (list* (car pair) measure-alist (cdr pair)))))

(defun put-induction-info-recursive
  (loop$-recursion names
    arglists
    col
    ttree
    measure-alist
    t-machines
    ruler-extenders-lst
    bodies
    mp
    rel
    wrld
    state)
  (let* ((subset-lst (collect-all-vars (strip-cdrs measure-alist))) (sig-fns (get-sig-fns wrld))
      (subversive-p (and sig-fns
          (subversive-cliquep sig-fns
            t-machines
            (pairlis$ names (pairlis$ arglists subset-lst))
            wrld)))
      (wrld2 (putprop-induction-machine-lst loop$-recursion
          names
          arglists
          measure-alist
          bodies
          ruler-extenders-lst
          subversive-p
          wrld))
      (wrld3 (putprop-justification-lst measure-alist
          subset-lst
          mp
          rel
          ruler-extenders-lst
          subversive-p
          wrld2))
      (wrld4 (putprop-quick-block-info-lst names t-machines wrld3)))
    (value (list* col
        wrld4
        (push-lemma (cddr (assoc-eq rel
              (global-val 'well-founded-relation-alist wrld4)))
          ttree)
        subversive-p))))

(defun maybe-warn-or-error-on-non-rec-measure
  (name ctx wrld state)
  (let ((bogus-defun-hints-ok (cdr (assoc-eq :bogus-defun-hints-ok (table-alist 'acl2-defaults-table wrld)))))
    (cond ((eq bogus-defun-hints-ok :warn) (pprogn (warning$ ctx
            "Non-rec"
            "Since ~x0 is non-recursive your supplied :measure will be ~
                  ignored (as the :measure is used only during termination ~
                  proofs)."
            name)
          (value nil)))
      (bogus-defun-hints-ok (value nil))
      (t (er soft
          ctx
          "It is illegal to supply a measure for a non-recursive function, as ~
           has been done for ~x0.  To avoid this error, see :DOC ~
           set-bogus-measure-ok."
          name)))))

(defun collect-problematic-quoted-fns
  (names0 fns wrld progs unwars)
  (cond ((endp fns) (mv (reverse progs) (reverse unwars)))
    ((or (member-eq (car fns) names0)
       (hons-get (car fns)
         (unquote (getpropc '*badge-prim-falist* 'const nil wrld)))
       (assoc-eq (car fns)
         (unquote (getpropc '*apply$-boot-fns-badge-alist* 'const nil wrld)))) (collect-problematic-quoted-fns names0
        (cdr fns)
        wrld
        progs
        unwars))
    ((programp (car fns) wrld) (collect-problematic-quoted-fns names0
        (cdr fns)
        wrld
        (add-to-set-eq (car fns) progs)
        unwars))
    ((not (get-warrantp (car fns) wrld)) (collect-problematic-quoted-fns names0
        (cdr fns)
        wrld
        progs
        (add-to-set-eq (car fns) unwars)))
    (t (collect-problematic-quoted-fns names0
        (cdr fns)
        wrld
        progs
        unwars))))

(defun maybe-warn-on-problematic-quoted-fns
  (names measures bodies ctx wrld state)
  (if (global-val 'boot-strap-flg wrld)
    (value nil)
    (mv-let (progs unwars)
      (collect-problematic-quoted-fns names
        (all-fnnames! t
          :inside nil
          (append measures bodies)
          nil
          wrld
          nil)
        wrld
        nil
        nil)
      (pprogn (cond (progs (warning$ ctx
              "Problematic-quoted-fns"
              "The definition~#0~[~/s~] of ~&0 ~#0~[is~/are~] in ~
                      :LOGIC mode but mention~#0~[s~/~] the :PROGRAM mode ~
                      function~#1~[~/s~] ~&1 in one or more :FN or :EXPR ~
                      slots.  Conjectures about ~#0~[~&0~/the functions ~
                      defined in the clique~] may not be provable until ~
                      ~#1~[this program is~/these programs are~] converted to ~
                      :LOGIC mode and warranted!  See :DOC verify-termination ~
                      and defwarrant."
              names
              progs))
          (t state))
        (cond (unwars (warning$ ctx
              "Problematic-quoted-fns"
              "The definition~#0~[~/s~] of ~&0 ~#0~[is~/are~] in ~
                      :LOGIC mode but mention~#0~[s~/~] the unwarranted ~
                      function~#1~[~/s~] ~&1 in one or more :FN or :EXPR ~
                      slots.  Conjectures about ~#0~[~&0~/the functions ~
                      defined in the clique~] may not be provable until ~
                      ~#1~[this unwarranted function is~/these unwarranted ~
                      functions are~] warranted!  See :DOC defwarrant."
              names
              unwars))
          (t state))
        (value nil)))))

(defun put-induction-info
  (loop$-recursion names
    arglists
    measures
    ruler-extenders-lst
    bodies
    mp
    rel
    hints
    otf-flg
    big-mutrec
    measure-debug
    ctx
    ens
    wrld
    state)
  (let ((wrld1 (putprop-recursivep-lst t loop$-recursion names bodies wrld)))
    (cond ((and (null (cdr names))
         (null (getpropc (car names) 'recursivep nil wrld1))) (er-progn (cond ((equal (car measures) *no-measure*) (value nil))
            (t (maybe-warn-or-error-on-non-rec-measure (car names)
                ctx
                wrld1
                state)))
          (maybe-warn-on-problematic-quoted-fns names
            (if (equal (car measures) *no-measure*)
              nil
              measures)
            bodies
            ctx
            wrld1
            state)
          (prove-termination-non-recursive names
            bodies
            mp
            rel
            hints
            otf-flg
            big-mutrec
            ctx
            ens
            wrld1
            state)))
      (t (let ((t-machines (termination-machines t
               loop$-recursion
               names
               arglists
               bodies
               ruler-extenders-lst)))
          (er-let* ((wrld1 (update-w t wrld1)) (temp (maybe-warn-on-problematic-quoted-fns names
                  (if (equal (car measures) *no-measure*)
                    nil
                    measures)
                  bodies
                  ctx
                  wrld1
                  state))
              (triple (prove-termination-recursive names
                  arglists
                  measures
                  t-machines
                  mp
                  rel
                  hints
                  otf-flg
                  bodies
                  measure-debug
                  ctx
                  ens
                  wrld1
                  state)))
            (let* ((col (car triple)) (measure-alist (cadr triple))
                (ttree (cddr triple)))
              (put-induction-info-recursive loop$-recursion
                names
                arglists
                col
                ttree
                measure-alist
                t-machines
                ruler-extenders-lst
                bodies
                mp
                rel
                wrld1
                state))))))))

(defun destructure-definition
  (term install-body ens wrld ttree)
  (mv-let (hyps equiv fn-args body)
    (case-match term
      (('implies hyp (equiv fn-args body)) (mv (flatten-ands-in-lit hyp) equiv fn-args body))
      ((equiv fn-args body) (mv nil equiv fn-args body))
      (& (mv nil nil nil nil)))
    (let ((equiv (if (member-eq equiv *equality-aliases*)
           'equal
           equiv)) (fn (and (consp fn-args) (car fn-args))))
      (cond ((and fn
           (symbolp fn)
           (not (member-eq fn ''if))
           (equivalence-relationp equiv wrld)) (mv-let (body ttree)
            (cond ((eq install-body :normalize) (normalize (remove-guard-holders body wrld)
                  nil
                  nil
                  ens
                  wrld
                  ttree
                  (normalize-ts-backchain-limit-for-defs wrld)))
              (t (mv body ttree)))
            (mv hyps equiv fn (cdr fn-args) body ttree)))
        (t (mv nil nil nil nil nil nil))))))

(defun member-rewrite-rule-rune
  (rune lst)
  (cond ((null lst) nil)
    ((equal rune (access rewrite-rule (car lst) :rune)) t)
    (t (member-rewrite-rule-rune rune (cdr lst)))))

(defun replace-rewrite-rule-rune
  (rune rule lst)
  (cond ((null lst) nil)
    ((equal rune (access rewrite-rule (car lst) :rune)) (cons rule (cdr lst)))
    (t (cons (car lst)
        (replace-rewrite-rule-rune rune rule (cdr lst))))))

(defun preprocess-hyp
  (hyp wrld)
  (case-match hyp
    (('atom x) (list (mcons-term* 'not
          (mcons-term* 'consp (remove-guard-holders x wrld)))))
    (& (list (remove-guard-holders hyp wrld)))))

(defun preprocess-hyps
  (hyps wrld)
  (cond ((null hyps) nil)
    (t (append (preprocess-hyp (car hyps) wrld)
        (preprocess-hyps (cdr hyps) wrld)))))

(defun add-definition-rule-with-ttree
  (rune nume
    clique
    controller-alist
    install-body
    term
    ens
    wrld
    ttree)
  (mv-let (hyps equiv fn args body ttree)
    (destructure-definition term install-body ens wrld ttree)
    (let* ((vars-bag (all-vars-bag-lst args nil)) (abbreviationp (and (null hyps)
            (null clique)
            (abbreviationp (not (all-nils-or-dfs (getpropc fn 'stobjs-out '(nil) wrld)))
              vars-bag
              body)))
        (rule (make rewrite-rule
            :rune rune
            :nume nume
            :hyps (preprocess-hyps hyps wrld)
            :equiv equiv
            :lhs (mcons-term fn args)
            :var-info (cond (abbreviationp (not (null vars-bag)))
              (t (var-counts args body)))
            :rhs body
            :subclass (cond (abbreviationp 'abbreviation) (t 'definition))
            :heuristic-info (cond (abbreviationp nil)
              (t (cons clique controller-alist)))
            :backchain-limit-lst nil)))
      (let ((wrld0 (if (eq fn 'hide)
             wrld
             (putprop fn
               'lemmas
               (cons rule (getpropc fn 'lemmas nil wrld))
               wrld))))
        (cond (install-body (mv (putprop fn
                'def-bodies
                (cons (make def-body
                    :nume nume
                    :hyp (and hyps (conjoin hyps))
                    :concl body
                    :equiv equiv
                    :rune rune
                    :formals args
                    :recursivep clique
                    :controller-alist controller-alist)
                  (getpropc fn 'def-bodies nil wrld))
                wrld0)
              ttree))
          (t (mv wrld0 ttree)))))))

(defun add-definition-rule
  (rune nume
    clique
    controller-alist
    install-body
    term
    ens
    wrld)
  (mv-let (wrld ttree)
    (add-definition-rule-with-ttree rune
      nume
      clique
      controller-alist
      install-body
      term
      ens
      wrld
      nil)
    (declare (ignore ttree))
    wrld))

(defun putprop-body-lst
  (names arglists
    bodies
    normalizeps
    clique
    controller-alist
    ens
    wrld
    installed-wrld
    ttree)
  (cond ((null names) (mv wrld ttree))
    (t (let* ((fn (car names)) (args (car arglists))
          (body (car bodies))
          (normalizep (car normalizeps))
          (rune (fn-rune-nume fn nil nil installed-wrld))
          (nume (fn-rune-nume fn t nil installed-wrld)))
        (let* ((eqterm (fcons-term* 'equal (fcons-term fn args) body)) (term eqterm))
          (mv-let (wrld ttree)
            (add-definition-rule-with-ttree rune
              nume
              clique
              controller-alist
              (if normalizep
                :normalize t)
              term
              ens
              (putprop fn 'unnormalized-body body wrld)
              ttree)
            (putprop-body-lst (cdr names)
              (cdr arglists)
              (cdr bodies)
              (cdr normalizeps)
              clique
              controller-alist
              ens
              wrld
              installed-wrld
              ttree)))))))

(defun type-set-implied-by-term1
  (term tvar fvar)
  (cond ((variablep term) (fcons-term* 'if term tvar fvar))
    ((fquotep term) (if (equal term *nil*)
        fvar
        tvar))
    ((eq (ffn-symb term) 'if) (fcons-term* 'if
        (fargn term 1)
        (type-set-implied-by-term1 (fargn term 2) tvar fvar)
        (type-set-implied-by-term1 (fargn term 3) tvar fvar)))
    (t (fcons-term* 'if term tvar fvar))))

(defun type-set-implied-by-term
  (var not-flg term ens wrld ttree)
  (let* ((new-var (genvar 'genvar "EMPTY" nil (all-vars term))) (type-alist (list (list* new-var *ts-empty* nil))))
    (mv-let (normal-term ttree)
      (normalize term
        t
        nil
        ens
        wrld
        ttree
        (backchain-limit wrld :ts))
      (type-set (type-set-implied-by-term1 normal-term
          (if not-flg
            new-var
            var)
          (if not-flg
            var
            new-var))
        nil
        nil
        type-alist
        ens
        wrld
        ttree
        nil
        nil))))

(defun putprop-initial-type-prescriptions
  (names wrld)
  (cond ((null names) wrld)
    (t (let ((fn (car names)))
        (putprop-initial-type-prescriptions (cdr names)
          (putprop fn
            'type-prescriptions
            (cons (make type-prescription
                :rune *fake-rune-for-anonymous-enabled-rule*
                :nume nil
                :term (mcons-term fn (formals fn wrld))
                :hyps nil
                :backchain-limit-lst nil
                :basic-ts *ts-empty*
                :vars nil
                :corollary *t*)
              (getpropc fn 'type-prescriptions nil wrld))
            wrld))))))

(defun map-returned-formals-via-formals
  (formals pockets returned-formals)
  (cond ((null formals) nil)
    ((member-eq (car formals) returned-formals) (union-eq (car pockets)
        (map-returned-formals-via-formals (cdr formals)
          (cdr pockets)
          returned-formals)))
    (t (map-returned-formals-via-formals (cdr formals)
        (cdr pockets)
        returned-formals))))

(defun map-type-sets-via-formals
  (formals ts-lst returned-formals)
  (cond ((null formals) *ts-empty*)
    ((member-eq (car formals) returned-formals) (ts-union (car ts-lst)
        (map-type-sets-via-formals (cdr formals)
          (cdr ts-lst)
          returned-formals)))
    (t (map-type-sets-via-formals (cdr formals)
        (cdr ts-lst)
        returned-formals))))

(defun vector-ts-union
  (ts-lst1 ts-lst2)
  (cond ((null ts-lst1) nil)
    (t (cons (ts-union (car ts-lst1) (car ts-lst2))
        (vector-ts-union (cdr ts-lst1) (cdr ts-lst2))))))

(defun map-cons-tag-trees
  (lst ttree)
  (cond ((null lst) ttree)
    (t (map-cons-tag-trees (cdr lst)
        (cons-tag-trees (car lst) ttree)))))

(defun type-set-and-returned-formals-with-rule1
  (alist rule-vars
    type-alist
    ens
    wrld
    basic-ts
    vars-ts
    vars
    ttree)
  (cond ((null alist) (mv basic-ts vars-ts vars type-alist ttree))
    ((member-eq (caar alist) rule-vars) (mv-let (ts ttree)
        (type-set (cdar alist)
          nil
          nil
          type-alist
          ens
          wrld
          ttree
          nil
          nil)
        (let ((variablep-image (variablep (cdar alist))))
          (type-set-and-returned-formals-with-rule1 (cdr alist)
            rule-vars
            type-alist
            ens
            wrld
            (if variablep-image
              basic-ts
              (ts-union ts basic-ts))
            (if variablep-image
              (ts-union ts vars-ts)
              vars-ts)
            (if variablep-image
              (add-to-set-eq (cdar alist) vars)
              vars)
            ttree))))
    (t (type-set-and-returned-formals-with-rule1 (cdr alist)
        rule-vars
        type-alist
        ens
        wrld
        basic-ts
        vars-ts
        vars
        ttree))))

(defun type-set-and-returned-formals-with-rule
  (tp term type-alist ens wrld ttree)
  (cond ((enabled-numep (access type-prescription tp :nume) ens) (mv-let (unify-ans unify-subst)
        (one-way-unify (access type-prescription tp :term) term)
        (cond (unify-ans (with-accumulated-persistence (access type-prescription tp :rune)
              (basic-ts vars-ts vars type-alist ttree)
              (not (and (ts= basic-ts *ts-unknown*)
                  (ts= vars-ts *ts-empty*)
                  (null vars)))
              (let* ((backchain-limit (backchain-limit wrld :ts)) (type-alist (extend-type-alist-with-bindings unify-subst
                      nil
                      nil
                      type-alist
                      nil
                      ens
                      wrld
                      nil
                      nil
                      nil
                      backchain-limit)))
                (mv-let (relieve-hyps-ans type-alist ttree)
                  (type-set-relieve-hyps (access type-prescription tp :rune)
                    term
                    (access type-prescription tp :hyps)
                    (access type-prescription tp :backchain-limit-lst)
                    nil
                    nil
                    unify-subst
                    type-alist
                    nil
                    ens
                    wrld
                    nil
                    ttree
                    nil
                    nil
                    backchain-limit
                    1)
                  (cond (relieve-hyps-ans (type-set-and-returned-formals-with-rule1 unify-subst
                        (access type-prescription tp :vars)
                        type-alist
                        ens
                        wrld
                        (access type-prescription tp :basic-ts)
                        *ts-empty*
                        nil
                        (push-lemma (access type-prescription tp :rune) ttree)))
                    (t (mv *ts-unknown* *ts-empty* nil type-alist ttree)))))))
          (t (mv *ts-unknown* *ts-empty* nil type-alist ttree)))))
    (t (mv *ts-unknown* *ts-empty* nil type-alist ttree))))

(defun type-set-and-returned-formals-with-rules
  (tp-lst term type-alist ens w ts vars-ts vars ttree)
  (cond ((null tp-lst) (mv-let (ts1 ttree1)
        (type-set term nil nil type-alist ens w ttree nil nil)
        (let ((ts2 (ts-intersection ts1 ts)))
          (mv ts2
            vars-ts
            vars
            (if (ts= ts2 ts)
              ttree
              ttree1)))))
    (t (mv-let (ts1 vars-ts1 vars1 type-alist1 ttree1)
        (type-set-and-returned-formals-with-rule (car tp-lst)
          term
          type-alist
          ens
          w
          ttree)
        (let* ((ts2 (ts-intersection ts1 ts)) (unchangedp (and (ts= ts2 ts) (equal type-alist type-alist1))))
          (type-set-and-returned-formals-with-rules (cdr tp-lst)
            term
            type-alist1
            ens
            w
            ts2
            (if unchangedp
              vars-ts
              (ts-union vars-ts1 vars-ts))
            (if unchangedp
              vars
              (union-eq vars1 vars))
            (if unchangedp
              ttree
              ttree1)))))))

(defun type-set-and-returned-formals-top
  (term ens wrld ttree)
  (mv-let (basic-type-set returned-vars-type-set returned-vars ttree)
    (type-set-and-returned-formals term nil ens wrld ttree)
    (cond ((ts= returned-vars-type-set -1) (mv basic-type-set returned-vars ttree))
      (t (mv (ts-union basic-type-set returned-vars-type-set)
          nil
          ttree)))))

(defun guess-type-prescription-for-fn-step
  (name body ens wrld ttree)
  (let* ((ttree0 ttree) (old-type-prescriptions (getpropc name 'type-prescriptions nil wrld))
      (tp (car old-type-prescriptions)))
    (mv-let (new-basic-type-set new-returned-vars ttree)
      (type-set-and-returned-formals-top body ens wrld ttree)
      (cond ((ts= new-basic-type-set *ts-unknown*) (mv (putprop name
              'type-prescriptions
              (cons (change type-prescription
                  tp
                  :basic-ts *ts-unknown*
                  :vars nil)
                (cdr old-type-prescriptions))
              wrld)
            ttree0))
        (t (mv (putprop name
              'type-prescriptions
              (cons (change type-prescription
                  tp
                  :basic-ts new-basic-type-set
                  :vars new-returned-vars)
                (cdr old-type-prescriptions))
              wrld)
            ttree))))))

(defun guess-and-putprop-type-prescription-lst-for-clique-step
  (names bodies ens wrld ttree interval state)
  (cond ((null names) (mv wrld ttree state))
    (t (mv-let (erp val state)
        (update-w (int= interval 0) wrld)
        (declare (ignore erp val))
        (mv-let (wrld ttree)
          (guess-type-prescription-for-fn-step (car names)
            (car bodies)
            ens
            wrld
            ttree)
          (guess-and-putprop-type-prescription-lst-for-clique-step (cdr names)
            (cdr bodies)
            ens
            wrld
            ttree
            (if (int= interval 0)
              *clique-step-install-interval*
              (1- interval))
            state))))))

(defun conjoin-type-prescriptions
  (tp1 tp2 ens wrld)
  (cond ((null tp1) (cond ((consp tp2) (mv-let (corollary ttree)
            (convert-type-prescription-to-term tp2 ens wrld)
            (mv (change type-prescription tp2 :corollary corollary)
              ttree)))
        (t (mv nil nil))))
    (t (assert$ (and (null (access type-prescription tp1 :hyps))
          (null (access type-prescription tp1 :backchain-limit-lst)))
        (cond ((atom tp2) (cond ((guarded-termp (access type-prescription tp1 :corollary)
                 wrld) (mv (change type-prescription tp1 :nume tp2)
                  (push-lemma *fake-rune-for-cert-data* nil)))
              (t (mv-let (corollary ttree)
                  (convert-type-prescription-to-term tp1 ens wrld)
                  (mv (change type-prescription
                      tp1
                      :nume tp2
                      :corollary corollary)
                    (push-lemma *fake-rune-for-cert-data* ttree))))))
          (t (assert$ (and (null (access type-prescription tp2 :hyps))
                (null (access type-prescription tp2 :backchain-limit-lst))
                (equal (access type-prescription tp1 :term)
                  (access type-prescription tp2 :term))
                (equal (access type-prescription tp1 :rune)
                  (access type-prescription tp2 :rune)))
              (let ((basic-ts1 (access type-prescription tp1 :basic-ts)) (basic-ts2 (access type-prescription tp2 :basic-ts)))
                (cond ((and (ts-subsetp basic-ts1 basic-ts2)
                     (guarded-termp (access type-prescription tp1 :corollary)
                       wrld)) (mv (change type-prescription
                        tp1
                        :nume (access type-prescription tp2 :nume))
                      (push-lemma *fake-rune-for-cert-data* nil)))
                  ((ts-subsetp basic-ts2 basic-ts1) (mv-let (corollary ttree)
                      (convert-type-prescription-to-term tp2 ens wrld)
                      (mv (change type-prescription tp2 :corollary corollary)
                        ttree)))
                  (t (let* ((vars1 (access type-prescription tp1 :vars)) (vars2 (access type-prescription tp2 :vars))
                        (tp (cond ((equal vars1 vars2) (change type-prescription
                                tp2
                                :basic-ts (ts-intersection basic-ts1 basic-ts2)))
                            (t (change type-prescription
                                tp2
                                :basic-ts (ts-intersection basic-ts1 basic-ts2)
                                :vars (union-eq vars1 vars2))))))
                      (mv-let (corollary ttree)
                        (convert-type-prescription-to-term tp ens wrld)
                        (mv (change type-prescription tp :corollary corollary)
                          ttree)))))))))))))

(defun cleanse-type-prescriptions
  (names type-prescriptions-lst
    def-nume
    rmp-cnt
    ens
    wrld
    installed-wrld
    cert-data-tp-entry
    ttree)
  (cond ((null names) (mv wrld ttree))
    (t (let* ((fn (car names)) (lst (car type-prescriptions-lst))
          (tp1 (cert-data-val fn cert-data-tp-entry))
          (tp2 (cond ((ts= *ts-unknown*
                 (access type-prescription (car lst) :basic-ts)) (+ 2 def-nume))
              (t (change type-prescription
                  (car lst)
                  :rune (list :type-prescription fn)
                  :nume (+ 2 def-nume))))))
        (mv-let (new-tp ttree1)
          (conjoin-type-prescriptions tp1 tp2 ens installed-wrld)
          (let ((ttree2 (cons-tag-trees ttree1 ttree)))
            (mv-let (wrld ttree3)
              (cond ((null new-tp) (mv (putprop fn 'type-prescriptions (cdr lst) wrld) ttree))
                (t (mv (putprop fn
                      'type-prescriptions
                      (cons new-tp (cdr lst))
                      wrld)
                    ttree2)))
              (cleanse-type-prescriptions (cdr names)
                (cdr type-prescriptions-lst)
                (+ rmp-cnt def-nume)
                rmp-cnt
                ens
                wrld
                installed-wrld
                cert-data-tp-entry
                ttree3))))))))

(defun guess-and-putprop-type-prescription-lst-for-clique
  (names bodies
    def-nume
    ens
    wrld
    ttree
    big-mutrec
    cert-data-tp-entry
    state)
  (let ((old-type-prescriptions-lst (getprop-x-lst names 'type-prescriptions wrld)))
    (mv-let (wrld1 ttree state)
      (guess-and-putprop-type-prescription-lst-for-clique-step names
        bodies
        ens
        wrld
        ttree
        *clique-step-install-interval*
        state)
      (er-progn (update-w big-mutrec wrld1)
        (cond ((equal old-type-prescriptions-lst
             (getprop-x-lst names 'type-prescriptions wrld1)) (mv-let (wrld2 ttree)
              (cleanse-type-prescriptions names
                old-type-prescriptions-lst
                def-nume
                (length (getpropc (car names) 'runic-mapping-pairs nil wrld))
                ens
                wrld
                wrld1
                cert-data-tp-entry
                ttree)
              (er-progn (update-w big-mutrec wrld t)
                (update-w big-mutrec wrld2)
                (mv wrld2 ttree state))))
          (t (guess-and-putprop-type-prescription-lst-for-clique names
              bodies
              def-nume
              ens
              wrld1
              ttree
              big-mutrec
              cert-data-tp-entry
              state)))))))

(defun get-normalized-bodies
  (names wrld)
  (cond ((endp names) nil)
    (t (cons (access def-body (def-body (car names) wrld) :concl)
        (get-normalized-bodies (cdr names) wrld)))))

(defun cert-data-putprop-type-prescription-lst-for-clique
  (cert-data-tp-entry names
    def-nume
    rmp-cnt
    ttree
    ens
    wrld
    installed-wrld
    changedp)
  (cond ((endp names) (mv wrld
        (if changedp
          (push-lemma *fake-rune-for-cert-data* ttree)
          ttree)))
    (t (let* ((fn (car names)) (cert-data-pair (cert-data-pair fn cert-data-tp-entry)))
        (cond ((null cert-data-pair) (cert-data-putprop-type-prescription-lst-for-clique cert-data-tp-entry
              (cdr names)
              (+ rmp-cnt def-nume)
              rmp-cnt
              ttree
              ens
              wrld
              installed-wrld
              changedp))
          (t (let ((cert-data-tp (cdr cert-data-pair)))
              (mv-let (corollary ttree1)
                (if (or (null cert-data-tp)
                    (guarded-termp (access type-prescription cert-data-tp :corollary)
                      installed-wrld))
                  (mv nil nil)
                  (convert-type-prescription-to-term cert-data-tp
                    ens
                    installed-wrld))
                (cert-data-putprop-type-prescription-lst-for-clique cert-data-tp-entry
                  (cdr names)
                  (+ rmp-cnt def-nume)
                  rmp-cnt
                  (cons-tag-trees ttree1 ttree)
                  ens
                  (putprop fn
                    'type-prescriptions
                    (list (if corollary
                        (change type-prescription
                          cert-data-tp
                          :nume (+ 2 def-nume)
                          :corollary corollary)
                        (change type-prescription cert-data-tp :nume (+ 2 def-nume))))
                    wrld)
                  installed-wrld
                  t)))))))))

(defun putprop-type-prescription-lst
  (names subversive-p def-nume ens wrld ttree state)
  (cond ((and (consp names)
       (eq (car names) 'hide)
       (null (cdr names))) (mv wrld ttree state))
    (subversive-p (mv wrld ttree state))
    (t (let* ((cert-data-tp-entry-pair (cert-data-entry-pair :type-prescription state)) (cert-data-tp-entry (cdr cert-data-tp-entry-pair))
          (cert-data-pass1-saved (cert-data-entry-pair :pass1-saved state)))
        (cond ((and cert-data-tp-entry-pair (not cert-data-pass1-saved)) (mv-let (wrld ttree)
              (cert-data-putprop-type-prescription-lst-for-clique cert-data-tp-entry
                names
                def-nume
                (length (getpropc (car names) 'runic-mapping-pairs nil wrld))
                ttree
                ens
                wrld
                wrld
                nil)
              (mv wrld ttree state)))
          (t (let ((bodies (get-normalized-bodies names wrld)) (big-mutrec (big-mutrec names)))
              (er-let* ((wrld1 (update-w big-mutrec
                     (putprop-initial-type-prescriptions names wrld))))
                (guess-and-putprop-type-prescription-lst-for-clique names
                  bodies
                  def-nume
                  ens
                  wrld1
                  ttree
                  big-mutrec
                  cert-data-tp-entry
                  state)))))))))

(defun putprop-level-no-lst
  (names wrld)
  (cond ((null names) wrld)
    (t (let ((maximum (max-level-no (body (car names) t wrld) wrld)))
        (putprop-level-no-lst (cdr names)
          (putprop (car names)
            'level-no
            (if (getpropc (car names) 'recursivep nil wrld)
              (1+ maximum)
              maximum)
            wrld))))))

(defun primitive-recursive-argp
  (var term wrld)
  (cond ((variablep term) (eq var term))
    ((fquotep term) nil)
    (t (let ((fn (ffn-symb term)))
        (case fn
          (binary-+ (or (and (nvariablep (fargn term 1))
                (fquotep (fargn term 1))
                (rationalp (cadr (fargn term 1)))
                (< (cadr (fargn term 1)) 0)
                (primitive-recursive-argp var (fargn term 2) wrld))
              (and (nvariablep (fargn term 2))
                (fquotep (fargn term 2))
                (rationalp (cadr (fargn term 2)))
                (< (cadr (fargn term 2)) 0)
                (primitive-recursive-argp var (fargn term 1) wrld))))
          (otherwise (and (symbolp fn)
              (fargs term)
              (null (cdr (fargs term)))
              (= (get-level-no fn wrld) 0)
              (primitive-recursive-argp var (fargn term 1) wrld))))))))

(defun primitive-recursive-callp
  (formals args wrld)
  (cond ((null formals) t)
    (t (and (primitive-recursive-argp (car formals) (car args) wrld)
        (primitive-recursive-callp (cdr formals) (cdr args) wrld)))))

(defun primitive-recursive-callsp
  (formals calls wrld)
  (cond ((null calls) t)
    (t (and (primitive-recursive-callp formals (fargs (car calls)) wrld)
        (primitive-recursive-callsp formals (cdr calls) wrld)))))

(defun primitive-recursive-machinep
  (formals machine wrld)
  (cond ((null machine) t)
    (t (and (primitive-recursive-callsp formals
          (access tests-and-calls (car machine) :calls)
          wrld)
        (primitive-recursive-machinep formals (cdr machine) wrld)))))

(defun putprop-primitive-recursive-defunp-lst
  (names wrld)
  (cond ((null names) wrld)
    ((cdr names) wrld)
    ((primitive-recursive-machinep (formals (car names) wrld)
       (getpropc (car names) 'induction-machine nil wrld)
       wrld) (putprop (car names) 'primitive-recursive-defunp t wrld))
    (t wrld)))

(defun make-controller-pocket
  (formals vars)
  (cond ((null formals) nil)
    (t (cons (if (member (car formals) vars)
          t
          nil)
        (make-controller-pocket (cdr formals) vars)))))

(defun make-controller-alist1
  (names wrld)
  (cond ((null names) nil)
    (t (cons (cons (car names)
          (make-controller-pocket (formals (car names) wrld)
            (access justification
              (getpropc (car names)
                'justification
                '(:error "See MAKE-CONTROLLER-ALIST1.")
                wrld)
              :subset)))
        (make-controller-alist1 (cdr names) wrld)))))

(defun make-controller-alist
  (names wrld)
  (and (getpropc (car names) 'justification nil wrld)
    (make-controller-alist1 names wrld)))

(defun max-nume-exceeded-error
  (ctx)
  (er hard
    ctx
    "ACL2 assumes that no nume exceeds ~x0.  It is very surprising that ~
       this bound is about to be exceeded.  We are causing an error because ~
       for efficiency, ACL2 assumes this bound is never exceeded.  Please ~
       contact the ACL2 implementors with a request that this assumption be ~
       removed from enabled-numep."
    (fixnum-bound)))

(defun putprop-defun-runic-mapping-pairs1
  (names def-nume tp-flg ind-flg wrld)
  (cond ((null names) wrld)
    (t (putprop-defun-runic-mapping-pairs1 (cdr names)
        (+ 2
          (if tp-flg
            1
            0)
          (if ind-flg
            1
            0)
          def-nume)
        tp-flg
        ind-flg
        (putprop (car names)
          'runic-mapping-pairs
          (list* (cons def-nume (list :definition (car names)))
            (cons (+ 1 def-nume)
              (list :executable-counterpart (car names)))
            (if tp-flg
              (list* (cons (+ 2 def-nume) (list :type-prescription (car names)))
                (if ind-flg
                  (list (cons (+ 3 def-nume) (list :induction (car names))))
                  nil))
              nil))
          wrld)))))

(defun putprop-defun-runic-mapping-pairs
  (names tp-flg wrld)
  (let ((next-nume (get-next-nume wrld)))
    (prog2$ (or (<= (the-fixnat next-nume)
          (- (the-fixnat (fixnum-bound))
            (the-fixnat (* (the-fixnat 4) (the-fixnat (length names))))))
        (max-nume-exceeded-error 'putprop-defun-runic-mapping-pairs))
      (putprop-defun-runic-mapping-pairs1 names
        next-nume
        tp-flg
        (and tp-flg (getpropc (car names) 'recursivep nil wrld))
        wrld))))

(defun print-verify-guards-msg
  (names col state)
  (cond ((ld-skip-proofsp state) state)
    (t (pprogn (increment-timer 'other-time state)
        (mv-let (col state)
          (io? event
            nil
            (mv col state)
            (col names)
            (fmt1 "~#0~[This lambda expression~/~&1~] ~#1~[is~/are~] ~
                         compliant with Common Lisp.~|"
              (list (cons #\0
                  (if (and (consp names)
                      (consp (car names))
                      (eq (car (car names)) 'lambda))
                    0
                    1))
                (cons #\1 names))
              col
              (proofs-co state)
              state
              nil)
            :default-bindings ((col 0)))
          (declare (ignore col))
          (increment-timer 'print-time state))))))

(defun collect-ideals
  (names wrld acc)
  (cond ((null names) acc)
    ((eq (symbol-class (car names) wrld) :ideal) (collect-ideals (cdr names) wrld (cons (car names) acc)))
    (t (collect-ideals (cdr names) wrld acc))))

(defun collect-non-ideals
  (names wrld)
  (cond ((null names) nil)
    ((eq (symbol-class (car names) wrld) :ideal) (collect-non-ideals (cdr names) wrld))
    (t (cons (car names) (collect-non-ideals (cdr names) wrld)))))

(defun collect-non-common-lisp-compliants
  (names wrld)
  (cond ((null names) nil)
    ((eq (symbol-class (car names) wrld) :common-lisp-compliant) (collect-non-common-lisp-compliants (cdr names) wrld))
    (t (cons (car names)
        (collect-non-common-lisp-compliants (cdr names) wrld)))))

(defun all-fnnames1-exec
  (flg x acc)
  (cond (flg (cond ((null x) acc)
        (t (all-fnnames1-exec nil
            (car x)
            (all-fnnames1-exec t (cdr x) acc)))))
    ((variablep x) acc)
    ((fquotep x) acc)
    ((flambda-applicationp x) (all-fnnames1-exec nil
        (lambda-body (ffn-symb x))
        (all-fnnames1-exec t (fargs x) acc)))
    ((eq (ffn-symb x) 'return-last) (cond ((equal (fargn x 1) ''mbe1-raw) (all-fnnames1-exec nil (fargn x 2) acc))
        ((and (equal (fargn x 1) ''ec-call1-raw)
           (nvariablep (fargn x 3))
           (not (fquotep (fargn x 3)))
           (not (flambdap (ffn-symb (fargn x 3))))) (all-fnnames1-exec t (fargs (fargn x 3)) acc))
        (t (all-fnnames1-exec t
            (fargs x)
            (add-to-set-eq (ffn-symb x) acc)))))
    (t (all-fnnames1-exec t
        (fargs x)
        (add-to-set-eq (ffn-symb x) acc)))))

(defun collect-guards-and-bodies
  (lst)
  (cond ((endp lst) nil)
    (t (add-to-set-equal (lambda-object-guard (car lst))
        (add-to-set-equal (lambda-object-body (car lst))
          (collect-guards-and-bodies (cdr lst)))))))

(defun chk-common-lisp-compliant-subfunctions-cmp
  (names0 names terms wrld str ctx)
  (cond ((null names) (value-cmp nil))
    (t (let* ((fns (set-difference-eq (all-fnnames1-exec t
               (cons (car terms)
                 (if (global-val 'boot-strap-flg wrld)
                   nil
                   (collect-guards-and-bodies (collect-certain-lambda-objects :well-formed (car terms)
                       wrld
                       nil))))
               (if (global-val 'boot-strap-flg wrld)
                 nil
                 (all-fnnames! nil :inside nil (car terms) nil wrld nil)))
             names0)) (bad (collect-non-common-lisp-compliants fns wrld)))
        (cond (bad (er-cmp ctx
              "The ~@0 for ~x1 calls the function~#2~[ ~&2~/s ~
                            ~&2~], the guards of which have not yet been ~
                            verified.  See :DOC verify-guards."
              str
              (car names)
              bad))
          (t (mv-let (warrants unwarranteds)
              (if (global-val 'boot-strap-flg wrld)
                (mv nil nil)
                (warrants-for-tamep-lambdap-lst (collect-certain-lambda-objects :well-formed (car terms)
                    wrld
                    nil)
                  wrld
                  nil
                  nil))
              (declare (ignore warrants))
              (cond (unwarranteds (er-cmp ctx
                    "The ~@0 for ~x1 applies the function~#2~[ ~
                                  ~&2~/s ~&2~] which ~#2~[is~/are~] not yet ~
                                  warranted.  Lambda objects containing ~
                                  unwarranted function symbols are not ~
                                  provably tame and can't be applied.  See ~
                                  :DOC verify-guards."
                    str
                    (car names)
                    unwarranteds))
                (t (chk-common-lisp-compliant-subfunctions-cmp names0
                    (cdr names)
                    (cdr terms)
                    wrld
                    str
                    ctx))))))))))

(defun chk-common-lisp-compliant-subfunctions
  (names0 names terms wrld str ctx state)
  (cmp-to-error-triple (chk-common-lisp-compliant-subfunctions-cmp names0
      names
      terms
      wrld
      str
      ctx)))

(defun chk-acceptable-verify-guards-formula-cmp
  (name x ctx wrld state-vars)
  (mv-let (erp term bindings)
    (translate1-cmp x
      :stobjs-out '((:stobjs-out . :stobjs-out))
      t
      ctx
      wrld
      state-vars)
    (declare (ignore bindings))
    (cond ((and erp (null name)) (mv-let (erp2 term2 bindings)
          (translate1-cmp x t nil t ctx wrld state-vars)
          (declare (ignore bindings term2))
          (cond (erp2 (mv erp term))
            (t (er-cmp ctx
                "The guards for the given formula cannot be verified ~
                     because it has the wrong syntactic form for evaluation, ~
                     perhaps due to restrictions about multiple-values, ~
                     stobjs or dfs.  See :DOC verify-guards.")))))
      (erp (er-cmp ctx
          "The guards for ~x0 cannot be verified because its formula has ~
               the wrong syntactic form for evaluation, perhaps due to ~
               multiple-value or stobj restrictions.  See :DOC verify-guards."
          (or name x)))
      ((collect-non-common-lisp-compliants (all-fnnames-exec term)
         wrld) (er-cmp ctx
          "The formula ~#0~[named ~x1~/~x1~] contains a call of the ~
               function~#2~[ ~&2~/s ~&2~], the guards of which have not yet ~
               been verified.  See :DOC verify-guards."
          (if name
            0
            1)
          (or name x)
          (collect-non-common-lisp-compliants (all-fnnames-exec term)
            wrld)))
      (t (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp (list name)
            (list name)
            (list term)
            wrld
            "formula"
            ctx)
          (value-cmp (cons :term term)))))))

(defun guard-simplify-msg
  (x)
  (msg "The only legal values for :GUARD-SIMPIFY are ~x0 and ~x1.  The value ~
        ~x2 is thus illegal.~@3"
    t
    :limited x
    (if (eq x nil)
      (msg "  (Consider using :LIMITED in place of ~x0.)" nil)
      "")))

(defun guard-simplify-p
  (x ctx)
  (declare (xargs :guard (member-eq x '(t :limited))))
  (cond ((eq x t) t)
    ((eq x :limited) nil)
    (t (er hard ctx "~@0" (guard-simplify-msg x)))))

(defun chk-acceptable-verify-guards-cmp
  (name rrp guard-simplify ctx wrld state-vars)
  (er-let*-cmp ((ignore (cond ((member-eq guard-simplify '(t :limited)) (value-cmp nil))
         (t (er-cmp ctx "~@0" (guard-simplify-msg guard-simplify))))) (name (cond ((symbolp name) (value-cmp name))
          ((and (consp name)
             (or (eq (car name) 'lambda) (eq (car name) 'lambda$))) (cond ((eq (car name) 'lambda) (cond ((well-formed-lambda-objectp name wrld) (mv-let (erp val)
                      (hons-copy-lambda-object? (kwote name))
                      (cond (erp (er-cmp ctx "~@0" val))
                        (t (value-cmp (unquote val))))))
                  (t (er-cmp ctx
                      "~x0 is not a well-formed LAMBDA expression.  See :DOC ~
                      verify-guards."
                      name))))
              (t (mv-let (erp val bindings)
                  (translate11-lambda-object name
                    '(nil)
                    nil
                    nil
                    nil
                    name
                    'verify-guards
                    wrld
                    state-vars
                    nil)
                  (declare (ignore bindings))
                  (mv erp
                    (if erp
                      val
                      (unquote val)))))))
          (t (er-cmp ctx
              "~x0 is not a symbol, a lambda object, or a lambda$ ~
                  expression.  See :DOC verify-guards."
              name)))))
    (let ((symbol-class (cond ((symbolp name) (symbol-class name wrld))
           ((member-equal name
              (global-val 'common-lisp-compliant-lambdas wrld)) :common-lisp-compliant)
           (t :program))))
      (cond ((and rrp (eq symbol-class :common-lisp-compliant)) (value-cmp 'redundant))
        ((consp name) (let* ((names (list name)) (guards (list (lambda-object-guard name)))
              (bodies (list (lambda-object-body name))))
            (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp names
                names
                guards
                wrld
                "guard"
                ctx)
              (chk-common-lisp-compliant-subfunctions-cmp names
                names
                bodies
                wrld
                "body"
                ctx)
              (value-cmp names))))
        ((getpropc name 'theorem nil wrld) (er-progn-cmp (chk-acceptable-verify-guards-formula-cmp name
              (getpropc name 'untranslated-theorem nil wrld)
              ctx
              wrld
              state-vars)
            (value-cmp (list name))))
        ((function-symbolp name wrld) (case symbol-class
            (:program (er-cmp ctx
                "~x0 is in :program mode.  Only :logic mode functions can ~
                   have their guards verified.  See :DOC verify-guards."
                name))
            ((:ideal :common-lisp-compliant) (let* ((recp (getpropc name 'recursivep nil wrld)) (names (cond ((null recp) (list name)) (t recp)))
                  (bad-names (if (eq symbol-class :ideal)
                      (collect-non-ideals names wrld)
                      (collect-programs names wrld))))
                (cond (bad-names (er-cmp ctx
                      "One or more of the mutually-recursive peers of ~
                            ~x0 ~#1~[was not defined in :logic mode~/either ~
                            was not defined in :logic mode or has already had ~
                            its guards verified~].  The offending ~
                            function~#2~[ is~/s are~] ~&2.  We thus cannot ~
                            verify the guards of ~x0.  This situation can ~
                            arise only through redefinition."
                      name
                      (if (eq symbol-class :ideal)
                        1
                        0)
                      bad-names))
                  (t (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp names
                        names
                        (guard-lst names nil wrld)
                        wrld
                        "guard"
                        ctx)
                      (chk-common-lisp-compliant-subfunctions-cmp names
                        names
                        (getprop-x-lst names 'unnormalized-body wrld)
                        wrld
                        "body"
                        ctx)
                      (value-cmp names))))))
            (otherwise (er-cmp ctx
                "Implementation error: Unexpected symbol-class, ~x0, for ~
                   the function symbol ~x1."
                symbol-class
                name))))
        (t (let ((fn (deref-macro-name name (macro-aliases wrld))))
            (er-cmp ctx
              "~x0 is not a function symbol or a theorem name in the ~
                    current ACL2 world.  ~@1"
              name
              (cond ((eq fn name) "See :DOC verify-guards.")
                (t (msg "Note that ~x0 is a macro-alias for ~x1.  ~
                                  Consider calling verify-guards with ~
                                  argument ~x1 instead, or use ~
                                  verify-guards+.  See :DOC verify-guards, ~
                                  see :DOC verify-guards+, and see :DOC ~
                                  macro-aliases-table."
                    name
                    fn))))))))))

(defun chk-acceptable-verify-guards
  (name rrp guard-simplify ctx wrld state)
  (cmp-to-error-triple (chk-acceptable-verify-guards-cmp name
      rrp
      guard-simplify
      ctx
      wrld
      (default-state-vars t))))

(defun guard-obligation-clauses
  (x guard-debug ens wrld state)
  (mv-let (cl-set cl-set-ttree)
    (cond ((and (consp x) (eq (car x) :term)) (mv-let (cl-set cl-set-ttree)
          (guard-clauses+ (cdr x)
            (and guard-debug :top-level)
            nil
            nil
            ens
            wrld
            (f-get-global 'safe-mode state)
            (gc-off state)
            nil
            nil)
          (mv cl-set cl-set-ttree)))
      ((and (consp x)
         (null (cdr x))
         (symbolp (car x))
         (getpropc (car x) 'theorem nil wrld)) (mv-let (cl-set cl-set-ttree)
          (guard-clauses+ (getpropc (car x) 'theorem nil wrld)
            (and guard-debug (car x))
            nil
            nil
            ens
            wrld
            (f-get-global 'safe-mode state)
            (gc-off state)
            nil
            nil)
          (mv cl-set cl-set-ttree)))
      (t (guard-clauses-for-clique x
          (cond ((null guard-debug) nil) ((cdr x) 'mut-rec) (t t))
          ens
          wrld
          (f-get-global 'safe-mode state)
          nil
          nil)))
    (mv-let (cl-set cl-set-ttree)
      (clean-up-clause-set cl-set
        (if (eq ens :do-not-simplify)
          nil
          ens)
        wrld
        cl-set-ttree
        state)
      (mv cl-set cl-set-ttree))))

(defun guard-obligation
  (x rrp guard-debug guard-simplify ctx state)
  (let* ((wrld (w state)) (namep (and (symbolp x)
          (not (keywordp x))
          (not (defined-constant x wrld)))))
    (er-let*-cmp ((y (cond (namep (chk-acceptable-verify-guards-cmp x
               rrp
               guard-simplify
               ctx
               wrld
               (default-state-vars t)))
           (t (chk-acceptable-verify-guards-formula-cmp nil
               x
               ctx
               wrld
               (default-state-vars t))))))
      (cond ((and namep (eq y 'redundant)) (value-cmp :redundant))
        (t (mv-let (cl-set cl-set-ttree)
            (guard-obligation-clauses y
              guard-debug
              (if (guard-simplify-p guard-simplify ctx)
                (ens state)
                :do-not-simplify)
              wrld
              state)
            (value-cmp (list* y cl-set cl-set-ttree))))))))

(defun prove-guard-clauses-msg
  (names cl-set
    cl-set-ttree
    displayed-goal
    verify-guards-formula-p
    guard-simplify
    ctx
    state)
  (let ((simp-phrase (tilde-*-simp-phrase cl-set-ttree)))
    (cond ((null cl-set) (fmt "The guard conjecture for ~#0~[this lambda expression~/~&1~/the ~
            given term~] is trivial to prove~#2~[~/, given ~*3~].~@4"
          (list (cons #\0
              (if names
                (if (consp (car names))
                  0
                  1)
                2))
            (cons #\1 names)
            (cons #\2
              (if (nth 4 simp-phrase)
                1
                0))
            (cons #\3 simp-phrase)
            (cons #\4
              (if verify-guards-formula-p
                "~|"
                "  ")))
          (proofs-co state)
          state
          nil))
      (t (pprogn (fms "The ~@0 for ~#1~[this lambda expression~/~&2~/the given ~
             term~]~#3~[~/, given ~*4,~] is~%~%Goal~%~Q56."
            (list (cons #\0
                (if (guard-simplify-p guard-simplify ctx)
                  "non-trivial part of the guard conjecture"
                  "guard conjecture (with only :limited ~
                           simplification)"))
              (cons #\1
                (if names
                  (if (consp (car names))
                    0
                    1)
                  2))
              (cons #\2 names)
              (cons #\3
                (if (nth 4 simp-phrase)
                  1
                  0))
              (cons #\4 simp-phrase)
              (cons #\5 displayed-goal)
              (cons #\6
                (or (term-evisc-tuple nil state)
                  (and (gag-mode)
                    (let ((tuple (gag-mode-evisc-tuple state)))
                      (cond ((eq tuple t) (term-evisc-tuple t state)) (t tuple)))))))
            (proofs-co state)
            state
            nil)
          (mv 0 state))))))

(defun verify-guards-formula-fn
  (x rrp guard-debug guard-simplify ctx state)
  (er-let* ((tuple (cmp-to-error-triple (guard-obligation x
           rrp
           guard-debug
           guard-simplify
           'verify-guards-formula
           state))))
    (cond ((eq tuple :redundant) (value :redundant))
      (t (let ((names (car tuple)) (displayed-goal (prettyify-clause-set (cadr tuple)
                (let*-abstractionp state)
                (w state)))
            (cl-set-ttree (cddr tuple)))
          (mv-let (col state)
            (prove-guard-clauses-msg (if (and (consp names) (eq (car names) :term))
                nil
                names)
              (cadr tuple)
              cl-set-ttree
              displayed-goal
              t
              guard-simplify
              ctx
              state)
            (declare (ignore col))
            (value :invisible)))))))

(defun prove-guard-clauses
  (names hints
    otf-flg
    guard-debug
    guard-simplify
    ctx
    ens
    wrld
    state)
  (cond ((ld-skip-proofsp state) (value '(0)))
    (t (mv-let (cl-set cl-set-ttree state)
        (pprogn (io? event
            nil
            state
            (names)
            (fms "Computing the guard conjecture for ~&0....~|"
              (list (cons #\0 names))
              (proofs-co state)
              state
              nil))
          (mv-let (cl-set cl-set-ttree)
            (guard-obligation-clauses names
              guard-debug
              (if (guard-simplify-p guard-simplify ctx)
                ens
                :do-not-simplify)
              wrld
              state)
            (mv cl-set cl-set-ttree state)))
        (pprogn (increment-timer 'other-time state)
          (let ((displayed-goal (prettyify-clause-set cl-set (let*-abstractionp state) wrld)))
            (mv-let (col state)
              (io? event
                nil
                (mv col state)
                (names cl-set
                  cl-set-ttree
                  displayed-goal
                  guard-simplify
                  ctx)
                (prove-guard-clauses-msg names
                  cl-set
                  cl-set-ttree
                  displayed-goal
                  nil
                  guard-simplify
                  ctx
                  state)
                :default-bindings ((col 0)))
              (pprogn (increment-timer 'print-time state)
                (cond ((null cl-set) (value (cons col cl-set-ttree)))
                  (t (mv-let (erp ttree state)
                      (prove (termify-clause-set cl-set)
                        (make-pspv ens
                          wrld
                          state
                          :displayed-goal displayed-goal
                          :otf-flg otf-flg)
                        hints
                        ens
                        wrld
                        ctx
                        state)
                      (cond (erp (mv-let (erp1 val state)
                            (er soft
                              ctx
                              "The proof of the guard conjecture for ~&0 has ~
                         failed.  You may wish to avoid specifying a guard, ~
                         or to supply option :VERIFY-GUARDS ~x1 with the ~
                         :GUARD.~@2~|"
                              names
                              nil
                              (if guard-debug
                                ""
                                "  Otherwise, you may wish to specify :GUARD-DEBUG ~
                           T; see :DOC verify-guards."))
                            (declare (ignore erp1))
                            (mv (msg "The proof of the guard conjecture for ~&0 has ~
                          failed; see the discussion above about ~&1.  "
                                names
                                (if guard-debug
                                  '(:verify-guards)
                                  '(:verify-guards :guard-debug)))
                              val
                              state)))
                        (t (mv-let (col state)
                            (io? event
                              nil
                              (mv col state)
                              (names)
                              (fmt "That completes the proof of the guard theorem ~
                               for ~&0.  "
                                (list (cons #\0 names))
                                (proofs-co state)
                                state
                                nil)
                              :default-bindings ((col 0)))
                            (pprogn (increment-timer 'print-time state)
                              (value (cons (or col 0) (cons-tag-trees cl-set-ttree ttree))))))))))))))))))

(defun maybe-remove-invariant-risk
  (names wrld new-wrld)
  (cond ((endp names) new-wrld)
    (t (let ((new-wrld (if (and (symbolp (car names))
               (getpropc (car names) 'invariant-risk nil wrld)
               (equal (guard (car names) t wrld) *t*))
             (putprop (car names) 'invariant-risk nil new-wrld)
             new-wrld)))
        (maybe-remove-invariant-risk (cdr names) wrld new-wrld)))))

(defun verify-guards-fn1
  (names hints otf-flg guard-debug guard-simplify ctx state)
  (let ((wrld (w state)) (ens (ens state)))
    (er-let* ((pair (prove-guard-clauses names
           hints
           otf-flg
           guard-debug
           guard-simplify
           ctx
           ens
           wrld
           state)))
      (let* ((col (car pair)) (ttree1 (cdr pair))
          (wrld1 (maybe-remove-invariant-risk names wrld wrld))
          (lambda-objects (and (not (global-val 'boot-strap-flg wrld1))
              (collect-well-formed-lambda-objects-lst names wrld1)))
          (wrld2 (global-set 'common-lisp-compliant-lambdas
              (union-equal lambda-objects
                (global-val 'common-lisp-compliant-lambdas wrld1))
              wrld1))
          (wrld3 (if (and (consp names) (consp (car names)))
              wrld2
              (putprop-x-lst1 names
                'symbol-class
                :common-lisp-compliant wrld2))))
        (pprogn (print-verify-guards-msg names col state)
          (value (cons wrld3 ttree1)))))))

(defun convert-runes-to-unordered-mapping-pairs
  (lst wrld ans)
  (cond ((endp lst) ans)
    (t (convert-runes-to-unordered-mapping-pairs (cdr lst)
        wrld
        (let ((pair (frunic-mapping-pair (car lst) wrld)))
          (cond (pair (cons pair ans)) (t ans)))))))

(defun augment-theory-weak
  (lst wrld)
  (declare (xargs :guard (true-listp lst)))
  (duplicitous-sort-car nil
    (convert-runes-to-unordered-mapping-pairs lst wrld nil)))

(defun with-useless-runes-aux
  (name state)
  (let ((useless-runes (f-get-global 'useless-runes state)))
    (cond ((or (null useless-runes)
         (null name)
         (ld-skip-proofsp state)
         (global-val 'include-book-path (w state))) (mv nil nil useless-runes))
      ((eq (access useless-runes useless-runes :tag) 'fast-alist) (let* ((fal (access useless-runes useless-runes :data)) (lst (cdr (hons-get name fal))))
          (cond ((consp lst) (let* ((runes (car lst)) (fal (hons-acons name (cdr lst) fal))
                  (useless-runes-2 (change useless-runes useless-runes :data fal)))
                (cond (t (mv 'read
                      (change useless-runes
                        useless-runes
                        :tag 'theory
                        :data (augment-theory-weak runes (w state)))
                      useless-runes-2)))))
            (t (mv nil nil useless-runes)))))
      ((and (eq (access useless-runes useless-runes :tag) 'channel)) (mv 'write
          (access useless-runes useless-runes :data)
          useless-runes))
      (t (mv nil nil useless-runes)))))

(defun accp-info (state) (read-acl2-oracle state))

(defun useless-runes
  (accp-info)
  (let* ((totals (access accp-info accp-info :totals)) (alist (merge-sort-lexorder (show-accumulated-persistence-phrase2 :useless (car (last totals))
            nil))))
    (show-accumulated-persistence-list (show-accumulated-persistence-remove-useless alist nil)
      nil)))

(defun bad-useless-runes
  (useless-runes known-pkgs acc)
  (cond ((endp useless-runes) (reverse acc))
    (t (bad-useless-runes (cdr useless-runes)
        known-pkgs
        (let ((rune (caddr (car useless-runes))))
          (if (member-equal (symbol-package-name (base-symbol rune))
              known-pkgs)
            acc
            (cons (car useless-runes) acc)))))))

(defun set-difference-equal-sorted
  (lst1 lst2)
  (cond ((null lst2) lst1)
    ((endp lst1) (er hard?
        'set-difference-equal-sorted
        "Implementation error: Reached end of lst1 before end of lst2."))
    ((equal (car lst1) (car lst2)) (set-difference-equal-sorted (cdr lst1) (cdr lst2)))
    (t (cons (car lst1)
        (set-difference-equal-sorted (cdr lst1) lst2)))))

(defun remove-executable-counterpart-useless-runes1
  (useless-runes)
  (cond ((endp useless-runes) nil)
    (t (let ((rune (caddr (car useless-runes))))
        (cond ((eq (car rune) :executable-counterpart) (remove-executable-counterpart-useless-runes1 (cdr useless-runes)))
          (t (cons rune
              (remove-executable-counterpart-useless-runes1 (cdr useless-runes)))))))))

(defun executable-counterpart-useless-runes-p
  (useless-runes)
  (cond ((endp useless-runes) nil)
    (t (let ((rune (caddr (car useless-runes))))
        (cond ((eq (car rune) :executable-counterpart) t)
          (t (executable-counterpart-useless-runes-p (cdr useless-runes))))))))

(defun remove-executable-counterpart-useless-runes
  (useless-runes)
  (cond ((executable-counterpart-useless-runes-p useless-runes) (remove-executable-counterpart-useless-runes1 useless-runes))
    (t useless-runes)))

(defun print-rune
  (rune channel state)
  (pprogn (princ$ #\( channel state)
    (prin1$ (car rune) channel state)
    (princ$ #\  channel state)
    (prin1$ (cadr rune) channel state)
    (cond ((cddr rune) (pprogn (princ$ " . " channel state)
          (prin1$ (cddr rune) channel state)))
      (t state))
    (princ$ #\) channel state)))

(defun useless-runes-report-p
  (lst)
  (cond ((atom lst) (null lst))
    ((let ((x (car lst)))
       (and (true-listp x)
         (natp (car x))
         (natp (cadr x))
         (caddr x)
         (null (cdddr x)))) (useless-runes-report-p (cdr lst)))
    (t nil)))

(defun print-useless-runes-tuples-rec
  (lst channel state)
  (declare (xargs :guard (useless-runes-report-p lst)))
  (cond ((endp lst) (pprogn (newline channel state)
        (princ$ " )" channel state)
        (newline channel state)))
    (t (let* ((triple (car lst)) (n1 (car triple))
          (n2 (cadr triple))
          (rune (caddr triple)))
        (pprogn (newline channel state)
          (princ$ " (" channel state)
          (prin1$ n1 channel state)
          (princ$ #\  channel state)
          (prin1$ n2 channel state)
          (princ$ #\  channel state)
          (print-rune rune channel state)
          (princ$ #\) channel state)
          (print-useless-runes-tuples-rec (cdr lst) channel state))))))

(defun print-useless-runes-tuples
  (lst channel state)
  (declare (xargs :guard (useless-runes-report-p lst)))
  (cond ((null lst) (pprogn (princ$ #\) channel state) (newline channel state)))
    (t (print-useless-runes-tuples-rec lst channel state))))

(defun print-useless-runes
  (name channel known-pkgs state)
  (error-free-triple-to-state 'print-useless-runes
    (er-let* ((accp-info (accp-info state)))
      (state-global-let* ((current-package "ACL2" set-current-package-state) (fmt-hard-right-margin 10000 set-fmt-hard-right-margin)
          (fmt-soft-right-margin 10000 set-fmt-soft-right-margin))
        (let* ((bad-pkg (not (member-equal (symbol-package-name name) known-pkgs))) (useless-runes0 (remove-executable-counterpart-useless-runes (useless-runes accp-info)))
            (bad-tuples (and (not bad-pkg)
                (bad-useless-runes useless-runes0 known-pkgs nil)))
            (useless-runes (if (null bad-tuples)
                useless-runes0
                (set-difference-equal-sorted useless-runes0 bad-tuples))))
          (pprogn (cond (bad-tuples (pprogn (princ$ "; Just below, skipping the following list where the rune"
                    channel
                    state)
                  (newline channel state)
                  (princ$ "; has an unknown package in the certification world:"
                    channel
                    state)
                  (newline channel state)
                  (princ$ "#|" channel state)
                  (newline channel state)
                  (princ$ "(" channel state)
                  (print-useless-runes-tuples bad-tuples channel state)
                  (princ$ "|#" channel state)
                  (newline channel state)))
              (bad-pkg (pprogn (princ$ "; Omitting the following entry because the package of"
                    channel
                    state)
                  (newline channel state)
                  (princ$ "; the event name is unknown in the certification world."
                    channel
                    state)
                  (newline channel state)
                  (princ$ "#|" channel state)
                  (newline channel state)))
              (t state))
            (princ$ #\( channel state)
            (prin1$ name channel state)
            (print-useless-runes-tuples useless-runes channel state)
            (cond (bad-pkg (pprogn (princ$ "|#" channel state) (newline channel state)))
              (t state))
            (prog2$ (accumulated-persistence nil) (value nil))))))))

(defun augmented-runes-after-1
  (nume pairs)
  (cond ((endp pairs) nil)
    ((> (caar pairs) nume) (cons (car pairs)
        (augmented-runes-after-1 nume (cdr pairs))))
    (t nil)))

(defun augmented-runes-after
  (nume wrld ans)
  (cond ((endp wrld) (reverse ans))
    ((and (eq (cadr (car wrld)) 'runic-mapping-pairs)
       (not (eq (cddr (car wrld)) *acl2-property-unbound*))) (let ((pairs (cddr (car wrld))))
        (cond ((null pairs) (augmented-runes-after nume (cdr wrld) ans))
          ((> (caar pairs) nume) (augmented-runes-after nume (cdr wrld) (append pairs ans)))
          ((<= (car (car (last pairs))) nume) (reverse ans))
          (t (revappend ans (augmented-runes-after-1 nume pairs))))))
    (t (augmented-runes-after nume (cdr wrld) ans))))

(defun extend-set-difference-theories
  (thy1 thy2 nm1 wrld)
  (let ((thy1++ (augmented-runes-after nm1 wrld nil)))
    (append (set-difference-augmented-theories thy1++ thy2 nil)
      (set-difference-augmented-theories thy1 thy2 nil))))

(defun useless-runes-ens
  (ens wrld state)
  (let ((active-useless-runes (active-useless-runes state)))
    (cond (active-useless-runes (let* ((ens-theory (cdr (access enabled-structure ens :theory-array))) (index-of-last-enabling (access enabled-structure ens :index-of-last-enabling))
            (ext-p (< index-of-last-enabling (caar active-useless-runes))))
          (mv-let (index-of-last-enabling thy)
            (cond (ext-p (mv (caar active-useless-runes)
                  (extend-set-difference-theories ens-theory
                    active-useless-runes
                    index-of-last-enabling
                    wrld)))
              (t (mv index-of-last-enabling
                  (set-difference-augmented-theories ens-theory
                    active-useless-runes
                    nil))))
            (load-theory-into-enabled-structure-1 thy
              (if ext-p
                'ext-p
                t)
              ens
              t
              index-of-last-enabling
              wrld))))
      (t ens))))

(defun verify-guards-old-dcl-alist
  (fn wrld)
  (let ((ev (get-defun-event fn wrld)))
    (and ev
      (assert$ (and (consp ev) (member-eq (car ev) '(defun defund)))
        (let* ((dcls (butlast (cdddr ev) 1)) (h-lst (fetch-dcl-field :guard-hints dcls))
            (d-lst (fetch-dcl-field :guard-debug dcls))
            (s-lst (fetch-dcl-field :guard-simplify dcls)))
          (append (and h-lst (list (cons :guard-hints (car h-lst))))
            (and d-lst (list (cons :guard-debug (car d-lst))))
            (and s-lst (list (cons :guard-simplify (car s-lst))))))))))

(defun verify-guards-fn
  (name state
    hints
    hints-p
    otf-flg
    guard-debug
    guard-debug-p
    guard-simplify
    guard-simplify-p
    event-form)
  (when-logic "VERIFY-GUARDS"
    (with-ctx-summarized (cond ((and (null hints) (null otf-flg)) (msg "( VERIFY-GUARDS ~x0)" name))
        (t (cons 'verify-guards name)))
      (let* ((wrld (w state)) (event-form (or event-form
              (list* 'verify-guards
                name
                (append (if hints
                    (list :hints hints)
                    nil)
                  (if otf-flg
                    (list :otf-flg otf-flg)
                    nil)))))
          (assumep (or (eq (ld-skip-proofsp state) 'include-book)
              (eq (ld-skip-proofsp state) 'include-book-with-locals)
              (eq (ld-skip-proofsp state) 'initialize-acl2)))
          (old-alist (and (symbolp name) (verify-guards-old-dcl-alist name wrld)))
          (guard-simplify (if (and (not guard-simplify-p)
                (assoc-eq :guard-simplify old-alist))
              (cdr (assoc-eq :guard-simplify old-alist))
              guard-simplify)))
        (er-let* ((names (chk-acceptable-verify-guards name
               t
               guard-simplify
               ctx
               wrld
               state)))
          (cond ((eq names 'redundant) (stop-redundant-event ctx state))
            (t (enforce-redundancy event-form
                ctx
                wrld
                (with-useless-runes name
                  wrld
                  (let ((hints (if (and (not hints-p) (assoc-eq :guard-hints old-alist))
                         (cdr (assoc-eq :guard-hints old-alist))
                         hints)) (guard-debug (if (and (not guard-debug-p) (assoc-eq :guard-debug old-alist))
                          (cdr (assoc-eq :guard-debug old-alist))
                          guard-debug)))
                    (er-let* ((hints (if assumep
                           (value nil)
                           (translate-hints+ (cons "Guard Lemma for" name)
                             hints
                             (default-hints wrld)
                             ctx
                             wrld
                             state))) (pair (verify-guards-fn1 names
                            hints
                            otf-flg
                            guard-debug
                            guard-simplify
                            ctx
                            state)))
                      (er-progn (chk-assumption-free-ttree (cdr pair) ctx state)
                        (install-event name
                          event-form
                          'verify-guards
                          0
                          (cdr pair)
                          nil
                          nil
                          nil
                          (car pair)
                          state))))))))))
      :event-type 'verify-guards
      :event event-form)))

(defun project-out-columns-i-and-j
  (i j table)
  (cond ((null table) nil)
    (t (cons (cons (nth i (car table)) (nth j (car table)))
        (project-out-columns-i-and-j i j (cdr table))))))

(defun super-defun-wart-bindings
  (bindings)
  (cond ((null bindings) nil)
    (t (cons (or (assoc-eq (caar bindings) *super-defun-wart-binding-alist*)
          (car bindings))
        (super-defun-wart-bindings (cdr bindings))))))

(defun store-stobjs-ins
  (names stobjs-ins w)
  (cond ((null names) w)
    (t (store-stobjs-ins (cdr names)
        (cdr stobjs-ins)
        (putprop (car names) 'stobjs-in (car stobjs-ins) w)))))

(defun store-super-defun-warts-stobjs-in
  (names wrld)
  (cond ((null names) wrld)
    ((assoc-eq (car names) *super-defun-wart-stobjs-in-alist*) (store-super-defun-warts-stobjs-in (cdr names)
        (putprop (car names)
          'stobjs-in
          (cdr (assoc-eq (car names) *super-defun-wart-stobjs-in-alist*))
          wrld)))
    (t (store-super-defun-warts-stobjs-in (cdr names) wrld))))

(defun collect-old-nameps
  (names wrld)
  (cond ((null names) nil)
    ((new-namep (car names) wrld) (collect-old-nameps (cdr names) wrld))
    (t (cons (car names) (collect-old-nameps (cdr names) wrld)))))

(defun put-invariant-risk1
  (new-fns body-fns wrld)
  (cond ((endp body-fns) wrld)
    (t (let ((risk-fn (getpropc (car body-fns) 'invariant-risk nil wrld)))
        (cond (risk-fn (putprop-x-lst1 new-fns 'invariant-risk risk-fn wrld))
          (t (put-invariant-risk1 new-fns (cdr body-fns) wrld)))))))

(defun stobjs-guard-only-lst
  (lst wrld)
  (cond ((endp lst) t)
    (t (and (let ((term (car lst)))
          (and (nvariablep term)
            (symbolp (ffn-symb term))
            (fargs term)
            (null (cdr (fargs term)))
            (variablep (fargn term 1))
            (stobj-recognizer-p (ffn-symb term) wrld)))
        (stobjs-guard-only-lst (cdr lst) wrld)))))

(defun stobjs-guard-only
  (guard wrld)
  (stobjs-guard-only-lst (flatten-ands-in-lit guard) wrld))

(defun remove-guard-t
  (names guards wrld acc)
  (cond ((endp names) acc)
    (t (remove-guard-t (cdr names)
        (cdr guards)
        wrld
        (if (or (equal (car guards) *t*)
            (stobjs-guard-only (car guards) wrld))
          acc
          (cons (car names) acc))))))

(defun put-invariant-risk
  (names bodies non-executablep symbol-class guards wrld)
  (cond ((or non-executablep
       (null (get-register-invariant-risk-world wrld))) wrld)
    (t (let ((new-fns (if (eq symbol-class :common-lisp-compliant)
             (remove-guard-t names guards wrld nil)
             names)))
        (cond ((null new-fns) wrld)
          (t (let ((pair (assoc-eq (car new-fns) *boot-strap-invariant-risk-alist*)))
              (cond (pair (if (cdr pair)
                    (putprop-x-lst1 new-fns 'invariant-risk (car new-fns) wrld)
                    wrld))
                (t (put-invariant-risk1 new-fns
                    (all-fnnames1-exec t bodies nil)
                    wrld))))))))))

(defun defuns-fn-short-cut
  (loop$-recursion-checkedp loop$-recursion
    names
    docs
    pairs
    guards
    measures
    split-types-terms
    bodies
    non-executablep
    ctx
    wrld
    state)
  (declare (ignore docs pairs))
  (prog2$ (choke-on-loop$-recursion loop$-recursion-checkedp
      names
      bodies
      'defuns-fn-short-cut)
    (er-progn (cond ((and (null (cdr names))
           (not (equal (car measures) *no-measure*))
           (not loop$-recursion)
           (not (ffnnamep-mod-mbe (car names) (car bodies)))) (maybe-warn-or-error-on-non-rec-measure (car names)
            ctx
            wrld
            state))
        (t (value nil)))
      (let* ((boot-strap-flg (global-val 'boot-strap-flg wrld)) (wrld0 (cond (non-executablep (putprop-x-lst1 names 'non-executablep non-executablep wrld))
              (t wrld)))
          (wrld1 (cond (boot-strap-flg wrld0)
              (t (putprop-x-lst2 names 'unnormalized-body bodies wrld0))))
          (wrld2 (put-invariant-risk names
              bodies
              non-executablep
              :program guards
              (putprop-x-lst2-unless names
                'guard
                guards
                *t*
                (putprop-x-lst2-unless names
                  'split-types-term
                  split-types-terms
                  *t*
                  wrld1)))))
        (value (cons wrld2 nil))))))

(defun print-defun-msg/collect-type-prescriptions
  (names wrld)
  (cond ((null names) (mv nil nil))
    (t (mv-let (fns alist)
        (print-defun-msg/collect-type-prescriptions (cdr names)
          wrld)
        (let ((lst (getpropc (car names) 'type-prescriptions nil wrld)))
          (cond ((null lst) (mv (cons (car names) fns) alist))
            (t (mv fns
                (cons (cons (car names)
                    (untranslate (access type-prescription (car lst) :corollary)
                      t
                      wrld))
                  alist)))))))))

(defun print-defun-msg/type-prescriptions1
  (alist simp-phrase col state)
  (cond ((null alist) (mv col state))
    ((null (cdr alist)) (fmt1 "the type of ~xn is described by the theorem ~Pt0.  ~#p~[~/We ~
                used ~*s.~]~|"
        (list (cons #\n (caar alist))
          (cons #\t (cdar alist))
          (cons #\0 (term-evisc-tuple nil state))
          (cons #\p
            (if (nth 4 simp-phrase)
              1
              0))
          (cons #\s simp-phrase))
        col
        (proofs-co state)
        state
        nil))
    ((null (cddr alist)) (fmt1 "the type of ~xn is described by the theorem ~Pt0 ~
                and the type of ~xm is described by the theorem ~Ps0.~|"
        (list (cons #\n (caar alist))
          (cons #\t (cdar alist))
          (cons #\0 (term-evisc-tuple nil state))
          (cons #\m (caadr alist))
          (cons #\s (cdadr alist)))
        col
        (proofs-co state)
        state
        nil))
    (t (mv-let (col state)
        (fmt1 "the type of ~xn is described by the theorem ~Pt0, "
          (list (cons #\n (caar alist))
            (cons #\t (cdar alist))
            (cons #\0 (term-evisc-tuple nil state)))
          col
          (proofs-co state)
          state
          nil)
        (print-defun-msg/type-prescriptions1 (cdr alist)
          simp-phrase
          col
          state)))))

(defun print-defun-msg/type-prescriptions
  (names ttree wrld col state)
  (let ((simp-phrase (tilde-*-simp-phrase ttree)))
    (mv-let (fns alist)
      (print-defun-msg/collect-type-prescriptions names wrld)
      (cond ((null alist) (fmt1 "  We could deduce no constraints on the type of ~#0~[~&0.~/any of ~
          the functions in the clique.~]~#1~[~/  However, in normalizing the ~
          definition~#0~[~/s~] we used ~*2.~]~%"
            (list (cons #\0 names)
              (cons #\1
                (if (nth 4 simp-phrase)
                  1
                  0))
              (cons #\2 simp-phrase))
            col
            (proofs-co state)
            state
            nil))
        (fns (mv-let (col state)
            (fmt1 "  We could deduce no constraints on the type of ~#f~[~vf,~/any of ~
            ~vf,~] but we do observe that "
              (list (cons #\f fns))
              col
              (proofs-co state)
              state
              nil)
            (print-defun-msg/type-prescriptions1 alist
              simp-phrase
              col
              state)))
        (t (mv-let (col state)
            (fmt1 "  We observe that "
              nil
              col
              (proofs-co state)
              state
              nil)
            (print-defun-msg/type-prescriptions1 alist
              simp-phrase
              col
              state)))))))

(defun simple-signaturep
  (fn wrld)
  (and (all-nils (stobjs-in fn wrld))
    (let ((stobjs-out (getpropc fn 'stobjs-out '(nil) wrld)))
      (and (null (cdr stobjs-out))
        (not (eq (car stobjs-out) :df))))))

(defun all-simple-signaturesp
  (names wrld)
  (cond ((endp names) t)
    (t (and (simple-signaturep (car names) wrld)
        (all-simple-signaturesp (cdr names) wrld)))))

(defun print-defun-msg/signatures1
  (names wrld state)
  (cond ((endp names) state)
    ((not (simple-signaturep (car names) wrld)) (pprogn (fms "~x0 => ~x1."
          (list (cons #\0
              (cons (car names)
                (prettyify-stobj-flags (stobjs-in (car names) wrld))))
            (cons #\1
              (prettyify-stobjs-out (getpropc (car names) 'stobjs-out '(nil) wrld))))
          (proofs-co state)
          state
          nil)
        (print-defun-msg/signatures1 (cdr names) wrld state)))
    (t (print-defun-msg/signatures1 (cdr names) wrld state))))

(defun print-defun-msg/signatures
  (names wrld state)
  (cond ((all-simple-signaturesp names wrld) state)
    ((cdr names) (pprogn (fms "The Non-simple Signatures:"
          nil
          (proofs-co state)
          state
          nil)
        (print-defun-msg/signatures1 names wrld state)
        (newline (proofs-co state) state)))
    (t (pprogn (print-defun-msg/signatures1 names wrld state)
        (newline (proofs-co state) state)))))

(defun print-defun-msg
  (names ttree wrld col state)
  (cond ((ld-skip-proofsp state) state)
    (t (io? event
        nil
        state
        (names ttree wrld col)
        (pprogn (increment-timer 'other-time state)
          (mv-let (erp ttree state)
            (accumulate-ttree-and-step-limit-into-state ttree
              :skip state)
            (declare (ignore erp))
            (mv-let (col state)
              (print-defun-msg/type-prescriptions names
                ttree
                wrld
                col
                state)
              (declare (ignore col))
              (pprogn (print-defun-msg/signatures names wrld state)
                (increment-timer 'print-time state)))))))))

(defun get-ignores
  (lst)
  (cond ((null lst) nil)
    (t (cons (ignore-vars (fourth (car lst)))
        (get-ignores (cdr lst))))))

(defun get-ignorables
  (lst)
  (cond ((null lst) nil)
    (t (cons (ignorable-vars (fourth (car lst)))
        (get-ignorables (cdr lst))))))

(defun irrelevant-vars
  (dcls)
  (cond ((null dcls) nil)
    ((eq (caar dcls) 'irrelevant) (append (cdar dcls) (irrelevant-vars (cdr dcls))))
    (t (irrelevant-vars (cdr dcls)))))

(defun get-irrelevants
  (lst)
  (cond ((null lst) nil)
    (t (cons (irrelevant-vars (fourth (car lst)))
        (get-irrelevants (cdr lst))))))

(defun chk-all-stobj-names
  (lst src msg ctx wrld state)
  (cond ((endp lst) (value nil))
    ((not (stobjp (car lst) t wrld)) (er soft
        ctx
        "Every name used as a stobj ~@0 must have been previously ~
              defined as a single-threaded object with defstobj or ~
              defabsstobj.  ~x1 is used as stobj name ~#2~[~/in ~@2 ~]but has ~
              not been defined as a stobj."
        (cond ((eq src :stobjs) "with a :STOBJS keyword")
          ((eq src :stobjs?) "(whether declared explicitly via the :STOBJS keyword ~
                     argument or implicitly via *-notation)")
          ((eq src :global-stobjs) "with a :GLOBAL-STOBJS keyword")
          (t (er hard
              ctx
              "Implementation error: unexpected case of src, ~x0. ~
                           Please report this error to the ACL2 implementors."
              src)))
        (car lst)
        msg))
    (t (chk-all-stobj-names (cdr lst) src msg ctx wrld state))))

(defun get-declared-kwd-names
  (kwd edcls ctx wrld state)
  (cond ((endp edcls) (value nil))
    ((eq (caar edcls) 'xargs) (let* ((temp (assoc-keyword kwd (cdar edcls))) (lst (cond ((null temp) nil)
              ((null (cadr temp)) nil)
              ((atom (cadr temp)) (list (cadr temp)))
              (t (cadr temp)))))
        (cond (lst (cond ((not (symbol-listp lst)) (er soft
                  ctx
                  "The value specified for the ~x0 xarg must be a true ~
                    list of symbols and ~x1 is not."
                  kwd
                  lst))
              (t (er-progn (case kwd
                    (:stobjs (chk-all-stobj-names lst
                        :stobjs (msg "... :stobjs ~x0 ..." (cadr temp))
                        ctx
                        wrld
                        state))
                    (:dfs (value nil))
                    (t (value (er hard
                          'get-declared-kwd-names
                          "Implementation error: Unexpected keyword, ~
                                   ~x0"
                          kwd))))
                  (er-let* ((rst (get-declared-kwd-names kwd (cdr edcls) ctx wrld state)))
                    (value (union-eq lst rst)))))))
          (t (get-declared-kwd-names kwd (cdr edcls) ctx wrld state)))))
    (t (get-declared-kwd-names kwd (cdr edcls) ctx wrld state))))

(defun get-stobjs-in-lst
  (lst defun-mode ctx wrld state)
  (cond ((null lst) (value nil))
    (t (let ((fn (first (car lst))) (formals (second (car lst))))
        (er-let* ((dcl-stobj-names (get-declared-kwd-names :stobjs (fourth (car lst))
               ctx
               wrld
               state)) (dcl-df-names-1 (get-declared-kwd-names :dfs (fourth (car lst))
                ctx
                wrld
                state))
            (dcl-df-names-2 (value (extend-known-dfs-with-declared-df-types (fourth (car lst))
                  nil)))
            (dcl-stobj-namesx (cond ((and (member-eq 'state formals)
                   (not (member-eq 'state dcl-stobj-names))) (er-progn (cond ((and (eq defun-mode :logic) (function-symbolp fn wrld)) (value nil))
                      (t (chk-state-ok ctx wrld state)))
                    (value (cons 'state dcl-stobj-names))))
                (t (value dcl-stobj-names)))))
          (cond ((not (subsetp-eq dcl-stobj-namesx formals)) (er soft
                ctx
                "The stobj name~#0~[ ~&0 is~/s ~&0 are~] ~
                        declared but not among the formals of ~x1.  ~
                        This generally indicates some kind of ~
                        typographical error and is illegal.  Declare ~
                        only those stobj names listed in the formals. ~
                        The formals list of ~x1 is ~x2."
                (set-difference-equal dcl-stobj-namesx formals)
                fn
                formals))
            ((or (intersectp-eq dcl-stobj-namesx dcl-df-names-1)
               (intersectp-eq dcl-stobj-namesx dcl-df-names-2)) (mv-let (n int)
                (if (intersectp-eq dcl-stobj-namesx dcl-df-names-1)
                  (mv 0 (intersection-eq dcl-stobj-namesx dcl-df-names-1))
                  (mv 1 (intersection-eq dcl-stobj-namesx dcl-df-names-2)))
                (er soft
                  ctx
                  "The formal~#0~[ ~&0 of function ~x1 is~/s of ~
                          function ~x1 ~&0 are each~] declared both with ~
                          xargs :STOBJS and with ~#2~[xargs :DFS~/a ~
                          double-float type declaration~].  But a formal ~
                          cannot name both a stobj and a df."
                  int
                  fn
                  n)))
            (t (er-let* ((others (get-stobjs-in-lst (cdr lst) defun-mode ctx wrld state)))
                (value (cons (compute-stobj-flags formals
                      dcl-stobj-namesx
                      (union-eq dcl-df-names-1 dcl-df-names-2)
                      wrld)
                    others))))))))))

(defun chk-stobjs-out-bound
  (names bindings ctx state)
  (cond ((null names) (value nil))
    ((translate-unbound (car names) bindings) (er soft
        ctx
        "Translate failed to determine the output signature of ~
              ~x0."
        (car names)))
    (t (chk-stobjs-out-bound (cdr names) bindings ctx state))))

(defun store-stobjs-out
  (names bindings w)
  (cond ((null names) w)
    (t (store-stobjs-out (cdr names)
        bindings
        (putprop (car names)
          'stobjs-out
          (translate-deref (car names) bindings)
          w)))))

(defun unparse-signature
  (x)
  (let* ((fn (car x)) (pretty-flags1 (prettyify-stobj-flags (caddr x)))
      (output (prettyify-stobjs-out (cadddr x))))
    `((,FN ,@PRETTY-FLAGS1) => ,OUTPUT)))

(defun chk-defun-mode
  (defun-mode ctx state)
  (cond ((eq defun-mode :program) (value nil))
    ((eq defun-mode :logic) (value nil))
    (t (er soft
        ctx
        "The legal defun-modes are :program and :logic.  ~x0 is ~
                not a recognized defun-mode."
        defun-mode))))

(defun dcl-fields1
  (lst)
  (declare (xargs :guard (plausible-dclsp1 lst)))
  (cond ((endp lst) nil)
    ((member-eq (caar lst) '(type ignore ignorable)) (add-to-set-eq (caar lst) (dcl-fields1 (cdr lst))))
    (t (union-eq (evens (cdar lst)) (dcl-fields1 (cdr lst))))))

(defun dcl-fields
  (lst)
  (declare (xargs :guard (plausible-dclsp lst)))
  (cond ((endp lst) nil)
    ((stringp (car lst)) (add-to-set-eq 'comment (dcl-fields (cdr lst))))
    (t (union-eq (dcl-fields1 (cdar lst)) (dcl-fields (cdr lst))))))

(defun set-equalp-eq
  (lst1 lst2)
  (declare (xargs :guard (and (true-listp lst1)
        (true-listp lst2)
        (or (symbol-listp lst1) (symbol-listp lst2)))))
  (and (subsetp-eq lst1 lst2) (subsetp-eq lst2 lst1)))

(defun non-identical-defp-chk-measures
  (name new-measures old-measures justification)
  (cond ((equal new-measures old-measures) nil)
    (t (let ((old-measured-subset (assert$ justification
             (access justification justification :subset))))
        (cond ((and (consp new-measures)
             (null (cdr new-measures))
             (let ((new-measure (car new-measures)))
               (or (equal new-measure (car old-measures))
                 (and (true-listp new-measure)
                   (eq (car new-measure) :?)
                   (arglistp (cdr new-measure))
                   (set-equalp-eq old-measured-subset (cdr new-measure)))))) nil)
          (old-measures (msg "the proposed and existing definitions for ~x0 differ on their ~
              measures.  The proposed measure is ~x1 but the existing measure ~
              is ~x2.  The proposed measure needs to be specified explicitly ~
              in fully translated form with :measure (see :DOC xargs), either ~
              to be identical to the existing measure or to be a call of :? ~
              on the measured subset; for example, ~x3 will serve as the ~
              proposed :measure."
              name
              (car new-measures)
              (car old-measures)
              (cons :? old-measured-subset)))
          (t (msg "the existing definition for ~x0 does not have an explicitly ~
              specified measure.  Either remove the :measure declaration from ~
              your proposed definition, or else specify a :measure that ~
              applies :? to the existing measured subset, for example, ~x1."
              name
              (cons :? old-measured-subset))))))))

(defun non-identical-defp
  (def1 def2 chk-measure-p wrld)
  (let* ((justification (and chk-measure-p
         (getpropc (car def2) 'justification nil wrld))) (all-but-body1 (butlast (cddr def1) 1))
      (all-but-body2 (butlast (cddr def2) 1))
      (ruler-extenders1-lst (fetch-dcl-field :ruler-extenders all-but-body1))
      (ruler-extenders2-lst (fetch-dcl-field :ruler-extenders all-but-body2)))
    (cond ((and justification
         (or (not (equal ruler-extenders1-lst ruler-extenders2-lst))
           (and (null ruler-extenders1-lst)
             (not (equal (access justification justification :ruler-extenders)
                 (default-ruler-extenders wrld)))))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            ruler-extenders (see :DOC ruler-extenders).  The proposed ~
            ruler-extenders value does not match the existing ruler-extenders ~
            for ~x0, namely, ~x1."
          (car def1)
          (access justification justification :ruler-extenders)))
      ((equal def1 def2) nil)
      ((not (eq (car def1) (car def2))) (msg "the name of the new event, ~x0, differs from the name of the ~
            corresponding existing event, ~x1."
          (car def1)
          (car def2)))
      ((not (equal (cadr def1) (cadr def2))) (msg "the proposed argument list for ~x0, ~x1, differs from the ~
            existing argument list, ~x2."
          (car def1)
          (cadr def1)
          (cadr def2)))
      ((not (equal (car (last def1)) (car (last def2)))) (msg "the proposed body for ~x0,~|~%~p1,~|~%differs from the existing ~
            body,~|~%~p2.~|~%"
          (car def1)
          (car (last def1))
          (car (last def2))))
      ((not (equal (fetch-dcl-field :non-executable all-but-body1)
           (fetch-dcl-field :non-executable all-but-body2))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            :non-executable declarations."
          (car def1)))
      ((not (equal (fetch-dcl-field :type-prescription all-but-body1)
           (fetch-dcl-field :type-prescription all-but-body2))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            :type-prescription declarations."
          (car def1)))
      ((flet ((normalize-value (x)
            (cond ((equal x '(nil)) nil)
              ((or (equal x '(t)) (null x)) t)
              (t (er hard
                  'non-identical-defp
                  "Internal error: Unexpected value when processing ~
                            :normalize xargs keyword, ~x0.  Please contact ~
                            the ACL2 implementors."
                  x)))))
         (not (equal (normalize-value (fetch-dcl-field :normalize all-but-body1))
             (normalize-value (fetch-dcl-field :normalize all-but-body2))))) (msg "the proposed and existing definitions for ~x0 differ on the ~
            values supplied by :normalize declarations."
          (car def1)))
      ((not (let ((stobjs1 (fetch-dcl-field :stobjs all-but-body1)) (stobjs2 (fetch-dcl-field :stobjs all-but-body2)))
           (or (equal stobjs1 stobjs2)
             (equal (remove1-eq 'state stobjs1)
               (remove1-eq 'state stobjs2))))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            :stobjs declarations."
          (car def1)))
      ((not (equal (fetch-dcl-field :dfs all-but-body1)
           (fetch-dcl-field :dfs all-but-body2))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            :dfs declarations."
          (car def1)))
      ((not (equal (fetch-dcl-field 'type all-but-body1)
           (fetch-dcl-field 'type all-but-body2))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            type declarations."
          (car def1)))
      ((let* ((guards1 (fetch-dcl-field :guard all-but-body1)) (guards1-trivial-p (or (null guards1) (equal guards1 '(t))))
           (guards2 (fetch-dcl-field :guard all-but-body2))
           (guards2-trivial-p (or (null guards2) (equal guards2 '(t)))))
         (cond ((and guards1-trivial-p guards2-trivial-p) nil)
           ((not (equal guards1 guards2)) (msg "the proposed and existing definitions for ~x0 differ on ~
                     their :guard declarations."
               (car def1)))
           ((not (equal (fetch-dcl-fields '(type :guard) all-but-body1)
                (fetch-dcl-fields '(type :guard) all-but-body2))) (msg "although the proposed and existing definitions for ~x0 ~
                     agree on the their type and :guard declarations, they ~
                     disagree on the combined orders of those declarations.")))))
      ((let ((split-types1 (fetch-dcl-field :split-types all-but-body1)) (split-types2 (fetch-dcl-field :split-types all-but-body2)))
         (or (not (eq (all-nils split-types1) (all-nils split-types2)))
           (not (boolean-listp split-types1))
           (and (member-eq nil split-types1)
             (member-eq t split-types1)))) (msg "the proposed and existing definitions for ~x0 differ on their ~
            :split-types declarations."
          (car def1)))
      ((not chk-measure-p) nil)
      ((null justification) nil)
      (t (non-identical-defp-chk-measures (car def1)
          (fetch-dcl-field :measure all-but-body1)
          (fetch-dcl-field :measure all-but-body2)
          justification)))))

(defun identical-defp
  (def1 def2 chk-measure-p wrld)
  (not (non-identical-defp def1 def2 chk-measure-p wrld)))

(defun redundant-or-reclassifying-defunp
  (defun-mode symbol-class
    ld-skip-proofsp
    chk-measure-p
    def
    wrld)
  (cond ((function-symbolp (car def) wrld) (let* ((wrld1 (decode-logical-name (car def) wrld)) (name (car def))
          (val (scan-to-cltl-command (cdr wrld1)))
          (chk-measure-p (and chk-measure-p
              (not ld-skip-proofsp)
              (eq (cadr val) :logic)
              (eq defun-mode :logic))))
        (cond ((null val) nil)
          ((and (consp val)
             (eq (car val) 'defuns)
             (keywordp (cadr val))) (cond ((non-identical-defp def
                 (assoc-eq name (cdddr val))
                 chk-measure-p
                 wrld))
              ((eq (cadr val) defun-mode) (cond ((and (eq symbol-class :common-lisp-compliant)
                     (eq (symbol-class name wrld) :ideal)) 'verify-guards)
                  (t 'redundant)))
              ((and (eq (cadr val) :program) (eq defun-mode :logic)) 'reclassifying)
              (t 'redundant)))
          ((and (null (cadr val))
             (fetch-dcl-field :non-executable (butlast (cddr def) 1))) (cond ((let* ((event-tuple (cddr (car wrld1))) (event (access-event-tuple-form event-tuple)))
                 (non-identical-defp def
                   (case (car event)
                     (mutual-recursion (assoc-eq name (strip-cdrs (cdr event))))
                     (defuns (assoc-eq name (cdr event)))
                     (otherwise (cdr event)))
                   chk-measure-p
                   wrld)))
              ((and (eq (symbol-class name wrld) :program)
                 (eq defun-mode :logic)) 'reclassifying)
              (t 'redundant)))
          (t nil))))
    (t nil)))

(defun redundant-or-reclassifying-defunsp1
  (defun-mode symbol-class
    ld-skip-proofsp
    chk-measure-p
    def-lst
    wrld
    ans)
  (cond ((null def-lst) ans)
    (t (let ((x (redundant-or-reclassifying-defunp defun-mode
             symbol-class
             ld-skip-proofsp
             chk-measure-p
             (car def-lst)
             wrld)))
        (cond ((consp x) x)
          ((eq ans x) (redundant-or-reclassifying-defunsp1 defun-mode
              symbol-class
              ld-skip-proofsp
              chk-measure-p
              (cdr def-lst)
              wrld
              ans))
          (t nil))))))

(defun recover-defs-lst
  (fn wrld)
  (let ((err-str "For technical reasons, we do not attempt to recover the ~
                  definition of a ~s0 function such as ~x1.  It is surprising ~
                  actually that you are seeing this message; please contact ~
                  the ACL2 implementors unless you have called ~x2 yourself.") (ctx 'recover-defs-lst))
    (cond ((getpropc fn 'non-executablep nil wrld) (er hard ctx err-str "non-executable" fn 'recover-defs-lst))
      (t (let ((val (scan-to-cltl-command (cdr (lookup-world-index 'event
                   (getpropc fn
                     'absolute-event-number
                     '(:error "See ~
                                                           RECOVER-DEFS-LST.")
                     wrld)
                   wrld)))))
          (cond ((and (consp val) (eq (car val) 'defuns)) (cond ((cadr val) (cdddr val))
                (t (er hard
                    ctx
                    err-str
                    "non-executable or :LOGIC mode"
                    fn
                    'recover-defs-lst))))
            (t (er hard
                ctx
                "We failed to find the expected CLTL-COMMAND for the ~
                      introduction of ~x0."
                fn))))))))

(defun get-clique
  (fn wrld)
  (cond ((programp fn wrld) (let ((defs (recover-defs-lst fn wrld)))
        (strip-cars defs)))
    (t (let ((recp (getpropc fn 'recursivep nil wrld)))
        (cond ((null recp) (list fn)) (t recp))))))

(defun redundant-or-reclassifying-defunsp0
  (defun-mode symbol-class
    ld-skip-proofsp
    chk-measure-p
    def-lst
    wrld)
  (cond ((null def-lst) 'redundant)
    (t (let ((ans (redundant-or-reclassifying-defunp defun-mode
             symbol-class
             ld-skip-proofsp
             chk-measure-p
             (car def-lst)
             wrld)))
        (cond ((consp ans) ans)
          (t (let ((ans (redundant-or-reclassifying-defunsp1 defun-mode
                   symbol-class
                   ld-skip-proofsp
                   chk-measure-p
                   (cdr def-lst)
                   wrld
                   ans)))
              (cond ((eq ans 'redundant) (cond ((set-equalp-eq (strip-cars def-lst)
                       (get-clique (caar def-lst) wrld)) ans)
                    (t (msg "for definitions to be redundant, if one ~
                                    is defined with mutual-recursion then the ~
                                    old and new definition must occur in ~
                                    mutual-recursion events that define the ~
                                    same set of function symbols.  See :DOC ~
                                    redundant-events.~|~%"))))
                ((and (eq ans 'reclassifying)
                   (not (set-equalp-eq (strip-cars def-lst)
                       (get-clique (caar def-lst) wrld)))) (msg "for reclassifying :program mode definitions ~
                                to :logic mode, an entire mutual-recursion ~
                                clique must be reclassified.  In this case, ~
                                the mutual-recursion that defined ~x0 also ~
                                defined the following, not included in the ~
                                present event: ~&1.~|~%"
                    (caar def-lst)
                    (set-difference-eq (get-clique (caar def-lst) wrld)
                      (strip-cars def-lst))))
                (t ans)))))))))

(defun strip-last-elements
  (lst)
  (declare (xargs :guard (true-list-listp lst)))
  (cond ((endp lst) nil)
    (t (cons (car (last (car lst)))
        (strip-last-elements (cdr lst))))))

(defun redundant-or-reclassifying-defunsp
  (defun-mode symbol-class
    ld-skip-proofsp
    def-lst
    ctx
    wrld
    ld-redefinition-action
    fives
    non-executablep
    stobjs-in-lst
    default-state-vars)
  (let ((ans (redundant-or-reclassifying-defunsp0 defun-mode
         symbol-class
         ld-skip-proofsp
         t
         def-lst
         wrld)))
    (cond ((and ld-redefinition-action
         (member-eq ans '(redundant reclassifying verify-guards))) (let ((names (strip-cars fives)) (arglists (strip-cadrs fives))
            (bodies (get-bodies fives)))
          (mv-let (erp lst bindings)
            (translate-bodies1 (eq non-executablep t)
              names
              bodies
              (pairlis$ names names)
              arglists
              stobjs-in-lst
              ctx
              wrld
              default-state-vars)
            (declare (ignore bindings))
            (cond (erp ans)
              ((eq (symbol-class (car names) wrld) :program) (let ((old-defs (recover-defs-lst (car names) wrld)))
                  (and (equal names (strip-cars old-defs))
                    (mv-let (erp old-lst bindings)
                      (translate-bodies1 nil
                        names
                        (strip-last-elements old-defs)
                        (pairlis$ names names)
                        arglists
                        stobjs-in-lst
                        ctx
                        wrld
                        default-state-vars)
                      (declare (ignore bindings))
                      (cond ((and (null erp) (equal lst old-lst)) ans) (t nil))))))
              ((equal lst (get-unnormalized-bodies names wrld)) ans)
              (t nil)))))
      (t ans))))

(defun collect-when-cadr-eq
  (sym lst)
  (cond ((null lst) nil)
    ((eq sym (cadr (car lst))) (cons (car lst) (collect-when-cadr-eq sym (cdr lst))))
    (t (collect-when-cadr-eq sym (cdr lst)))))

(defun all-programp
  (names wrld)
  (cond ((null names) t)
    (t (and (programp (car names) wrld)
        (all-programp (cdr names) wrld)))))

(defun formal-position
  (var formals i)
  (cond ((null formals) i)
    ((eq var (car formals)) i)
    (t (formal-position var (cdr formals) (1+ i)))))

(defun make-posns
  (formals vars)
  (cond ((null vars) nil)
    (t (cons (formal-position (car vars) formals 0)
        (make-posns formals (cdr vars))))))

(defun relevant-posns-clique1
  (fns arglists bodies all-fns ans)
  (cond ((null fns) ans)
    (t (relevant-posns-clique1 (cdr fns)
        (cdr arglists)
        (cdr bodies)
        all-fns
        (let* ((posns (cdr (assoc-equal (car fns) ans))) (new-posns (cond ((flambdap (car fns)) (relevant-posns-term (car fns)
                    (lambda-formals (car fns))
                    (lambda-body (car fns))
                    all-fns
                    ans
                    posns))
                (t (relevant-posns-term (car fns)
                    (car arglists)
                    (car bodies)
                    all-fns
                    ans
                    posns)))))
          (cond ((equal posns new-posns) ans)
            (t (put-assoc-equal (car fns) new-posns ans))))))))

(defun relevant-posns-clique-recur
  (fns arglists bodies clique-alist)
  (let ((clique-alist1 (relevant-posns-clique1 fns
         arglists
         bodies
         fns
         clique-alist)))
    (cond ((equal clique-alist1 clique-alist) clique-alist)
      (t (relevant-posns-clique-recur fns
          arglists
          bodies
          clique-alist1)))))

(defun relevant-posns-clique-init
  (fns arglists
    guards
    split-types-terms
    measures
    ignores
    ignorables
    ans)
  (cond ((null fns) ans)
    (t (relevant-posns-clique-init (cdr fns)
        (cdr arglists)
        (cdr guards)
        (cdr split-types-terms)
        (cdr measures)
        (cdr ignores)
        (cdr ignorables)
        (acons (car fns)
          (make-posns (car arglists)
            (all-vars1 (car guards)
              (all-vars1 (car split-types-terms)
                (all-vars1 (car measures)
                  (union-eq (car ignorables) (car ignores))))))
          ans)))))

(defun relevant-posns-merge
  (alist acc)
  (cond ((endp alist) acc)
    ((endp (cdr alist)) (cons (car alist) acc))
    ((equal (car (car alist)) (car (cadr alist))) (relevant-posns-merge (acons (caar alist)
          (union$ (cdr (car alist)) (cdr (cadr alist)))
          (cddr alist))
        acc))
    (t (relevant-posns-merge (cdr alist) (cons (car alist) acc)))))

(defun relevant-posns-lambdas-top
  (bodies)
  (let ((alist (merge-sort-lexorder (relevant-posns-lambdas-lst bodies nil))))
    (relevant-posns-merge alist nil)))

(defun relevant-posns-clique
  (fns arglists
    guards
    split-types-terms
    measures
    ignores
    ignorables
    bodies)
  (let* ((clique-alist1 (relevant-posns-clique-init fns
         arglists
         guards
         split-types-terms
         measures
         ignores
         ignorables
         nil)) (clique-alist2 (relevant-posns-lambdas-top bodies)))
    (relevant-posns-clique-recur (append fns (strip-cars clique-alist2))
      arglists
      bodies
      (revappend clique-alist1 clique-alist2))))

(defun irrelevant-non-lambda-slots-clique2
  (fn formals i posns acc)
  (cond ((endp formals) acc)
    (t (irrelevant-non-lambda-slots-clique2 fn
        (cdr formals)
        (1+ i)
        posns
        (cond ((member i posns) acc)
          (t (cons (list* fn i (car formals)) acc)))))))

(defun irrelevant-non-lambda-slots-clique1
  (fns arglists clique-alist acc)
  (cond ((endp fns) (assert$ (or (null clique-alist) (flambdap (caar clique-alist)))
        acc))
    (t (assert$ (eq (car fns) (caar clique-alist))
        (irrelevant-non-lambda-slots-clique1 (cdr fns)
          (cdr arglists)
          (cdr clique-alist)
          (irrelevant-non-lambda-slots-clique2 (car fns)
            (car arglists)
            0
            (cdar clique-alist)
            acc))))))

(defun irrelevant-non-lambda-slots-clique
  (fns arglists
    guards
    split-types-terms
    measures
    ignores
    ignorables
    bodies)
  (let ((clique-alist (relevant-posns-clique fns
         arglists
         guards
         split-types-terms
         measures
         ignores
         ignorables
         bodies)))
    (irrelevant-non-lambda-slots-clique1 fns
      arglists
      clique-alist
      nil)))

(defun tilde-*-irrelevant-formals-msg1
  (slots)
  (cond ((null slots) nil)
    (t (cons (cons "~n0 formal of ~x1, ~x2,"
          (list (cons #\0 (list (1+ (cadar slots))))
            (cons #\1 (caar slots))
            (cons #\2 (cddar slots))))
        (tilde-*-irrelevant-formals-msg1 (cdr slots))))))

(defun tilde-*-irrelevant-formals-msg
  (slots)
  (list ""
    "~@*"
    "~@* and the "
    "~@* the "
    (tilde-*-irrelevant-formals-msg1 slots)))

(defun missing-irrelevant-slots1
  (irrelevant-slots irrelevants-alist acc)
  (cond ((endp irrelevant-slots) acc)
    (t (missing-irrelevant-slots1 (cdr irrelevant-slots)
        irrelevants-alist
        (if (member-eq (cddr (car irrelevant-slots))
            (cdr (assoc-eq (car (car irrelevant-slots)) irrelevants-alist)))
          acc
          (cons (car irrelevant-slots) acc))))))

(defun missing-irrelevant-slots
  (irrelevant-slots irrelevants-alist)
  (cond ((null irrelevant-slots) nil)
    ((null irrelevants-alist) irrelevant-slots)
    (t (missing-irrelevant-slots1 irrelevant-slots
        irrelevants-alist
        nil))))

(defun find-slot
  (fn var irrelevant-slots)
  (cond ((endp irrelevant-slots) nil)
    ((let ((slot (car irrelevant-slots)))
       (or (and (eq fn (car slot)) (eq var (cddr slot))))))
    (t (find-slot fn var (cdr irrelevant-slots)))))

(defun bogus-irrelevants-alist2
  (irrelevant-slots fn vars)
  (cond ((endp vars) nil)
    ((find-slot fn (car vars) irrelevant-slots) (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars)))
    (t (cons (car vars)
        (bogus-irrelevants-alist2 irrelevant-slots fn (cdr vars))))))

(defun bogus-irrelevants-alist1
  (irrelevant-slots irrelevants-alist acc)
  (cond ((endp irrelevants-alist) acc)
    (t (bogus-irrelevants-alist1 irrelevant-slots
        (cdr irrelevants-alist)
        (let ((bogus-vars (bogus-irrelevants-alist2 irrelevant-slots
               (caar irrelevants-alist)
               (cdar irrelevants-alist))))
          (if bogus-vars
            (acons (caar irrelevants-alist) bogus-vars acc)
            acc))))))

(defun bogus-irrelevants-alist
  (irrelevant-slots irrelevants-alist)
  (cond ((null irrelevants-alist) irrelevant-slots)
    (t (bogus-irrelevants-alist1 irrelevant-slots
        irrelevants-alist
        nil))))

(defun tilde-*-bogus-irrelevants-alist-msg1
  (alist)
  (cond ((endp alist) nil)
    (t (cons (cons "formal~#0~[~/s~] ~&0 of ~x1"
          (list (cons #\0 (cdar alist)) (cons #\1 (caar alist))))
        (tilde-*-bogus-irrelevants-alist-msg1 (cdr alist))))))

(defun tilde-*-bogus-irrelevants-alist-msg
  (alist)
  (list ""
    "~@*"
    "~@*; and the "
    "~@*; the "
    (tilde-*-bogus-irrelevants-alist-msg1 alist)))

(defun chk-irrelevant-formals-msg
  (fns arglists
    guards
    split-types-terms
    measures
    ignores
    ignorables
    irrelevants-alist
    bodies
    rawp)
  (let ((irrelevant-slots (irrelevant-non-lambda-slots-clique fns
         arglists
         guards
         split-types-terms
         measures
         ignores
         ignorables
         bodies)))
    (cond ((and (null irrelevant-slots) (null irrelevants-alist)) nil)
      (t (let ((bogus-irrelevants-alist (bogus-irrelevants-alist irrelevant-slots irrelevants-alist)) (missing-irrelevant-slots (missing-irrelevant-slots irrelevant-slots
                irrelevants-alist)))
          (cond ((and (null bogus-irrelevants-alist)
               (null missing-irrelevant-slots)) nil)
            (rawp (list bogus-irrelevants-alist missing-irrelevant-slots))
            (t (msg "~@0~@1See :DOC irrelevant-formals."
                (if missing-irrelevant-slots
                  (msg "The ~*0 ~#1~[is~/are~] irrelevant but not declared ~
                         to be irrelevant.  "
                    (tilde-*-irrelevant-formals-msg missing-irrelevant-slots)
                    (if (cdr missing-irrelevant-slots)
                      1
                      0))
                  "")
                (if bogus-irrelevants-alist
                  (msg "The ~*0 ~#1~[is~/are~] falsely declared irrelevant.  "
                    (tilde-*-bogus-irrelevants-alist-msg bogus-irrelevants-alist)
                    (if (or (cdr bogus-irrelevants-alist)
                        (cddr (car bogus-irrelevants-alist)))
                      1
                      0))
                  "")))))))))

(defun chk-irrelevant-formals
  (fns arglists
    guards
    split-types-terms
    measures
    ignores
    ignorables
    irrelevants-alist
    bodies
    ctx
    state)
  (let ((irrelevant-formals-ok (cdr (assoc-eq :irrelevant-formals-ok (table-alist 'acl2-defaults-table (w state))))))
    (cond ((or (eq irrelevant-formals-ok t)
         (and (eq irrelevant-formals-ok :warn)
           (warning-disabled-p "Irrelevant-formals"))) (value nil))
      (t (let ((msg (chk-irrelevant-formals-msg fns
               arglists
               guards
               split-types-terms
               measures
               ignores
               ignorables
               irrelevants-alist
               bodies
               nil)))
          (cond ((null msg) (value nil))
            ((eq irrelevant-formals-ok :warn) (pprogn (warning$ ctx ("Irrelevant-formals") "~@0" msg)
                (value nil)))
            (t (er soft ctx "~@0" msg))))))))

(defun chk-logic-subfunctions
  (names0 names terms wrld str ctx state)
  (cond ((null names) (value nil))
    (t (let ((bad (collect-programs (set-difference-eq (all-fnnames (car terms)) names0)
             wrld)))
        (cond (bad (er soft
              ctx
              "The ~@0 for ~x1 calls the :program function~#2~[ ~&2~/s ~&2~].  We ~
          require that :logic definitions be defined entirely in terms of ~
          :logically defined functions.  See :DOC defun-mode."
              str
              (car names)
              (reverse bad)))
          (t (chk-logic-subfunctions names0
              (cdr names)
              (cdr terms)
              wrld
              str
              ctx
              state)))))))

(defun collect-unbadged
  (fns wrld)
  (cond ((endp fns) nil)
    ((executable-badge (car fns) wrld) (collect-unbadged (cdr fns) wrld))
    (t (cons (car fns) (collect-unbadged (cdr fns) wrld)))))

(defun chk-badged-quoted-subfunctions
  (names0 names terms wrld str ctx state)
  (cond ((null names) (value nil))
    (t (let ((bad (collect-unbadged (set-difference-eq (all-fnnames! nil :inside nil (car terms) nil wrld nil)
               names0)
             wrld)))
        (cond (bad (er soft
              ctx
              "The ~@0 for ~x1 uses the unbadged symbol~#2~[ ~&2~/s ~&2~] in one ~
          or more :FN or :EXPR slots.  We require that all such symbols be ~
          badged function symbols.  See :DOC defun and defbadge."
              str
              (car names)
              (reverse bad)))
          (t (chk-badged-quoted-subfunctions names0
              (cdr names)
              (cdr terms)
              wrld
              str
              ctx
              state)))))))

(defun translate-measures
  (terms logic-modep ctx wrld state)
  (cond ((null terms) (value nil))
    (t (er-let* ((term (cond ((and (consp (car terms)) (eq (car (car terms)) :?)) (cond ((arglistp (cdr (car terms))) (value (car terms)))
                 (t (er soft
                     ctx
                     "A measure whose car is :? must be of the ~
                                   form (:? v1 ... vk), where (v1 ... vk) is ~
                                   a list of distinct variables.  The measure ~
                                   ~x0 is thus illegal."
                     (car terms)))))
             (t (translate (car terms) t logic-modep t ctx wrld state)))) (rst (translate-measures (cdr terms) logic-modep ctx wrld state)))
        (value (cons term rst))))))

(defun redundant-predefined-error-msg
  (name wrld)
  (let ((pkg-name (and (symbolp name) (symbol-package-name name))))
    (msg "ACL2 is processing a redundant definition of the name ~s0 (package ~
          ~s1), which is ~#2~[already defined using special raw Lisp ~
          code~/predefined in the ~x3 package~].  We disallow non-LOCAL ~
          redundant definitions in such cases; for explanation, see :DOC ~
          redundant-events.  Consider wrapping this definition inside a call ~
          of LOCAL.~@4"
      (symbol-name name)
      (symbol-package-name name)
      (if (equal pkg-name *main-lisp-package-name*)
        1
        0)
      *main-lisp-package-name*
      (if (not (symbolp name))
        ""
        (let* ((wrld (decode-logical-name name wrld)) (path (global-val 'include-book-path wrld))
            (book-name (car path)))
          (cond ((null book-name) "")
            (t (msg "  Alternatively, include the book that introduces the ~
                       proposed redundant definition:~|~x0."
                (cond ((sysfile-p book-name) `(include-book ,(REMOVE-LISP-SUFFIX (SYSFILE-FILENAME BOOK-NAME) T) :dir ,(SYSFILE-KEY BOOK-NAME)))
                  (t `(include-book ,(REMOVE-LISP-SUFFIX BOOK-NAME T))))))))))))

(defun chk-acceptable-defuns-redundancy
  (names defun-mode ctx wrld state)
  (let ((localp (f-get-global 'in-local-flg state)))
    (cond ((and (not localp)
         (not (global-val 'boot-strap-flg (w state)))
         (not (f-get-global 'redundant-with-raw-code-okp state))
         (let ((recp (getpropc (car names) 'recursivep nil wrld)) (bad-fns (if (eq (symbol-class (car names) wrld) :program)
                 (f-get-global 'program-fns-with-raw-code state)
                 (f-get-global 'logic-fns-with-raw-code state))))
           (if recp
             (intersectp-eq recp bad-fns)
             (member-eq (car names) bad-fns)))) (er soft
          ctx
          "~@0"
          (redundant-predefined-error-msg (car names) wrld)))
      (t (progn$ (value (cons 'redundant defun-mode)))))))

(defun chk-acceptable-defuns-verify-guards-er
  (names ctx wrld state)
  (let ((include-book-path (global-val 'include-book-path wrld)))
    (mv-let (erp ev-wrld-and-cmd-wrld state)
      (state-global-let* ((inhibit-output-lst (cons 'error (f-get-global 'inhibit-output-lst state))))
        (let ((wrld (w state)))
          (er-let* ((ev-wrld (er-decode-logical-name (car names) wrld :pe state)) (cmd-wrld (superior-command-world ev-wrld wrld :pe state)))
            (value (cons ev-wrld cmd-wrld)))))
      (mv-let (erp1 val1 state)
        (er soft
          ctx
          "The definition of ~x0~#1~[~/ (along with the others in its ~
                  mutual-recursion clique)~]~@2 demands guard verification, ~
                  but there is already a corresponding existing definition ~
                  without its guard verified.  ~@3Use verify-guards instead; ~
                  see :DOC verify-guards. ~#4~[Here is the existing ~
                  definition of ~x0:~/The existing definition of ~x0 appears ~
                  to precede this one in the same top-level command.~]"
          (car names)
          names
          (cond (include-book-path (cons " in the book ~xa"
                (list (cons #\a
                    (book-name-to-filename (car include-book-path) wrld ctx)))))
            (t ""))
          (cond ((cddr include-book-path) (cons "Note: The above book is included under the ~
                          following sequence of included books from outside ~
                          to inside, i.e., top-level included book ~
                          first:~|~&b.~|"
                (list (cons #\b
                    (book-name-lst-to-filename-lst (reverse (cdr include-book-path))
                      (project-dir-alist wrld)
                      ctx)))))
            ((cdr include-book-path) (cons "Note: The above book is included inside the book ~
                          ~xb.  "
                (list (cons #\b
                    (book-name-to-filename (cadr include-book-path) wrld ctx)))))
            (t ""))
          (if erp
            1
            0))
        (pprogn (if erp
            state
            (pe-fn1 wrld
              (standard-co state)
              (car ev-wrld-and-cmd-wrld)
              (cdr ev-wrld-and-cmd-wrld)
              state))
          (mv erp1 val1 state))))))

(defun chk-non-executablep
  (defun-mode non-executablep ctx state)
  (cond ((eq non-executablep nil) (value nil))
    ((eq defun-mode :logic) (cond ((eq non-executablep t) (value nil))
        (t (er soft
            ctx
            "The :NON-EXECUTABLE flag for :LOGIC mode functions ~
                       must be ~x0 or ~x1, but ~x2 is neither."
            t
            nil
            non-executablep))))
    (t (cond ((eq non-executablep :program) (value nil))
        (t (er soft
            ctx
            "The :NON-EXECUTABLE flag for :PROGRAM mode functions ~
                       must be ~x0 or ~x1, but ~x2 is neither."
            :program nil
            non-executablep))))))

(defun chk-acceptable-defuns0
  (fives ctx wrld state)
  (er-let* ((defun-mode (get-unambiguous-xargs-flg :mode fives
         (default-defun-mode wrld)
         ctx
         state)) (stobjs-in-lst (get-stobjs-in-lst fives defun-mode ctx wrld state))
      (non-executablep (get-unambiguous-xargs-flg :non-executable fives
          nil
          ctx
          state))
      (verify-guards (get-unambiguous-xargs-flg :verify-guards fives
          '(unspecified)
          ctx
          state)))
    (er-progn (chk-defun-mode defun-mode ctx state)
      (chk-non-executablep defun-mode non-executablep ctx state)
      (cond ((consp verify-guards) (value nil))
        ((eq defun-mode :program) (if (eq verify-guards nil)
            (value nil)
            (er soft
              ctx
              "When the :MODE is :program, the only legal :VERIFY-GUARDS ~
                  setting is NIL.  ~x0 is illegal."
              verify-guards)))
        ((or (eq verify-guards nil) (eq verify-guards t)) (value nil))
        (t (er soft
            ctx
            "The legal :VERIFY-GUARD settings are NIL and T.  ~x0 is ~
                  illegal."
            verify-guards)))
      (let* ((symbol-class (cond ((eq defun-mode :program) :program)
             ((consp verify-guards) (cond ((= (default-verify-guards-eagerness wrld) 0) :ideal)
                 ((= (default-verify-guards-eagerness wrld) 1) (if (get-guardsp fives wrld)
                     :common-lisp-compliant :ideal))
                 (t :common-lisp-compliant)))
             (verify-guards :common-lisp-compliant)
             ((= (default-verify-guards-eagerness wrld) 3) :common-lisp-compliant)
             (t :ideal))))
        (value (list* stobjs-in-lst
            defun-mode
            non-executablep
            symbol-class))))))

(defun get-boolean-unambiguous-xargs-flg-lst
  (key lst default ctx state)
  (er-let* ((lst (get-unambiguous-xargs-flg-lst key lst default ctx state)))
    (cond ((boolean-listp lst) (value lst))
      (t (er soft
          ctx
          "The value~#0~[ ~&0 is~/s ~&0 are~] illegal for XARGS key ~x1,
                  as ~x2 and ~x3 are the only legal values for this key."
          lst
          key
          t
          nil)))))

(defun get-irrelevants-alist
  (fives)
  (cond ((null fives) nil)
    (t (acons (caar fives)
        (irrelevant-vars (fourth (car fives)))
        (get-irrelevants-alist (cdr fives))))))

(defun raw-lambda$s-to-lambdas
  (lst)
  (cond ((endp lst) nil)
    (t (cons (cons (unquote (fargn (lambda-object-body (car lst)) 2))
          (car lst))
        (raw-lambda$s-to-lambdas (cdr lst))))))

(defun chk-acceptable-lambda$-translations1
  (new-pairs ctx wrld state)
  (cond ((null new-pairs) (value nil))
    (t (let* ((key (car (car new-pairs))) (val (cdr (car new-pairs))))
        (mv-let (erp tkey bindings)
          (translate11-lambda-object key
            t
            nil
            t
            nil
            key
            ctx
            wrld
            (default-state-vars t)
            nil)
          (declare (ignore bindings))
          (cond (erp (er soft
                ctx
                "The attempt to translate a lambda$ to be stored as a key ~
                     on lambda$-alist has caused an error, despite the fact ~
                     that this very same lambda$ was successfully translated ~
                     a moment ago!  The error caused is:~%~@0~%~%The ~
                     offending lambda$ is ~x1.  This is an implementation ~
                     error and you should contact the ACL2 developers."
                tkey
                key))
            ((equal (unquote tkey) val) (chk-acceptable-lambda$-translations1 (cdr new-pairs)
                ctx
                wrld
                state))
            (t (er soft
                ctx
                "Imperfect counterfeit translated lambda$, ~x0.  Unless you ~
                   knowingly tried to construct a translated lambda$ (instead ~
                   of using lambda$ and letting ACL2 generate the ~
                   translation) this is an implementation error.  Please ~
                   report such errors to the ACL2 developers.~%~%But if you ~
                   tried to counterfeit a lambda$ we should point out that we ~
                   don't understand why you would do such a thing!  Your ~
                   counterfeit translated lambda$ won't enjoy the same ~
                   runtime support as our translated lambda$ even if you did ~
                   it perfectly.  The lambda object you created would be ~
                   interpreted by *1*apply even in a guard-verified raw Lisp ~
                   function while our lambda$ translation would produce ~
                   compiled code.~%~%Nevertheless, here's what's wrong with ~
                   your counterfeit version:  the lambda$ expression~%~Y01 ~
                   actually translates to~%~Y21 but your counterfeit claimed it ~
                   translates to~%~Y31."
                key
                nil
                (unquote tkey)
                val))))))))

(defun chk-acceptable-lambda$-translations2
  (new-pairs lambda$-alist ctx state)
  (cond ((null new-pairs) (value nil))
    (t (let* ((key (car (car new-pairs))) (val (cdr (car new-pairs)))
          (temp1 (assoc-equal key lambda$-alist)))
        (cond ((and temp1 (not (equal val (cdr temp1)))) (er soft
              ctx
              "A pair about to be added to lambda$-alist has the same key ~
               associated with a different value on lambda$-alist already.  ~
               This is an implementation error.  Please report it to the ACL2 ~
               developers.  The duplicate key is ~x0.  On lambda$-alist that ~
               key is mapped to the value ~x1.  But we were about to map it ~
               to the value ~x2.  This shouldn't happen because both values ~
               are allegedly the translation of the key!"
              key
              (cdr temp1)
              val))
          (t (let ((temp2 (assoc-equal key (cdr new-pairs))))
              (cond ((and temp2 (not (equal val (cdr temp2)))) (er soft
                    ctx
                    "Two pairs about to be added to lambda$-alist have the same key ~
               but different values.  This is an implementation error.  ~
               Please report it to the ACL2 developers.  The key is ~x0 and ~
               the two values are ~x1 and ~x2.  This shouldn't happen because ~
               both values are allegedly the translation of the key!"
                    key
                    (cdr temp2)
                    val))
                (t (chk-acceptable-lambda$-translations2 (cdr new-pairs)
                    lambda$-alist
                    ctx
                    state))))))))))

(defun chk-acceptable-lambda$-translations
  (symbol-class guards bodies ctx wrld state)
  (cond ((and (not (eq symbol-class :program))
       (not (global-val 'boot-strap-flg wrld))) (let ((new-pairs (raw-lambda$s-to-lambdas (collect-certain-lambda-objects-lst :lambda$ (append guards bodies)
               wrld
               nil))))
        (er-progn (chk-acceptable-lambda$-translations1 new-pairs
            ctx
            wrld
            state)
          (chk-acceptable-lambda$-translations2 new-pairs
            (global-val 'lambda$-alist wrld)
            ctx
            state)
          (value new-pairs))))
    (t (value nil))))

(defun loop$-alist-term
  (loop$-form loop$-alist)
  (let ((pair (assoc-equal loop$-form loop$-alist)))
    (and pair (access loop$-alist-entry (cdr pair) :term))))

(defun convert-to-dfs-fn
  (form stobjs-out index bound-vars-rev out-exprs-rev)
  (cond ((endp stobjs-out) `(mv-let ,(REVERSE BOUND-VARS-REV)
        ,FORM
        (mv ,@(REVERSE OUT-EXPRS-REV))))
    ((eq (car stobjs-out) :df) (let ((var (packn (list 'x index))))
        (convert-to-dfs-fn form
          (cdr stobjs-out)
          (1+ index)
          (cons var bound-vars-rev)
          (cons `(to-df ,VAR) out-exprs-rev))))
    (t (let ((var (packn (list 'x index))))
        (convert-to-dfs-fn form
          (cdr stobjs-out)
          (1+ index)
          (cons var bound-vars-rev)
          (cons var out-exprs-rev))))))

(defun convert-to-dfs
  (form stobjs-out)
  (cond ((not (member-eq :df stobjs-out)) form)
    ((null (cdr stobjs-out)) `(to-df ,FORM))
    (t (convert-to-dfs-fn form stobjs-out 0 nil nil))))

(defun authenticate-tagged-lambda$
  (x state)
  (cond ((let ((dcl (lambda-object-dcl x)))
       (and dcl (double-float-types-p dcl))) nil)
    ((lambda$-bodyp (lambda-object-body x)) (cond ((assoc-equal-cdr x (global-val 'lambda$-alist (w state))) t)
        (t (mv-let (erp obj bindings)
            (translate11-lambda-object (unquote (fargn (lambda-object-body x) 2))
              '(nil)
              nil
              nil
              nil
              nil
              'authenticate-tagged-lambda$-expression
              (w state)
              (default-state-vars state)
              t)
            (declare (ignore bindings))
            (cond (erp nil) ((equal (unquote obj) x) t) (t nil))))))
    (t nil)))

(defun make-compileable-guard-and-body-lambdas
  (x state)
  (let ((formals (lambda-object-formals x)) (dcl (lambda-object-dcl x))
      (body (lambda-object-body x))
      (wrld (w state)))
    (cond ((authenticate-tagged-lambda$ x state) (let* ((lambda$-expr (unquote (fargn (lambda-object-body x) 2))) (edcls (edcls-from-lambda-object-dcls-short-cut (cddr lambda$-expr)))
            (guard-lst (get-guards2 edcls '(types guards) nil wrld nil nil nil)))
          (mv `(lambda ,FORMALS
              (declare (ignorable ,@FORMALS))
              ,(COND ((NULL GUARD-LST) 'T) ((NULL (CDR GUARD-LST)) (CAR GUARD-LST))
       (T `(AND ,@GUARD-LST))))
            `(lambda ,@(CDR LAMBDA$-EXPR)))))
      (t (mv `(lambda ,FORMALS
            (declare (ignorable ,@FORMALS)
              ,@(REMOVE-DOUBLE-FLOAT-TYPES (CDR DCL)))
            ,(LOGIC-CODE-TO-RUNNABLE-CODE NIL
                              (REMOVE-GUARD-HOLDERS
                               (OR
                                (CADR
                                 (ASSOC-KEYWORD :GUARD
                                                (CDR
                                                 (ASSOC-EQ 'XARGS (CDR DCL)))))
                                *T*)
                               WRLD)
                              WRLD))
          `(lambda ,FORMALS
            ,@(LET ((D (REMOVE-DOUBLE-FLOAT-TYPES (CDR DCL))))
    (AND D `((DECLARE ,@D))))
            ,(LOGIC-CODE-TO-RUNNABLE-CODE NIL (REMOVE-GUARD-HOLDERS BODY WRLD) WRLD)))))))

(defun convert-tagged-loop$s-to-pairs
  (lst flg wrld)
  (cond ((endp lst) nil)
    (t (cons (cons (unquote (fargn (car lst) 2))
          (make loop$-alist-entry
            :term (logic-code-to-runnable-code nil (fargn (car lst) 3) wrld)
            :flg flg))
        (convert-tagged-loop$s-to-pairs (cdr lst) flg wrld)))))

(defun chk-acceptable-loop$-translations1
  (new-pairs ctx wrld state)
  (cond ((null new-pairs) (value nil))
    (t (let* ((key (car (car new-pairs))) (val (cdr (car new-pairs)))
          (val-term (access loop$-alist-entry val :term)))
        (mv-let (erp tkey bindings)
          (translate11-loop$ key
            t
            nil
            t
            nil
            nil
            key
            ctx
            wrld
            (default-state-vars t))
          (declare (ignore bindings))
          (cond (erp (er soft
                ctx
                "The attempt to translate a loop$ to be stored as a key ~
                     on loop$-alist has caused an error, despite the fact ~
                     that this very same loop$ was successfully translated ~
                     a moment ago!  The error caused is:~%~@0~%~%The ~
                     offending loop$ is ~x1.  This is an implementation ~
                     error and you should contact the ACL2 developers."
                tkey
                key))
            ((and (tagged-loop$p tkey)
               (equal (logic-code-to-runnable-code nil (fargn tkey 3) wrld)
                 val-term)) (chk-acceptable-loop$-translations1 (cdr new-pairs)
                ctx
                wrld
                state))
            (t (er soft
                ctx
                "Imperfect counterfeit translated loop$, ~x0.  Unless you ~
                   knowingly tried to construct a translated loop$ (instead ~
                   of using loop$ and letting ACL2 generate the translation) ~
                   this is an implementation error.  Please report such ~
                   errors to the ACL2 developers.~%~%But if you tried to ~
                   counterfeit a loop$ we should point out that we don't ~
                   understand why you would do such a thing!  Your ~
                   counterfeit translated loop$ won't enjoy the same runtime ~
                   support as our translated loop$ even if you did it ~
                   perfectly.  Had you written a loop$ it would enter raw ~
                   Lisp as a CLTL loop statement and run fast when guard ~
                   verified.  But the counterfeit term will just use the ~
                   logically translated term you claimed was the semantics ~
                   of the loop$.~%~%Nevertheless, here's what's wrong with ~
                   your counterfeit version:  the loop$ expression~%~Y01 ~
                   actually translates to~%~Y21, which when converted to ~
                   runnable raw Lisp is~%~Y31, but your counterfeit claimed the ~
                   runnable raw Lisp of its translation is~%~Y41."
                key
                nil
                tkey
                (logic-code-to-runnable-code nil (fargn tkey 3) wrld)
                val-term))))))))

(defun chk-acceptable-loop$-translations2
  (new-pairs loop$-alist ctx state)
  (cond ((null new-pairs) (value nil))
    (t (let* ((key (car (car new-pairs))) (val (cdr (car new-pairs)))
          (val-term (access loop$-alist-entry val :term))
          (loop$-term (loop$-alist-term key loop$-alist)))
        (cond ((and loop$-term (not (equal val-term loop$-term))) (er soft
              ctx
              "A pair about to be added to loop$-alist has the same key ~
               associated with a different value on loop$-alist already.  ~
               This is an implementation error.  Please report it to the ACL2 ~
               developers.  The duplicate key is ~x0.  On loop$-alist that ~
               key is mapped to the value ~x1.  But we were about to map it ~
               to the value ~x2.  This shouldn't happen because both values ~
               are allegedly the translation of the key!"
              key
              loop$-term
              val-term))
          (t (let ((temp2 (assoc-equal key (cdr new-pairs))))
              (cond ((and temp2 (not (equal val-term (cdr temp2)))) (er soft
                    ctx
                    "Two pairs about to be added to loop$-alist have the same ~
                   key but different values.  This is an implementation ~
                   error.  Please report it to the ACL2 developers.  The key ~
                   is ~x0 and the two values are ~x1 and ~x2.  This shouldn't ~
                   happen because both values are allegedly the translation ~
                   of the key!"
                    key
                    (cdr temp2)
                    val-term))
                (t (chk-acceptable-loop$-translations2 (cdr new-pairs)
                    loop$-alist
                    ctx
                    state))))))))))

(defun chk-acceptable-loop$-translations
  (symbol-class guards bodies ctx wrld state)
  (cond ((and (not (eq symbol-class :program))
       (not (global-val 'boot-strap-flg wrld))) (let* ((certify-book-info (f-get-global 'certify-book-info state)) (new-pairs (convert-tagged-loop$s-to-pairs (collect-certain-tagged-loop$s-lst :top (append guards bodies)
                nil)
              (and certify-book-info
                (let ((path (global-val 'include-book-path wrld)))
                  (if (consp path)
                    (and (null (cdr path))
                      (equal (car path)
                        (access certify-book-info certify-book-info :full-book-name)))
                    (null path))))
              wrld)))
        (er-progn (chk-acceptable-loop$-translations1 new-pairs
            ctx
            wrld
            state)
          (chk-acceptable-loop$-translations2 new-pairs
            (global-val 'loop$-alist wrld)
            ctx
            state)
          (value new-pairs))))
    (t (value nil))))

(defun chk-lambdas-for-loop$-recursion
  (fn body wrld ctx state)
  (er-let* ((fn-seenp (chk-lambdas-for-loop$-recursion1 fn
         nil
         body
         nil
         wrld
         ctx
         state)))
    (cond (fn-seenp (value nil))
      (t (er soft
          ctx
          "It is illegal to use :loop$-recursion t in the defun of ~x0 ~
             because ~x0 is never called in a loop$!  We cause an error ~
             simply because we expect you've made a mistake."
          fn)))))

(defun remove-lambdas
  (term)
  (declare (xargs :guard (pseudo-termp term) :verify-guards nil))
  (mv-let (changedp ans)
    (remove-lambdas1 term)
    (declare (ignore changedp))
    ans))

(defun type-prescription-disjunctp
  (var term)
  (cond ((variablep term) (eq term var))
    ((fquotep term) nil)
    ((flambda-applicationp term) nil)
    (t (or (and (eq (ffn-symb term) 'equal)
          (or (and (eq var (fargn term 1))
              (variablep (fargn term 2))
              (not (eq (fargn term 1) (fargn term 2))))
            (and (eq var (fargn term 2))
              (variablep (fargn term 1))
              (not (eq (fargn term 2) (fargn term 1))))))
        (equal (all-vars term) (list var))))))

(defun type-prescription-conclp
  (var concl)
  (cond ((variablep concl) (type-prescription-disjunctp var concl))
    ((fquotep concl) nil)
    ((flambda-applicationp concl) nil)
    ((eq (ffn-symb concl) 'if) (cond ((equal (fargn concl 1) (fargn concl 2)) (and (type-prescription-disjunctp var (fargn concl 1))
            (type-prescription-conclp var (fargn concl 3))))
        (t (type-prescription-disjunctp var concl))))
    (t (type-prescription-disjunctp var concl))))

(defun subst-nil-into-type-prescription-disjunct
  (var term)
  (cond ((variablep term) term)
    ((fquotep term) term)
    ((flambda-applicationp term) term)
    ((and (eq (ffn-symb term) 'equal)
       (or (and (eq var (fargn term 1))
           (variablep (fargn term 2))
           (not (eq (fargn term 1) (fargn term 2))))
         (and (eq var (fargn term 2))
           (variablep (fargn term 1))
           (not (eq (fargn term 2) (fargn term 1)))))) *nil*)
    (t term)))

(defun subst-nil-into-type-prescription-concl
  (var concl)
  (cond ((variablep concl) (subst-nil-into-type-prescription-disjunct var concl))
    ((fquotep concl) concl)
    ((flambda-applicationp concl) concl)
    ((eq (ffn-symb concl) 'if) (cond ((equal (fargn concl 1) (fargn concl 2)) (let ((temp (subst-nil-into-type-prescription-disjunct var
                 (fargn concl 1))))
            (fcons-term* 'if
              temp
              temp
              (subst-nil-into-type-prescription-concl var (fargn concl 3)))))
        (t (subst-nil-into-type-prescription-disjunct var concl))))
    (t (subst-nil-into-type-prescription-disjunct var concl))))

(defun unprettyify-tp
  (term)
  (case-match term
    (('implies t1 t2) (mv-let (hyps concl)
        (unprettyify-tp t2)
        (mv (append? (flatten-ands-in-lit t1) hyps) concl)))
    ((('lambda vars body) . args) (unprettyify-tp (subcor-var vars args body)))
    (& (mv nil (remove-lambdas term)))))

(defun destructure-type-prescription
  (name typed-term term ens wrld)
  (let ((term (remove-guard-holders term wrld)))
    (mv-let (hyps concl)
      (unprettyify-tp term)
      (cond ((or (variablep typed-term)
           (fquotep typed-term)
           (flambda-applicationp typed-term)) (mv (msg "The :TYPED-TERM, ~x0, provided in the :TYPE-PRESCRIPTION ~
                 rule class for ~x1 is illegal because it is a variable, ~
                 constant, or lambda application.  See :DOC type-prescription."
              typed-term
              name)
            nil
            nil
            nil
            nil
            nil))
        ((dumb-occur-lst typed-term hyps) (mv (msg "The :TYPED-TERM, ~x0, of the proposed :TYPE-PRESCRIPTION ~
                 rule ~x1 occurs in the hypotheses of the rule.  This would ~
                 cause ``infinite backchaining'' if we permitted ~x1 as a ~
                 :TYPE-PRESCRIPTION.  (Don't feel reassured by this check:  ~
                 infinite backchaining may occur anyway since it can be ~
                 caused by the combination of several rules.)"
              typed-term
              name)
            nil
            nil
            nil
            nil
            nil))
        (t (let ((all-vars-typed-term (all-vars typed-term)) (all-vars-concl (all-vars concl)))
            (cond ((not (subsetp-eq all-vars-concl all-vars-typed-term)) (mv (msg "~x0 cannot be used as a :TYPE-PRESCRIPTION rule as ~
                     described by the given rule class because the ~
                     :TYPED-TERM, ~x1, does not contain the ~#2~[variable ~&2 ~
                     which is~/variables ~&2 which are~] mentioned in the ~
                     conclusion.  See :DOC type-prescription."
                    name
                    typed-term
                    (reverse (set-difference-eq all-vars-concl all-vars-typed-term)))
                  nil
                  nil
                  nil
                  nil
                  nil))
              (t (let* ((new-var (genvar (find-pkg-witness typed-term)
                       "TYPED-TERM"
                       nil
                       all-vars-typed-term)) (concl1 (subst-expr new-var typed-term concl)))
                  (cond ((not (type-prescription-conclp new-var concl1)) (mv (msg "~x0 is an illegal :TYPE-PRESCRIPTION lemma of the ~
                           class indicated because its conclusion is not a ~
                           disjunction of type restrictions about the ~
                           :TYPED-TERM ~x1.  See :DOC type-prescription."
                          name
                          typed-term)
                        nil
                        nil
                        nil
                        nil
                        nil))
                    (t (let ((vars (remove1-eq new-var (all-vars concl1))) (basic-term (subst-nil-into-type-prescription-concl new-var concl1)))
                        (mv-let (ts ttree)
                          (type-set-implied-by-term new-var
                            nil
                            basic-term
                            ens
                            wrld
                            nil)
                          (cond ((ts= ts *ts-unknown*) (mv (msg "~x0 is a useless :TYPE-PRESCRIPTION ~
                                       lemma because we can deduce no type ~
                                       restriction about its :TYPED-TERM ~
                                       (below represented by ~x1) from the ~
                                       generalized conclusion, ~p2.  See :DOC ~
                                       type-prescription."
                                  name
                                  new-var
                                  (untranslate concl1 t wrld))
                                nil
                                nil
                                nil
                                nil
                                nil))
                            ((not (assumption-free-ttreep ttree)) (mv (if (tagged-objectsp 'fc-derivation ttree)
                                  (er hard
                                    'destructure-type-prescription
                                    "Somehow an 'fc-derivation, ~x0, has ~
                                       found its way into the ttree returned ~
                                       by type-set-implied-by-term."
                                    (car (tagged-objects 'fc-derivation ttree)))
                                  (msg "~x0 is an illegal :TYPE-PRESCRIPTION ~
                                      lemma because in determining the ~
                                      type-set implied for its :TYPED-TERM, ~
                                      ~x1, by its conclusion the ~
                                      ~#2~[assumption ~&2 was~/assumptions ~
                                      ~&2 were~] and our :TYPE-PRESCRIPTION ~
                                      preprocessor, ~
                                      CHK-ACCEPTABLE-TYPE-PRESCRIPTION-RULE, ~
                                      does not know how to handle this ~
                                      supposedly unusual situation.  It would ~
                                      be very helpful to report this error to ~
                                      the authors."
                                    name
                                    typed-term
                                    (tagged-objects 'assumption ttree)))
                                nil
                                nil
                                nil
                                nil
                                nil))
                            (t (mv nil hyps concl ts vars ttree))))))))))))))))

(defun get-xargs-type-prescription-lst
  (fives ctx state)
  (cond ((endp fives) (value nil))
    (t (er-let* ((rest (get-xargs-type-prescription-lst (cdr fives) ctx state)))
        (let* ((five (car fives)) (lst (fetch-dcl-fields1 '(:type-prescription) (fourth five))))
          (cond ((null lst) (value (cons nil rest)))
            ((cdr lst) (er soft
                ctx
                "The :type-prescription keyword for xargs must occur at most ~
               once in the declare forms for a function."))
            (t (value (cons (car lst) rest)))))))))

(defun chk-type-prescription-lst
  (names arglists type-prescription-lst ens wrld ctx state)
  (cond ((endp names) (value nil))
    ((null (car type-prescription-lst)) (chk-type-prescription-lst (cdr names)
        (cdr arglists)
        (cdr type-prescription-lst)
        ens
        wrld
        ctx
        state))
    (t (er-let* ((term (translate (car type-prescription-lst) t t t ctx wrld state)))
        (mv-let (erp hyps concl basic-ts vars ttree)
          (destructure-type-prescription (car names)
            (cons (car names) (car arglists))
            term
            ens
            wrld)
          (declare (ignore concl ttree))
          (cond (erp (er soft
                ctx
                "Illegal :type-prescription specified in xargs for name ~
                   ~x0.  Here is the error message one would see upon trying ~
                   to submit it as a :type-prescription rule:~|~%~@1"
                (car names)
                erp))
            (hyps (er soft
                ctx
                "Illegal :type-prescription specified in xargs for name ~
                    ~x0: hypotheses are not allowed."
                (car names)))
            (t (let* ((name (car names)) (old-tp (car (getpropc name 'type-prescriptions nil wrld)))
                  (uncertified-str "This warning may occur when including an uncertified book, ~
                   when a :type-prescription declaration depends on ~
                   a type-prescription from a locally included book."))
                (er-progn (cond ((null old-tp) (let ((str "It is illegal to specify a non-nil ~
                           :type-prescription in an xargs declaration for ~
                           ~x0, because ACL2 computed no built-in type ~
                           prescription for ~x0."))
                        (cond ((f-get-global 'including-uncertified-p state) (pprogn (warning$ ctx
                                "Uncertified"
                                "~@0  ~@1"
                                (msg str name)
                                uncertified-str)
                              (value nil)))
                          (t (er soft ctx str name)))))
                    (t (let* ((old-basic-ts (access type-prescription old-tp :basic-ts)) (old-vars (access type-prescription old-tp :vars))
                          (subsetp-vars (subsetp-eq old-vars vars)))
                        (assert$ (null (access type-prescription old-tp :hyps))
                          (cond ((and (ts= old-basic-ts basic-ts)
                               (or (equal vars old-vars)
                                 (and subsetp-vars (subsetp-eq vars old-vars)))) (value nil))
                            ((and (ts-subsetp old-basic-ts basic-ts)
                               (subsetp-eq old-vars vars)) (pprogn (warning$ ctx
                                  "Type-prescription"
                                  "The type-prescription specified by the xargs ~
                                :type-prescription for ~x0 is strictly weaker ~
                                than the computed type of ~x0~@1."
                                  name
                                  (if (or (member-eq 'event (f-get-global 'inhibit-output-lst state))
                                      (ld-skip-proofsp state))
                                    ""
                                    " that is noted above"))
                                (value nil)))
                            (t (let ((msg (msg "The type-prescription specified by the xargs ~
                                 :type-prescription for ~x0 is not implied by ~
                                 the computed type of ~x0~@1.~|OLD:~|  ~
                                 ~x2~|NEW:~|  ~x3~|"
                                     name
                                     (if (or (member-eq 'event (f-get-global 'inhibit-output-lst state))
                                         (ld-skip-proofsp state))
                                       ""
                                       " that is noted above")
                                     (access type-prescription old-tp :corollary)
                                     term)))
                                (cond ((f-get-global 'including-uncertified-p state) (pprogn (warning$ ctx "Uncertified" "~@0~@1" msg uncertified-str)
                                      (value nil)))
                                  (t (er soft ctx "~@0" msg))))))))))
                  (chk-type-prescription-lst (cdr names)
                    (cdr arglists)
                    (cdr type-prescription-lst)
                    ens
                    wrld
                    ctx
                    state))))))))))

(defun global-stobjs-prop
  (names bodies guards wrld)
  (mv-let (reads writes fns-seen)
    (collect-global-stobjs-lst bodies wrld nil nil names)
    (mv-let (reads writes fns-seen)
      (collect-global-stobjs-lst guards
        wrld
        reads
        writes
        fns-seen)
      (declare (ignore fns-seen))
      (cond (writes (cons (set-difference-eq reads writes) writes))
        (reads (cons reads nil))
        (t nil)))))

(defun translate-guards
  (guards arglists stobjs-in-lst ctx wrld state state-vars)
  (cond ((endp guards) (value nil))
    (t (mv-let (erp term bindings)
        (translate11 (car guards)
          nil
          '(nil)
          nil
          (if (eq stobjs-in-lst t)
            t
            (collect-non-*-df (car stobjs-in-lst)))
          (if (eq stobjs-in-lst t)
            nil
            (collect-by-position '(:df)
              (car stobjs-in-lst)
              (car arglists)))
          nil
          (car guards)
          ctx
          wrld
          state-vars)
        (declare (ignore bindings))
        (cond (erp (er-soft ctx "Translate" "~@0" term))
          (t (er-let* ((rst (translate-guards (cdr guards)
                   (cdr arglists)
                   (if (eq stobjs-in-lst t)
                     t
                     (cdr stobjs-in-lst))
                   ctx
                   wrld
                   state
                   state-vars)))
              (value (cons term rst)))))))))

(defun chk-acceptable-defuns1
  (names fives
    stobjs-in-lst
    defun-mode
    symbol-class
    rc
    non-executablep
    ctx
    wrld
    state)
  (let ((docs (get-docs fives)) (big-mutrec (big-mutrec names))
      (arglists (strip-cadrs fives))
      (default-hints (default-hints wrld))
      (assumep (or (eq (ld-skip-proofsp state) 'include-book)
          (eq (ld-skip-proofsp state) 'include-book-with-locals)))
      (reclassifying-all-programp (and (eq rc 'reclassifying) (all-programp names wrld)))
      (state-vars (default-state-vars t)))
    (er-let* ((wrld1 (chk-just-new-names names 'function rc ctx wrld state)) (wrld2 (update-w big-mutrec
            (store-stobjs-ins names
              stobjs-in-lst
              (putprop-x-lst2 names
                'formals
                arglists
                (putprop-x-lst1 names 'symbol-class symbol-class wrld1)))))
        (untranslated-measures (get-measures fives ctx state))
        (measures (translate-measures untranslated-measures
            (not (eq symbol-class :program))
            ctx
            wrld2
            state))
        (ruler-extenders-lst (get-ruler-extenders-lst symbol-class fives ctx wrld2 state))
        (rel (get-unambiguous-xargs-flg :well-founded-relation fives
            (default-well-founded-relation wrld2)
            ctx
            state))
        (do-not-translate-hints (value (or assumep (eq (ld-skip-proofsp state) 'initialize-acl2))))
        (hints (if (or do-not-translate-hints (eq defun-mode :program))
            (value nil)
            (let ((hints (get-hints fives)))
              (if hints
                (translate-hints+ (cons "Measure Lemma for" (car names))
                  hints
                  default-hints
                  ctx
                  wrld2
                  state)
                (value nil)))))
        (guard-hints (if (or do-not-translate-hints (eq defun-mode :program))
            (value nil)
            (value (append (get-guard-hints fives) default-hints))))
        (std-hints (value nil))
        (otf-flg (if do-not-translate-hints
            (value nil)
            (get-unambiguous-xargs-flg :otf-flg fives t ctx state)))
        (guard-debug (get-unambiguous-xargs-flg :guard-debug fives nil ctx state))
        (measure-debug (get-unambiguous-xargs-flg :measure-debug fives
            nil
            ctx
            state))
        (guard-simplify (get-unambiguous-xargs-flg :guard-simplify fives
            t
            ctx
            state))
        (guard-simplify (cond ((member-eq guard-simplify '(t :limited)) (value guard-simplify))
            (t (er soft ctx "~@0" (guard-simplify-msg guard-simplify)))))
        (split-types-lst (get-boolean-unambiguous-xargs-flg-lst :split-types fives
            nil
            ctx
            state))
        (normalizeps (get-boolean-unambiguous-xargs-flg-lst :normalize fives
            t
            ctx
            state))
        (loop$-recursion-lst (get-unambiguous-xargs-flg-lst :loop$-recursion fives
            nil
            ctx
            state))
        (type-prescription-lst (get-xargs-type-prescription-lst fives ctx state)))
      (er-progn (cond ((and (consp (cdr loop$-recursion-lst))
             (not (all-nils loop$-recursion-lst))) (er soft
              ctx
              "We do not support the declaration of non-nil :LOOP$-RECURSION ~
             settings in MUTUAL-RECURSION."))
          ((and (null (cdr loop$-recursion-lst))
             (car loop$-recursion-lst)
             (not (eq (car loop$-recursion-lst) t))) (er soft
              ctx
              "The only legal values for the XARGS key :LOOP$-RECURSION are T ~
             and NIL.  ~x0 is not allowed."
              (car loop$-recursion-lst)))
          ((and (car loop$-recursion-lst)
             (global-val 'boot-strap-flg wrld)) (er soft
              ctx
              "Implementors are not allowed to use :LOOP$-RECURSION in system ~
             code!"))
          (t (value nil)))
        (er-let* ((wrld2a (if (car loop$-recursion-lst)
               (let* ((badge-table (table-alist 'badge-table wrld2)) (userfn-structure (cdr (assoc-eq :badge-userfn-structure badge-table)))
                   (fn (car names))
                   (badge (make apply$-badge
                       :arity (length (car arglists))
                       :out-arity 1
                       :ilks t)))
                 (update-w t
                   (putprop fn
                     'stobjs-out
                     '(nil)
                     (putprop 'badge-table
                       'table-alist
                       (put-assoc-eq :badge-userfn-structure (put-badge-userfn-structure-tuple-in-alist (make-badge-userfn-structure-tuple fn nil badge)
                           userfn-structure
                           ctx)
                         badge-table)
                       wrld2))))
               (value wrld2))))
          (er-progn (cond ((not (and (symbolp rel)
                   (assoc-eq rel
                     (global-val 'well-founded-relation-alist wrld2a)))) (er soft
                  ctx
                  "The :WELL-FOUNDED-RELATION specified by XARGS must be a ~
                symbol which has previously been shown to be a well-founded ~
                relation.  ~x0 has not been. See :DOC well-founded-relation."
                  rel))
              (t (value nil)))
            (let ((mp (cadr (assoc-eq rel
                     (global-val 'well-founded-relation-alist wrld2a)))))
              (er-let* ((bodies-and-bindings (translate-bodies non-executablep
                     names
                     arglists
                     (get-bodies fives)
                     (if (car loop$-recursion-lst)
                       (list (cons (car names) '(nil)))
                       (pairlis$ names names))
                     stobjs-in-lst
                     reclassifying-all-programp
                     ctx
                     wrld2a
                     state)))
                (let* ((bodies (car bodies-and-bindings)) (bindings (super-defun-wart-bindings (cdr bodies-and-bindings))))
                  (er-progn (if assumep
                      (value nil)
                      (er-progn (chk-stobjs-out-bound names bindings ctx state)))
                    (if (car loop$-recursion-lst)
                      (chk-lambdas-for-loop$-recursion (car names)
                        (car bodies)
                        wrld2a
                        ctx
                        state)
                      (value nil))
                    (let* ((wrld30 (store-super-defun-warts-stobjs-in names wrld2a)) (wrld31 (store-stobjs-out names bindings wrld30))
                        (wrld3 wrld31)
                        (wrld4 (if (store-cert-data t bodies wrld state)
                            (update-translate-cert-data (car names)
                              wrld
                              wrld3
                              :type :translate-bodies :inputs names
                              :value bodies-and-bindings
                              :fns (all-fnnames-lst bodies)
                              :vars (state-globals-set-by-lst bodies nil))
                            wrld3))
                        (guards0 (get-guards fives split-types-lst nil wrld2a)))
                      (er-let* ((guards (translate-guards guards0
                             arglists
                             stobjs-in-lst
                             ctx
                             wrld3
                             state
                             state-vars)) (split-types-terms (translate-guards (get-guards fives split-types-lst t wrld2a)
                              arglists
                              stobjs-in-lst
                              ctx
                              wrld3
                              state
                              state-vars)))
                        (er-progn (if (eq defun-mode :logic)
                            (er-progn (chk-logic-subfunctions names
                                names
                                guards
                                wrld3
                                "guard"
                                ctx
                                state)
                              (chk-logic-subfunctions names
                                names
                                split-types-terms
                                wrld3
                                "split-types expression"
                                ctx
                                state)
                              (chk-logic-subfunctions names
                                names
                                bodies
                                wrld3
                                "body"
                                ctx
                                state))
                            (value nil))
                          (if (global-val 'boot-strap-flg (w state))
                            (value nil)
                            (er-progn (chk-badged-quoted-subfunctions names
                                names
                                guards
                                wrld3
                                "guard"
                                ctx
                                state)
                              (chk-badged-quoted-subfunctions names
                                names
                                split-types-terms
                                wrld3
                                "split-types expression"
                                ctx
                                state)
                              (chk-badged-quoted-subfunctions names
                                names
                                bodies
                                wrld3
                                "body"
                                ctx
                                state)))
                          (if (eq symbol-class :common-lisp-compliant)
                            (er-progn (chk-common-lisp-compliant-subfunctions names
                                names
                                guards
                                wrld3
                                "guard"
                                ctx
                                state)
                              (chk-common-lisp-compliant-subfunctions names
                                names
                                split-types-terms
                                wrld3
                                "split-types expression"
                                ctx
                                state)
                              (chk-common-lisp-compliant-subfunctions names
                                names
                                bodies
                                wrld3
                                "body"
                                ctx
                                state))
                            (value nil))
                          (mv-let (erp val state)
                            (cond (assumep (mv nil nil state))
                              (t (let ((ignores (get-ignores fives)) (ignorables (get-ignorables fives))
                                    (irrelevants-alist (get-irrelevants-alist fives)))
                                  (er-progn (chk-free-and-ignored-vars-lsts names
                                      arglists
                                      guards
                                      split-types-terms
                                      measures
                                      ignores
                                      ignorables
                                      bodies
                                      ctx
                                      state)
                                    (chk-irrelevant-formals names
                                      arglists
                                      guards
                                      split-types-terms
                                      measures
                                      ignores
                                      ignorables
                                      irrelevants-alist
                                      bodies
                                      ctx
                                      state)
                                    (chk-mutual-recursion names bodies ctx state)))))
                            (cond (erp (mv erp val state))
                              (t (er-let* ((new-lambda$-alist-pairs (if non-executablep
                                       (value nil)
                                       (chk-acceptable-lambda$-translations symbol-class
                                         guards
                                         bodies
                                         ctx
                                         wrld3
                                         state))) (new-loop$-alist-pairs (if non-executablep
                                        (value nil)
                                        (chk-acceptable-loop$-translations symbol-class
                                          guards
                                          bodies
                                          ctx
                                          wrld3
                                          state)))
                                    (global-stobjs-prop (value (global-stobjs-prop names bodies guards wrld2a)))
                                    (wrld5 (value (if global-stobjs-prop
                                          (putprop-x-lst1 names
                                            'global-stobjs
                                            global-stobjs-prop
                                            wrld4)
                                          wrld4)))
                                    (ignore (cond ((and global-stobjs-prop
                                           (not assumep)
                                           (or (ffnnamesp-lst names bodies)
                                             (ffnnamesp-lst names guards))) (er-progn (update-w t wrld5)
                                            (translate-bodies non-executablep
                                              names
                                              arglists
                                              (get-bodies fives)
                                              (if (car loop$-recursion-lst)
                                                (list (cons (car names) '(nil)))
                                                (pairlis$ names names))
                                              stobjs-in-lst
                                              reclassifying-all-programp
                                              ctx
                                              wrld5
                                              state)
                                            (translate-guards guards0
                                              arglists
                                              stobjs-in-lst
                                              ctx
                                              wrld5
                                              state
                                              state-vars)))
                                        (t (value nil)))))
                                  (value (list 'chk-acceptable-defuns
                                      names
                                      arglists
                                      docs
                                      nil
                                      guards
                                      measures
                                      ruler-extenders-lst
                                      mp
                                      rel
                                      hints
                                      guard-hints
                                      std-hints
                                      otf-flg
                                      bodies
                                      symbol-class
                                      normalizeps
                                      reclassifying-all-programp
                                      wrld5
                                      non-executablep
                                      guard-debug
                                      measure-debug
                                      split-types-terms
                                      (make lambda-info
                                        :loop$-recursion (car loop$-recursion-lst)
                                        :new-lambda$-alist-pairs new-lambda$-alist-pairs
                                        :new-loop$-alist-pairs new-loop$-alist-pairs)
                                      guard-simplify
                                      type-prescription-lst)))))))))))))))))))

(defun conditionally-memoized-fns
  (fns memoize-table)
  (declare (xargs :guard (and (symbol-listp fns) (alistp memoize-table))))
  (cond ((endp fns) nil)
    (t (let ((alist (cdr (assoc-eq (car fns) memoize-table))))
        (cond ((and alist
             (let ((condition-fn (cdr (assoc-eq :condition-fn alist))))
               (and condition-fn (not (eq condition-fn t))))) (cons (car fns)
              (conditionally-memoized-fns (cdr fns) memoize-table)))
          (t (conditionally-memoized-fns (cdr fns) memoize-table)))))))

(defun chk-acceptable-defuns
  (lst ctx wrld state)
  (er-let* ((fives (chk-defuns-tuples lst nil ctx wrld state)) (names (value (strip-cars fives))))
    (er-progn (chk-no-duplicate-defuns names ctx state)
      (chk-xargs-keywords fives *xargs-keywords* ctx state)
      (er-let* ((tuple (chk-acceptable-defuns0 fives ctx wrld state)))
        (let* ((stobjs-in-lst (car tuple)) (defun-mode (cadr tuple))
            (non-executablep (caddr tuple))
            (symbol-class (cdddr tuple))
            (rc (redundant-or-reclassifying-defunsp defun-mode
                symbol-class
                (ld-skip-proofsp state)
                lst
                ctx
                wrld
                (ld-redefinition-action state)
                fives
                non-executablep
                stobjs-in-lst
                (default-state-vars t))))
          (cond ((eq rc 'redundant) (chk-acceptable-defuns-redundancy names
                defun-mode
                ctx
                wrld
                state))
            ((eq rc 'verify-guards) (chk-acceptable-defuns-verify-guards-er names
                ctx
                wrld
                state))
            ((and (eq rc 'reclassifying)
               (conditionally-memoized-fns names
                 (table-alist 'memoize-table wrld))) (er soft
                ctx
                "It is illegal to verify termination (i.e., convert from ~
              :program to :logic mode) for function~#0~[~/s~] ~&0, because ~
              ~#0~[it is~/they are~] currently memoized with conditions; you ~
              need to unmemoize ~#0~[it~/them~] first.  See :DOC memoize."
                (conditionally-memoized-fns names
                  (table-alist 'memoize-table wrld))))
            (t (chk-acceptable-defuns1 names
                fives
                stobjs-in-lst
                defun-mode
                symbol-class
                rc
                non-executablep
                ctx
                wrld
                state))))))))

(defun union-eq1-rev
  (x y)
  (cond ((endp x) y)
    ((member-eq (car x) y) (union-eq1-rev (cdr x) y))
    (t (union-eq1-rev (cdr x) (cons (car x) y)))))

(defun collect-hereditarily-constrained-fnnames
  (names wrld ans)
  (cond ((endp names) ans)
    (t (let ((name-fns (getpropc (car names)
             'hereditarily-constrained-fnnames
             nil
             wrld)))
        (cond (name-fns (collect-hereditarily-constrained-fnnames (cdr names)
              wrld
              (union-eq1-rev name-fns ans)))
          (t (collect-hereditarily-constrained-fnnames (cdr names)
              wrld
              ans)))))))

(defun putprop-hereditarily-constrained-fnnames-lst
  (names fnnames-bodies wrld)
  (let ((fnnames (collect-hereditarily-constrained-fnnames fnnames-bodies
         wrld
         nil)))
    (cond (fnnames (global-set 'defined-hereditarily-constrained-fns
          (append names
            (global-val 'defined-hereditarily-constrained-fns wrld))
          (putprop-x-lst1 names
            'hereditarily-constrained-fnnames
            (append names fnnames)
            wrld)))
      (t wrld))))

(defun inline-namep
  (sname)
  (declare (xargs :guard (stringp sname)))
  (let ((len (length sname)))
    (and (not (int= len 0))
      (terminal-substringp *inline-suffix*
        sname
        *inline-suffix-len-minus-1*
        (1- len)))))

(defun notinline-namep
  (sname)
  (declare (xargs :guard (stringp sname)))
  (let ((len (length sname)))
    (and (not (int= len 0))
      (terminal-substringp *notinline-suffix*
        sname
        *notinline-suffix-len-minus-1*
        (1- len)))))

(defun split-inlines
  (names inlines not-inlines)
  (declare (xargs :guard (symbol-listp names)))
  (cond ((endp names) (mv inlines not-inlines))
    ((inline-namep (symbol-name (car names))) (split-inlines (cdr names)
        (cons (car names) inlines)
        not-inlines))
    (t (split-inlines (cdr names)
        inlines
        (cons (car names) not-inlines)))))

(defun put-ext-gen-info
  (ext-gens ext-gen-barriers names fnnames-bodies guards wrld)
  (cond ((null ext-gens) (assert$ (eq ext-gen-barriers nil) wrld))
    ((or (intersectp-eq ext-gens fnnames-bodies)
       (intersectp-eq ext-gens (all-fnnames-lst guards))) (mv-let (inlines not-inlines)
        (split-inlines names nil nil)
        (let* ((wrld (if inlines
               (global-set 'ext-gens (append inlines ext-gens) wrld)
               wrld)) (wrld (if not-inlines
                (global-set 'ext-gen-barriers
                  (append not-inlines ext-gen-barriers)
                  wrld)
                wrld)))
          wrld)))
    (t wrld)))

(defun defuns-fn1
  (tuple ens
    big-mutrec
    names
    arglists
    docs
    pairs
    guards
    guard-hints
    std-hints
    otf-flg
    guard-debug
    guard-simplify
    bodies
    symbol-class
    normalizeps
    split-types-terms
    lambda-info
    non-executablep
    type-prescription-lst
    ctx
    state)
  (declare (ignore std-hints))
  (declare (ignore docs pairs))
  (let* ((col (car tuple)) (subversive-p (cdddr tuple))
      (wrld0 (w state))
      (ext-gens (global-val 'ext-gens wrld0))
      (ext-gen-barriers (global-val 'ext-gen-barriers wrld0)))
    (er-let* ((wrld1 (update-w big-mutrec (cadr tuple))) (wrld2 (update-w big-mutrec
            (putprop-defun-runic-mapping-pairs names t wrld1)))
        (wrld3 (update-w big-mutrec
            (putprop-x-lst2-unless names 'guard guards *t* wrld2)))
        (wrld4 (update-w big-mutrec
            (putprop-x-lst2-unless names
              'split-types-term
              split-types-terms
              *t*
              wrld3)))
        (ttree1 (value (caddr tuple))))
      (mv-let (wrld5 ttree2)
        (putprop-body-lst names
          arglists
          bodies
          normalizeps
          (getpropc (car names) 'recursivep nil wrld4)
          (make-controller-alist names wrld4)
          ens
          wrld4
          wrld4
          nil)
        (er-progn (update-w big-mutrec wrld5)
          (mv-let (wrld6 ttree2 state)
            (putprop-type-prescription-lst names
              subversive-p
              (fn-rune-nume (car names) t nil wrld5)
              ens
              wrld5
              ttree2
              state)
            (er-progn (update-w big-mutrec wrld6)
              (let* ((wrld6a (if (access lambda-info lambda-info :loop$-recursion)
                     (putprop (car names) 'loop$-recursion t wrld6)
                     wrld6)) (lambda$-alist-wrld6a (global-val 'lambda$-alist wrld6a))
                  (new-lambda$-alist-pairs (access lambda-info lambda-info :new-lambda$-alist-pairs))
                  (wrld6b (if (subsetp-equal new-lambda$-alist-pairs lambda$-alist-wrld6a)
                      wrld6a
                      (global-set 'lambda$-alist
                        (union-equal new-lambda$-alist-pairs lambda$-alist-wrld6a)
                        wrld6a)))
                  (loop$-alist-wrld6b (global-val 'loop$-alist wrld6b))
                  (new-loop$-alist-pairs (access lambda-info lambda-info :new-loop$-alist-pairs))
                  (wrld6c (if (subsetp-equal new-loop$-alist-pairs loop$-alist-wrld6b)
                      wrld6b
                      (global-set 'loop$-alist
                        (union-equal new-loop$-alist-pairs loop$-alist-wrld6b)
                        wrld6b)))
                  (fnnames-bodies (all-fnnames1 t bodies nil)))
                (er-progn (update-w big-mutrec wrld6c)
                  (er-let* ((wrld7 (update-w big-mutrec (putprop-level-no-lst names wrld6c))) (wrld8 (update-w big-mutrec
                          (putprop-primitive-recursive-defunp-lst names wrld7)))
                      (wrld9 (update-w big-mutrec
                          (putprop-hereditarily-constrained-fnnames-lst names
                            fnnames-bodies
                            wrld8)))
                      (wrld10 (update-w big-mutrec
                          (put-invariant-risk names
                            bodies
                            non-executablep
                            symbol-class
                            guards
                            wrld9)))
                      (wrld11 (update-w big-mutrec
                          (putprop-x-lst1 names
                            'pequivs
                            nil
                            (putprop-x-lst1 names 'congruences nil wrld10))))
                      (wrld12 (update-w big-mutrec
                          (putprop-x-lst1 names 'coarsenings nil wrld11)))
                      (wrld13 (update-w big-mutrec
                          (if non-executablep
                            (putprop-x-lst1 names
                              'non-executablep
                              non-executablep
                              wrld12)
                            wrld12)))
                      (wrld14 (update-w big-mutrec
                          (put-ext-gen-info ext-gens
                            ext-gen-barriers
                            names
                            fnnames-bodies
                            guards
                            wrld13))))
                    (let ((wrld15 wrld14))
                      (pprogn (print-defun-msg names ttree2 wrld15 col state)
                        (set-w 'extension wrld15 state)
                        (er-progn (chk-type-prescription-lst names
                            arglists
                            type-prescription-lst
                            ens
                            wrld15
                            ctx
                            state)
                          (cond ((eq symbol-class :common-lisp-compliant) (er-let* ((guard-hints (if guard-hints
                                     (translate-hints (cons "Guard for" (car names))
                                       guard-hints
                                       ctx
                                       wrld15
                                       state)
                                     (value nil))) (pair (verify-guards-fn1 names
                                      guard-hints
                                      otf-flg
                                      guard-debug
                                      guard-simplify
                                      ctx
                                      state)))
                                (value (cons (car pair)
                                    (cons-tag-trees ttree1 (cons-tag-trees ttree2 (cdr pair)))))))
                            (t (value (cons wrld15 (cons-tag-trees ttree1 ttree2))))))))))))))))))

(defun defuns-fn0
  (names arglists
    docs
    pairs
    guards
    measures
    ruler-extenders-lst
    mp
    rel
    hints
    guard-hints
    std-hints
    otf-flg
    guard-debug
    guard-simplify
    measure-debug
    bodies
    symbol-class
    normalizeps
    split-types-terms
    lambda-info
    non-executablep
    type-prescription-lst
    ctx
    wrld
    state)
  (cond ((eq symbol-class :program) (defuns-fn-short-cut t
        (access lambda-info lambda-info :loop$-recursion)
        names
        docs
        pairs
        guards
        measures
        split-types-terms
        bodies
        non-executablep
        ctx
        wrld
        state))
    (t (let ((ens (ens state)) (big-mutrec (big-mutrec names)))
        (er-let* ((tuple (put-induction-info (access lambda-info lambda-info :loop$-recursion)
               names
               arglists
               measures
               ruler-extenders-lst
               bodies
               mp
               rel
               hints
               otf-flg
               big-mutrec
               measure-debug
               ctx
               ens
               wrld
               state)))
          (defuns-fn1 tuple
            ens
            big-mutrec
            names
            arglists
            docs
            pairs
            guards
            guard-hints
            std-hints
            otf-flg
            guard-debug
            guard-simplify
            bodies
            symbol-class
            normalizeps
            split-types-terms
            lambda-info
            non-executablep
            type-prescription-lst
            ctx
            state))))))

(defun strip-non-hidden-package-names
  (known-package-alist)
  (declare (xargs :guard (known-package-alistp known-package-alist)))
  (cond ((endp known-package-alist) nil)
    (t (let ((package-entry (car known-package-alist)))
        (cond ((package-entry-hidden-p package-entry) (strip-non-hidden-package-names (cdr known-package-alist)))
          (t (cons (package-entry-name package-entry)
              (strip-non-hidden-package-names (cdr known-package-alist)))))))))

(defun in-package-fn
  (str state)
  (cond ((not (stringp str)) (er soft
        'in-package
        "The argument to IN-PACKAGE must be a string, but ~
              ~x0 is not."
        str))
    ((not (find-non-hidden-package-entry str
         (known-package-alist state))) (er soft
        'in-package
        "The argument to IN-PACKAGE must be a known package ~
              name, but ~x0 is not.  The known packages are ~*1~@2"
        str
        (tilde-*-&v-strings '&
          (strip-non-hidden-package-names (known-package-alist state))
          #\.)
        (if (global-val 'include-book-path (w state))
          (msg "~%NOTE: This error might be eliminated by certifying ~
                       the book,~|~x0.~|See :DOC certify-book."
            (book-name-to-filename (car (global-val 'include-book-path (w state)))
              (w state)
              'in-package))
          "")))
    (t (let ((state (f-put-global 'current-package str state)))
        (value str)))))

(defun defstobj-functionsp
  (names embedded-event-lst)
  (let ((temp (assoc-eq 'defstobj embedded-event-lst)))
    (cond ((and temp (subsetp-equal names (caddr temp))) (cadr temp))
      (t nil))))

(defun index-of-non-number
  (lst)
  (cond ((endp lst) nil)
    ((acl2-numberp (car lst)) (let ((temp (index-of-non-number (cdr lst))))
        (and temp (1+ temp))))
    (t 0)))

(defun make-udf-insigs
  (names wrld)
  (cond ((endp names) nil)
    (t (cons (list (car names)
          (formals (car names) wrld)
          (stobjs-in (car names) wrld)
          (getpropc (car names) 'stobjs-out '(nil) wrld))
        (make-udf-insigs (cdr names) wrld)))))

(defun intro-udf
  (insig wrld)
  (case-match insig
    ((fn formals stobjs-in stobjs-out) (putprop fn
        'coarsenings
        nil
        (putprop fn
          'congruences
          nil
          (putprop fn
            'pequivs
            nil
            (putprop fn
              'constrainedp
              t
              (putprop fn
                'hereditarily-constrained-fnnames
                (list fn)
                (putprop fn
                  'symbol-class
                  :common-lisp-compliant (putprop-unless fn
                    'stobjs-out
                    stobjs-out
                    nil
                    (putprop-unless fn
                      'stobjs-in
                      stobjs-in
                      nil
                      (putprop fn 'formals formals (putprop fn 'guard *t* wrld)))))))))))
    (& (er hard 'store-signature "Unrecognized signature!"))))

(defun intro-udf-lst1
  (insigs wrld)
  (cond ((null insigs) wrld)
    (t (intro-udf-lst1 (cdr insigs) (intro-udf (car insigs) wrld)))))

(defun intro-udf-lst2
  (insigs kwd-value-list-lst)
  (cond ((null insigs) nil)
    (t (cons `(,(CAAR INSIGS) ,(CADAR INSIGS)
          ,@(COND
   ((EQ KWD-VALUE-LIST-LST 'NON-EXECUTABLE-PROGRAMP)
    '((DECLARE (XARGS :NON-EXECUTABLE :PROGRAM))))
   (T
    (LET ((GUARD (CADR (ASSOC-KEYWORD :GUARD (CAR KWD-VALUE-LIST-LST)))))
      (AND GUARD `((DECLARE (XARGS :GUARD ,GUARD)))))))
          ,(NULL-BODY-ER (CAAR INSIGS) (CADAR INSIGS) T))
        (intro-udf-lst2 (cdr insigs)
          (if (eq kwd-value-list-lst 'non-executable-programp)
            'non-executable-programp
            (cdr kwd-value-list-lst)))))))

(defun intro-udf-lst
  (insigs kwd-value-list-lst in-local-flg wrld state)
  (if (null insigs)
    wrld
    (put-cltl-command `(defuns nil
        nil
        ,@(INTRO-UDF-LST2 INSIGS
                  (AND (NOT (EQ KWD-VALUE-LIST-LST T)) KWD-VALUE-LIST-LST)))
      in-local-flg
      (intro-udf-lst1 insigs wrld)
      wrld
      state)))

(defun defun-ctx
  (def-lst)
  (cond ((atom def-lst) (msg "( DEFUNS ~x0)" def-lst))
    ((atom (car def-lst)) (cons 'defuns (car def-lst)))
    ((null (cdr def-lst)) (cons 'defun (caar def-lst)))
    (t (msg *mutual-recursion-ctx-string* (caar def-lst)))))

(defun install-event-defuns
  (names event-form
    def-lst0
    symbol-class
    reclassifyingp
    non-executablep
    pair
    ctx
    wrld
    state)
  (install-event (cond ((null (cdr names)) (car names)) (t names))
    event-form
    (cond ((null (cdr names)) 'defun) (t 'defuns))
    (cond ((null (cdr names)) (car names)) (t names))
    (cdr pair)
    (cond (non-executablep `(defuns nil
          nil
          ,@(INTRO-UDF-LST2 (MAKE-UDF-INSIGS NAMES WRLD)
                  (AND (EQ NON-EXECUTABLEP :PROGRAM) 'NON-EXECUTABLE-PROGRAMP))))
      (t `(defuns ,(IF (EQ SYMBOL-CLASS :PROGRAM)
     :PROGRAM
     :LOGIC)
          ,(IF RECLASSIFYINGP
     'RECLASSIFYING
     (IF (DEFSTOBJ-FUNCTIONSP NAMES
                              (GLOBAL-VAL 'EMBEDDED-EVENT-LST (CAR PAIR)))
         (CONS 'DEFSTOBJ
               (DEFSTOBJ-FUNCTIONSP NAMES
                                    (GLOBAL-VAL 'EMBEDDED-EVENT-LST
                                                (CAR PAIR))))
         NIL))
          ,@DEF-LST0)))
    t
    ctx
    (car pair)
    state))

(defun defuns-fn
  (def-lst state event-form)
  (with-ctx-summarized (defun-ctx def-lst)
    (let ((wrld (w state)) (def-lst0 def-lst)
        (event-form (or event-form (list 'defuns def-lst))))
      (revert-world-on-error (er-let* ((tuple (chk-acceptable-defuns def-lst ctx wrld state)))
          (cond ((eq (car tuple) 'redundant) (stop-redundant-event ctx
                state
                :name (caar def-lst0)
                :defun-mode (cdr tuple)
                :def-lst def-lst0))
            (t (enforce-redundancy event-form
                ctx
                wrld
                (let ((names (nth 1 tuple)) (arglists (nth 2 tuple))
                    (docs (nth 3 tuple))
                    (pairs (nth 4 tuple))
                    (guards (nth 5 tuple))
                    (measures (nth 6 tuple))
                    (ruler-extenders-lst (nth 7 tuple))
                    (mp (nth 8 tuple))
                    (rel (nth 9 tuple))
                    (hints (nth 10 tuple))
                    (guard-hints (nth 11 tuple))
                    (std-hints (nth 12 tuple))
                    (otf-flg (nth 13 tuple))
                    (bodies (nth 14 tuple))
                    (symbol-class (nth 15 tuple))
                    (normalizeps (nth 16 tuple))
                    (reclassifyingp (nth 17 tuple))
                    (wrld (nth 18 tuple))
                    (non-executablep (nth 19 tuple))
                    (guard-debug (nth 20 tuple))
                    (measure-debug (nth 21 tuple))
                    (split-types-terms (nth 22 tuple))
                    (lambda-info (nth 23 tuple))
                    (guard-simplify (nth 24 tuple))
                    (type-prescription-lst (nth 25 tuple)))
                  (with-useless-runes (car names)
                    wrld
                    (er-let* ((pair (defuns-fn0 names
                           arglists
                           docs
                           pairs
                           guards
                           measures
                           ruler-extenders-lst
                           mp
                           rel
                           hints
                           guard-hints
                           std-hints
                           otf-flg
                           guard-debug
                           guard-simplify
                           measure-debug
                           bodies
                           symbol-class
                           normalizeps
                           split-types-terms
                           lambda-info
                           non-executablep
                           type-prescription-lst
                           ctx
                           wrld
                           state)))
                      (er-progn (chk-assumption-free-ttree (cdr pair) ctx state)
                        (if (access lambda-info lambda-info :loop$-recursion)
                          (let ((wrld (car pair)))
                            (mv-let (erp msg-and-badge)
                              (ev-fncall-w 'badger
                                (list (car names) wrld)
                                wrld
                                nil
                                nil
                                nil
                                t
                                t)
                              (let ((msg1 msg-and-badge) (msg2 (if erp
                                      nil
                                      (car msg-and-badge)))
                                  (badge (if erp
                                      nil
                                      (cadr msg-and-badge))))
                                (cond ((or erp msg2) (er soft
                                      'defun
                                      "When :LOOP$-RECURSION T is declared for a ~
                                 function, as it was for ~x0, we must assign ~
                                 it a badge before we translate its body.  ~
                                 That assigned badge asserts that ~x0 returns ~
                                 a single value and is tame.  We then check ~
                                 that assumption after translation by ~
                                 generating the badge using the technique ~
                                 that DEFWARRANT would use.  But the attempt ~
                                 to generate the badge has failed, indicating ~
                                 that it is illegal to declare ~
                                 :LOOP$-RECURSION T for this function.  ~
                                 ~#1~[Our attempt to generate a badge ~
                                 produced the following error:~/The error ~
                                 message that would be reported by DEFWARRANT ~
                                 is:~]~%~%~@2"
                                      (car names)
                                      (if erp
                                        0
                                        1)
                                      (if erp
                                        msg1
                                        msg2)))
                                  ((not (equal (access apply$-badge badge :out-arity) 1)) (er soft
                                      'defun
                                      "Impossible error!  The final badger check in ~
                                 DEFUNS-FN has failed on the :OUT-ARITY.  ~
                                 This is impossible given ~
                                 chk-acceptable-defuns1. Please show the ~
                                 implementors this bug!"))
                                  ((not (eq (access apply$-badge badge :ilks) t)) (er soft
                                      'defun
                                      "When :LOOP$-RECURSION T is declared for a ~
                                 function the function must be tame.  But ~x0 ~
                                 is not!  Its ilks are actually ~x1."
                                      (car names)
                                      (access apply$-badge badge :ilks)))
                                  (t (value nil))))))
                          (value nil))
                        (install-event-defuns names
                          event-form
                          def-lst0
                          symbol-class
                          reclassifyingp
                          non-executablep
                          pair
                          ctx
                          wrld
                          state)))))))))))
    :event-type 'defun
    :event event-form))

(defun defun-fn
  (def state event-form)
  (defuns-fn (list def)
    state
    (or event-form (cons 'defun def))))

(defun args-fn
  (name state)
  (io? temporary
    nil
    (mv erp val state)
    (name)
    (let ((wrld (w state)) (channel (standard-co state)))
      (cond ((member-eq name *stobjs-out-invalid*) (pprogn (fms "Special form, basic to ACL2.  See :DOC ~x0.~|~%"
              (list (cons #\0 name))
              channel
              state
              nil)
            (value name)))
        ((and (symbolp name) (function-symbolp name wrld)) (let* ((formals (formals name wrld)) (stobjs-in (stobjs-in name wrld))
              (stobjs-out (stobjs-out name wrld))
              (guard (untranslate (guard name nil wrld) t wrld))
              (tp (find-runed-type-prescription (list :type-prescription name)
                  (getpropc name 'type-prescriptions nil wrld)))
              (tpthm (cond (tp (untranslate (access type-prescription tp :corollary)
                      t
                      wrld))
                  (t nil)))
              (badge (executable-badge name wrld))
              (warrant (find-warrant-function-name name wrld))
              (constraint-msg (mv-let (some-name constraint-lst origins)
                  (constraint-info name wrld)
                  (declare (ignore origins))
                  (cond ((unknown-constraints-p constraint-lst) "[UNKNOWN-CONSTRAINTS]")
                    (t (let ((constraint (if some-name
                             (untranslate (conjoin constraint-lst) t wrld)
                             t)))
                        (if (eq constraint t)
                          ""
                          (msg "~y0" constraint))))))))
            (pprogn (fms "Function         ~x0~|~
               Formals:         ~y1~|~
               Signature:       ~y2~|~
               ~                 => ~y3~|~
               Guard:           ~q4~|~
               Guards Verified: ~y5~|~
               Defun-Mode:      ~@6~|~
               Type:            ~#7~[built-in (or unrestricted)~/~q8~]~|~
               Badge:           ~#b~[~yc~/none~]~|~
               Warrant:         ~#d~[built-in~/~ye~/none~]~|~
               ~#9~[~/Constraint:      ~@a~|~]~
               ~%"
                (list (cons #\0 name)
                  (cons #\1 formals)
                  (cons #\2 (cons name (prettyify-stobj-flags stobjs-in)))
                  (cons #\3 (prettyify-stobjs-out stobjs-out))
                  (cons #\4 guard)
                  (cons #\5
                    (eq (symbol-class name wrld) :common-lisp-compliant))
                  (cons #\6 (defun-mode-string (fdefun-mode name wrld)))
                  (cons #\7
                    (if tpthm
                      1
                      0))
                  (cons #\8 tpthm)
                  (cons #\9
                    (if (equal constraint-msg "")
                      0
                      1))
                  (cons #\a constraint-msg)
                  (cons #\b
                    (if badge
                      0
                      1))
                  (cons #\c badge)
                  (cons #\d
                    (if (eq warrant t)
                      0
                      (if warrant
                        1
                        2)))
                  (cons #\e warrant))
                channel
                state
                nil)
              (value name))))
        ((and (symbolp name) (getpropc name 'macro-body nil wrld)) (let ((args (macro-args name wrld)) (guard (untranslate (guard name nil wrld) t wrld)))
            (pprogn (fms "Macro ~x0~|~
                    Macro Args:  ~y1~|~
                    Guard:       ~Q23~|~%"
                (list (cons #\0 name)
                  (cons #\1 args)
                  (cons #\2 guard)
                  (cons #\3 (term-evisc-tuple nil state)))
                channel
                state
                nil)
              (value name))))
        ((member-eq name
           '(let lambda
             declare
             quote)) (pprogn (fms "Special form, basic to the Common Lisp language.  ~
                         See for example CLtL."
              nil
              channel
              state
              nil)
            (value name)))
        (t (er soft
            :args "~x0 is neither a function symbol nor a macro name known to ~
                  ACL2."
            name))))))

(defun make-verify-termination-def
  (old-def new-dcls wrld)
  (let* ((fn (car old-def)) (args (cadr old-def))
      (body (car (last (cddr old-def))))
      (dcls (butlast (cddr old-def) 1))
      (new-fields (dcl-fields new-dcls))
      (modified-old-dcls (strip-dcls (add-to-set-eq :mode new-fields) dcls)))
    (assert$ (not (getpropc fn 'non-executablep nil wrld))
      `(,FN ,ARGS
        ,@NEW-DCLS
        ,@(IF (NOT (MEMBER-EQ :MODE NEW-FIELDS))
      '((DECLARE (XARGS :MODE :LOGIC)))
      NIL)
        ,@MODIFIED-OLD-DCLS
        ,BODY))))

(defun make-verify-termination-defs-lst
  (defs-lst lst wrld)
  (cond ((null defs-lst) nil)
    (t (let ((temp (assoc-eq (caar defs-lst) lst)))
        (cons (make-verify-termination-def (car defs-lst) (cdr temp) wrld)
          (make-verify-termination-defs-lst (cdr defs-lst) lst wrld))))))

(defun chk-acceptable-verify-termination1
  (lst clique fn1 ctx wrld state)
  (cond ((null lst) (value nil))
    ((not (and (consp (car lst))
         (symbolp (caar lst))
         (function-symbolp (caar lst) wrld)
         (plausible-dclsp (cdar lst)))) (er soft
        ctx
        "Each argument to verify-termination must be of the form (name ~
              dcl ... dcl), where each dcl is either a DECLARE form or a ~
              documentation string.  The DECLARE forms may contain TYPE, ~
              IGNORE, and XARGS entries, where the legal XARGS keys are ~&0.  ~
              The argument ~x1 is illegal.  See :DOC verify-termination."
        *xargs-keywords*
        (car lst)))
    ((not (member-eq (caar lst) clique)) (er soft
        ctx
        "The function symbols whose termination is to be verified must ~
              all be members of the same clique of mutually recursive ~
              functions.  ~x0 is not in the clique of ~x1.  The clique of ~x1 ~
              consists of ~&2.  See :DOC verify-termination."
        (caar lst)
        fn1
        clique))
    (t (chk-acceptable-verify-termination1 (cdr lst)
        clique
        fn1
        ctx
        wrld
        state))))

(defun uniform-defun-modes
  (defun-mode clique wrld)
  (cond ((null clique) defun-mode)
    ((programp (car clique) wrld) (and (eq defun-mode :program)
        (uniform-defun-modes defun-mode (cdr clique) wrld)))
    (t (and (eq defun-mode :logic)
        (uniform-defun-modes defun-mode (cdr clique) wrld)))))

(defun chk-acceptable-verify-termination
  (lst ctx wrld state)
  (cond ((and (consp lst) (consp (car lst)) (symbolp (caar lst))) (cond ((not (function-symbolp (caar lst) wrld)) (er soft
            ctx
            "The symbol ~x0 is not a function symbol in the current ACL2 world."
            (caar lst)))
        ((and (not (programp (caar lst) wrld))
           (getpropc (caar lst) 'constrainedp nil wrld)) (er soft
            ctx
            "The :LOGIC mode function symbol ~x0 was originally introduced ~
           introduced not with DEFUN, but ~#1~[as a constrained ~
           function~/with DEFCHOOSE~].  So VERIFY-TERMINATION does not make ~
           sense for this function symbol."
            (caar lst)
            (cond ((getpropc (caar lst) 'defchoose-axiom nil wrld) 1)
              (t 0))))
        ((getpropc (caar lst) 'non-executablep nil wrld) (er soft
            ctx
            "The :PROGRAM mode function symbol ~x0 is declared non-executable, ~
           so ~x1 is not legal for this symbol.  Such functions are intended ~
           only for hacking with defattach; see :DOC defproxy."
            (caar lst)
            'verify-termination
            'defun))
        (t (let ((clique (get-clique (caar lst) wrld)))
            (assert$ (uniform-defun-modes (fdefun-mode (caar lst) wrld)
                clique
                wrld)
              (chk-acceptable-verify-termination1 lst
                clique
                (caar lst)
                ctx
                wrld
                state))))))
    ((atom lst) (er soft
        ctx
        "Verify-termination requires at least one argument."))
    (t (er soft
        ctx
        "The first argument supplied to verify-termination, ~x0, is not of ~
           the form (fn dcl ...)."
        (car lst)))))

(defun verify-termination1
  (lst state)
  (let* ((lst (cond ((and (consp lst) (symbolp (car lst))) (list lst))
         (t lst))) (ctx (cond ((null lst) "(VERIFY-TERMINATION)")
          ((and (consp lst) (consp (car lst))) (cond ((null (cdr lst)) (cond ((symbolp (caar lst)) (cond ((null (cdr (car lst))) (msg "( VERIFY-TERMINATION ~x0)" (caar lst)))
                      (t (msg "( VERIFY-TERMINATION ~x0 ...)" (caar lst)))))
                  ((null (cdr (car lst))) (msg "( VERIFY-TERMINATION (~x0))" (caar lst)))
                  (t (msg "( VERIFY-TERMINATION (~x0 ...))" (caar lst)))))
              ((null (cdr (car lst))) (msg "( VERIFY-TERMINATION (~x0) ...)" (caar lst)))
              (t (msg "( VERIFY-TERMINATION (~x0 ...) ...)" (caar lst)))))
          (t (cons 'verify-termination lst))))
      (wrld (w state)))
    (er-progn (chk-acceptable-verify-termination lst ctx wrld state)
      (let ((defs (recover-defs-lst (caar lst) wrld)))
        (value (make-verify-termination-defs-lst defs lst wrld))))))