prove

(defun more-than-simplifiedp
  (hist)
  (cond ((null hist) nil)
    ((member-eq (caar hist)
       '(settled-down-clause simplify-clause preprocess-clause)) (more-than-simplifiedp (cdr hist)))
    ((eq (caar hist) 'apply-top-hints-clause) (if (or (tagged-objectsp 'hidden-clause
            (access history-entry (car hist) :ttree))
          (tagged-objectsp ':or
            (access history-entry (car hist) :ttree)))
        (more-than-simplifiedp (cdr hist))
        t))
    (t t)))

(defun remove1-assoc-eq-lst
  (lst alist)
  (declare (xargs :guard (if (symbol-listp lst)
        (alistp alist)
        (symbol-alistp alist))))
  (if (consp lst)
    (remove1-assoc-eq-lst (cdr lst)
      (remove1-assoc-eq (car lst) alist))
    alist))

(defun delete-assumptions-1
  (recs only-immediatep)
  (cond ((endp recs) (mv nil nil))
    (t (mv-let (changedp new-cdr-recs)
        (delete-assumptions-1 (cdr recs) only-immediatep)
        (cond ((cond ((eq only-immediatep 'non-nil) (access assumption (car recs) :immediatep))
             ((eq only-immediatep 'case-split) (eq (access assumption (car recs) :immediatep) 'case-split))
             ((eq only-immediatep t) (eq (access assumption (car recs) :immediatep) t))
             (t t)) (mv t new-cdr-recs))
          (changedp (mv t (cons (car recs) new-cdr-recs)))
          (t (mv nil recs)))))))

(defun delete-assumptions
  (ttree only-immediatep)
  (let ((objects (tagged-objects 'assumption ttree)))
    (cond (objects (mv-let (changedp new-objects)
          (delete-assumptions-1 objects only-immediatep)
          (cond ((null changedp) ttree)
            (new-objects (extend-tag-tree 'assumption
                new-objects
                (remove-tag-from-tag-tree! 'assumption ttree)))
            (t (remove-tag-from-tag-tree! 'assumption ttree)))))
      (t ttree))))

(defun induction-depth-limit
  (wrld)
  (cdr (assoc-eq t (table-alist 'induction-depth-limit-table wrld))))

(defun push-clause-msg1-abort
  (cl-id ttree pspv state)
  (let ((temp (tagged-object 'abort-cause ttree)) (cl-id-phrase (tilde-@-clause-id-phrase cl-id))
      (gag-mode (gag-mode)))
    (case temp
      (empty-clause (if gag-mode
          (msg "A goal of NIL, ~@0, has been generated!  Obviously, the ~
                 proof attempt has failed.~|"
            cl-id-phrase)
          ""))
      ((do-not-induct do-not-induct-otf-flg-override) (msg "Normally we would attempt to prove ~@0 by induction.  However, a ~
             :DO-NOT-INDUCT hint was supplied to abort the proof attempt.~|"
          cl-id-phrase
          (if (eq temp 'do-not-induct)
            t
            :otf-flg-override)))
      (induction-depth-limit-exceeded (msg "Normally we would attempt to prove ~@0 by induction.  However, ~
             that would cause the induction-depth-limit of ~x1 to be ~
             exceeded.  See :DOC induction-depth-limit.~|"
          cl-id-phrase
          (length (access clause-id cl-id :pool-lst))))
      (otherwise (msg "Normally we would attempt to prove ~@0 by induction.  However, ~
             we prefer in this instance to focus on the original input ~
             conjecture rather than this simplified special case.  We ~
             therefore abandon our previous work on this conjecture and ~
             reassign the name ~@1 to the original conjecture.  (See :DOC ~
             otf-flg.)~#2~[~/  [Note:  Thanks again for the hint.]~]~|"
          cl-id-phrase
          (tilde-@-pool-name-phrase (access clause-id cl-id :forcing-round)
            (pool-lst (cdr (access prove-spec-var pspv :pool))))
          (if (and (not gag-mode)
              (access prove-spec-var pspv :hint-settings))
            1
            0))))))

(defun push-clause-msg1
  (cl-id signal clauses ttree pspv state)
  (declare (ignore clauses))
  (cond ((eq signal 'abort) (fms "~@0"
        (list (cons #\0 (push-clause-msg1-abort cl-id ttree pspv state)))
        (proofs-co state)
        state
        nil))
    (t (fms "Name the formula above ~@0.~|"
        (list (cons #\0
            (tilde-@-pool-name-phrase (access clause-id cl-id :forcing-round)
              (pool-lst (cdr (access prove-spec-var pspv :pool))))))
        (proofs-co state)
        state
        nil))))

(defun clause-set-subsumes-1
  (init-subsumes-count cl-set1 cl-set2 acc)
  (cond ((null cl-set2) acc)
    (t (let ((temp (some-member-subsumes init-subsumes-count
             cl-set1
             (car cl-set2)
             nil)))
        (and temp
          (clause-set-subsumes-1 init-subsumes-count
            cl-set1
            (cdr cl-set2)
            temp))))))

(defun clause-set-subsumes
  (init-subsumes-count cl-set1 cl-set2)
  (or (equal cl-set1 cl-set2)
    (and cl-set1
      cl-set2
      (null (cdr cl-set2))
      (subsetp-equal (car cl-set1) (car cl-set2)))
    (clause-set-subsumes-1 init-subsumes-count
      cl-set1
      cl-set2
      t)))

(defun preprocess-clause?
  (cl hist pspv wrld state step-limit)
  (cond ((member-eq 'preprocess-clause
       (assoc-eq :do-not (access prove-spec-var pspv :hint-settings))) (mv step-limit 'miss nil nil nil))
    (t (preprocess-clause cl hist pspv wrld state step-limit))))

(defun apply-use-hint-clauses
  (temp clauses pspv wrld state step-limit)
  (let* ((hyps (caddr temp)) (constraint-cl (cadddr temp))
      (new-pspv (change prove-spec-var
          pspv
          :hint-settings (remove1-equal temp
            (access prove-spec-var pspv :hint-settings))))
      (a (disjoin-clause-segment-to-clause-set (dumb-negate-lit-lst hyps)
          clauses))
      (non-tautp-applications (length a)))
    (cond ((null clauses) (mv step-limit 'hit nil nil new-pspv))
      (t (sl-let (signal c ttree irrel-pspv)
          (preprocess-clause? constraint-cl
            nil
            pspv
            wrld
            state
            step-limit)
          (declare (ignore irrel-pspv))
          (cond ((eq signal 'miss) (mv step-limit
                'hit
                (conjoin-clause-sets a
                  (conjoin-clause-to-clause-set constraint-cl nil))
                (add-to-tag-tree! :use (cons (cdr temp) non-tautp-applications)
                  nil)
                new-pspv))
            ((or (tag-tree-occur 'hidden-clause t ttree)
               (and c
                 (null (cdr c))
                 constraint-cl
                 (null (cdr constraint-cl))
                 (equal (prettyify-clause-simple (car c))
                   (car constraint-cl)))) (mv step-limit
                'hit
                (conjoin-clause-sets a c)
                (add-to-tag-tree! :use (cons (cdr temp) non-tautp-applications)
                  nil)
                new-pspv))
            (t (mv step-limit
                'hit
                (conjoin-clause-sets a c)
                (add-to-tag-tree! :use (cons (cdr temp) non-tautp-applications)
                  (add-to-tag-tree! 'preprocess-ttree ttree nil))
                new-pspv))))))))

(defun apply-cases-hint-clause
  (temp cl pspv wrld)
  (let ((new-clauses (remove-trivial-clauses (conjoin-clause-to-clause-set (disjoin-clauses (cdr temp) cl)
           (split-on-assumptions (dumb-negate-lit-lst (reverse (cdr temp)))
             cl
             nil))
         wrld)))
    (mv 'hit
      new-clauses
      (add-to-tag-tree! :cases (cons (cdr temp) new-clauses) nil)
      (change prove-spec-var
        pspv
        :hint-settings (remove1-equal temp
          (access prove-spec-var pspv :hint-settings))))))

(defun non-term-listp-msg
  (x w)
  (declare (xargs :guard t))
  (cond ((atom x) (assert$ x "that fails to satisfy true-listp."))
    ((not (termp (car x) w)) (msg "that contains the following non-termp (see :DOC term):~|~%  ~Y01"
        (car x)
        nil))
    (t (non-term-listp-msg (cdr x) w))))

(defun non-term-list-listp-msg
  (l w)
  (declare (xargs :guard t))
  (cond ((atom l) (assert$ l "which fails to satisfy true-listp."))
    ((not (term-listp (car l) w)) (msg "which has a member~|~%  ~Y01~|~%~@2"
        (car l)
        nil
        (non-term-listp-msg (car l) w)))
    (t (non-term-list-listp-msg (cdr l) w))))

(defun all-ffn-symbs-lst-lst
  (lst ans)
  (cond ((null lst) ans)
    (t (all-ffn-symbs-lst-lst (cdr lst)
        (all-ffn-symbs-lst (car lst) ans)))))

(defun tilde-@-unknown-names-phrase
  (lst field wrld acc)
  (declare (xargs :guard (and (true-listp lst)
        (plist-worldp wrld)
        (null (collect-non-hint-events lst t)))))
  (cond ((endp lst) (and acc
        (msg "its ~x0 field contains the following that ~#1~[does not ~
                    name an event~/do not name events~]: ~&1"
          field
          acc)))
    (t (let ((name (if (symbolp (car lst))
             (car lst)
             (cadr (car lst)))))
        (cond ((getpropc name 'absolute-event-number nil wrld) (tilde-@-unknown-names-phrase (cdr lst) field wrld acc))
          (t (tilde-@-unknown-names-phrase (cdr lst)
              field
              wrld
              (cons name acc))))))))

(defun tilde-@-illegal-hint-events-phrase
  (lst field wrld)
  (declare (xargs :guard (and (member-eq field
          '(:use-names :by-names :clause-processor-fns))
        (plist-worldp wrld))))
  (cond ((not (true-listp lst)) (msg "its ~x0 field, ~x1, is not a true-list" field lst))
    (t (let* ((non-symbols-okp (member-eq field '(:use-names :by-names))) (bad (collect-non-hint-events lst non-symbols-okp)))
        (cond (bad (msg "its ~x0 field contains the following illegal ~
                         object~#1~[/s~]: ~&1"
              field
              bad))
          (t (tilde-@-unknown-names-phrase lst field wrld nil)))))))

(defun collect-non-runes-from-summary-data
  (runes wrld)
  (declare (xargs :mode :program :guard (and (true-listp runes) (plist-worldp wrld))))
  (cond ((endp runes) nil)
    ((let ((r (car runes)))
       (and (consp r)
         (consp (cdr r))
         (or (null (cadr r)) (runep r wrld)))) (collect-non-runes-from-summary-data (cdr runes) wrld))
    (t (cons (car runes)
        (collect-non-runes-from-summary-data (cdr runes) wrld)))))

(defun tilde-@-illegal-summary-data-phrase
  (x wrld)
  (declare (xargs :mode :program))
  (and x
    (or (and (not (weak-summary-data-p x))
        (msg "it is not a summary-data record.  Use ~x0 to ~
                      create such a record (see :DOC make-summary-data)"
          'make-summary-data))
      (let ((runes (access summary-data x :runes)))
        (or (and (not (true-listp runes))
            (msg "its :runes field, ~x0, is not a true-list" runes))
          (let ((bad (collect-non-runes-from-summary-data runes wrld)))
            (and bad
              (msg "its :runes field contains the following list of ~
                              unknown runes: ~x0"
                bad)))))
      (tilde-@-illegal-hint-events-phrase (access summary-data x :use-names)
        :use-names wrld)
      (tilde-@-illegal-hint-events-phrase (access summary-data x :by-names)
        :by-names wrld)
      (tilde-@-illegal-hint-events-phrase (access summary-data x :clause-processor-fns)
        :clause-processor-fns wrld))))

(defun eval-clause-processor
  (clause term stobjs-out verified-p pspv ctx state)
  (revert-world-on-error (let ((original-wrld (w state)) (cl-term (subst-var (kwote clause) 'clause term)))
      (protect-system-state-globals (mv-let (erp trans-result state)
          (ev-for-trans-eval cl-term
            stobjs-out
            ctx
            state
            t
            (f-get-global 'ld-user-stobjs-modified-warning state))
          (cond (erp (mv (msg "Evaluation failed for the :clause-processor hint.")
                nil
                state))
            (t (assert$ (equal (car trans-result) stobjs-out)
                (let* ((result (cdr trans-result)) (eval-erp (and (cdr stobjs-out) (car result)))
                    (val (if (cdr stobjs-out)
                        (cadr result)
                        result)))
                  (cond ((stringp eval-erp) (mv (msg "~s0" eval-erp) nil state))
                    ((tilde-@p eval-erp) (mv (msg "Error in clause-processor hint:~|~%  ~@0" eval-erp)
                        nil
                        state))
                    (eval-erp (mv (msg "Error in clause-processor hint:~|~%  ~Y01" term nil)
                        nil
                        state))
                    (t (pprogn (set-w! original-wrld state)
                        (cond ((equal val (list clause)) (value (cons val nil)))
                          (t (let* ((user-says-skip-termp-checkp (skip-meta-termp-checks (ffn-symb term) original-wrld)) (well-formedness-guarantee (if (consp verified-p)
                                    verified-p
                                    nil))
                                (not-skipped (and (not user-says-skip-termp-checkp)
                                    (not well-formedness-guarantee)))
                                (bad-arity-info (if (and well-formedness-guarantee
                                      (not user-says-skip-termp-checkp))
                                    (collect-bad-fn-arity-info (cdr well-formedness-guarantee)
                                      original-wrld
                                      nil
                                      nil)
                                    nil)))
                              (cond (bad-arity-info (let ((name (nth 0 (car well-formedness-guarantee))) (fn (nth 1 (car well-formedness-guarantee)))
                                      (thm-name1 (nth 2 (car well-formedness-guarantee))))
                                    (mv (bad-arities-msg name
                                        :clause-processor fn
                                        nil
                                        thm-name1
                                        nil
                                        bad-arity-info)
                                      nil
                                      state)))
                                ((and not-skipped
                                   (not (logic-term-list-listp val original-wrld))) (cond ((not (term-list-listp val original-wrld)) (mv (msg "The :CLAUSE-PROCESSOR hint~|~%  ~Y01~%did ~
                                   not evaluate to a list of clauses, but ~
                                   instead to~|~%  ~Y23~%~@4"
                                          term
                                          nil
                                          val
                                          nil
                                          (non-term-list-listp-msg val original-wrld))
                                        nil
                                        state))
                                    (t (mv (msg "The :CLAUSE-PROCESSOR hint~|~%  ~
                                   ~Y01~%evaluated to a list of clauses,~%  ~
                                   ~Y23,~%which however has a call of the ~
                                   following :program mode ~
                                   function~#4~[~/s~]:~|~&4."
                                          term
                                          nil
                                          val
                                          nil
                                          (collect-programs (all-ffn-symbs-lst-lst val nil)
                                            original-wrld))
                                        nil
                                        state))))
                                ((and not-skipped
                                   (forbidden-fns-in-term-list-list val
                                     (access rewrite-constant
                                       (access prove-spec-var pspv :rewrite-constant)
                                       :forbidden-fns))) (mv (msg "The :CLAUSE-PROCESSOR ~
                                 hint~|~%~Y01~%evaluated to a list of ~
                                 clauses~|~%~y2~%that contains a call of the ~
                                 function symbol~#3~[, ~&3, which is~/s ~&3, ~
                                 which are~] forbidden in that context.  See ~
                                 :DOC clause-processor and :DOC ~
                                 set-skip-meta-termp-checks and :DOC ~
                                 well-formedness-guarantee."
                                      term
                                      nil
                                      val
                                      (forbidden-fns-in-term-list-list val
                                        (access rewrite-constant
                                          (access prove-spec-var pspv :rewrite-constant)
                                          :forbidden-fns)))
                                    nil
                                    state))
                                (t (let* ((summary-data (and (cddr stobjs-out)
                                         (null (car (last stobjs-out)))
                                         (car (last result)))) (msg (tilde-@-illegal-summary-data-phrase summary-data
                                          original-wrld)))
                                    (cond (msg (mv (msg "The :CLAUSE-PROCESSOR ~
                                     hint~|~%~Y01~%evaluated to multiple ~
                                     values whose last value, ~X23, is not a ~
                                     valid summary-data record, because ~@4.  ~
                                     See :DOC clause-processor."
                                            term
                                            nil
                                            summary-data
                                            (term-evisc-tuple t state)
                                            msg)
                                          nil
                                          state))
                                      (t (value (cons val summary-data))))))))))))))))))))))

(defun apply-top-hints-clause1
  (temp cl-id cl pspv wrld state step-limit)
  (case (car temp)
    (:use (let ((cases-temp (assoc-eq :cases (access prove-spec-var pspv :hint-settings))))
        (cond ((null cases-temp) (apply-use-hint-clauses temp
              (list cl)
              pspv
              wrld
              state
              step-limit))
          (t (mv-let (signal cases-clauses cases-ttree cases-pspv)
              (apply-cases-hint-clause cases-temp cl pspv wrld)
              (declare (ignore signal))
              (sl-let (signal use-clauses use-ttree use-pspv)
                (apply-use-hint-clauses temp
                  cases-clauses
                  cases-pspv
                  wrld
                  state
                  step-limit)
                (declare (ignore signal))
                (mv step-limit
                  'hit
                  use-clauses
                  (cons-tag-trees use-ttree cases-ttree)
                  use-pspv)))))))
    (:by (cond ((symbolp (cdr temp)) (mv step-limit
            'hit
            nil
            (add-to-tag-tree! :bye (cons (cdr temp) cl) nil)
            pspv))
        (t (let ((lmi-lst (cadr temp)) (thm (remove-guard-holders (caddr temp) wrld))
              (constraint-cl (cadddr temp))
              (sr-limit (car (access rewrite-constant
                    (access prove-spec-var pspv :rewrite-constant)
                    :case-split-limitations)))
              (new-pspv (change prove-spec-var
                  pspv
                  :hint-settings (remove1-equal temp
                    (access prove-spec-var pspv :hint-settings)))))
            (let* ((cl (remove-guard-holders-lst cl wrld)) (cl (remove-equal *nil* cl))
                (easy-winp (cond ((null cl) (equal thm *nil*))
                    ((null (cdr cl)) (equal (car cl) thm))
                    (t (equal thm
                        (implicate (conjoin (dumb-negate-lit-lst (butlast cl 1)))
                          (car (last cl)))))))
                (cl1 (if (and (not easy-winp) (ffnnamep-lst 'implies cl))
                    (expand-some-non-rec-fns-lst '(implies) cl wrld)
                    cl))
                (cl-set (if (not easy-winp)
                    (clausify (disjoin cl1) nil t sr-limit)
                    (list cl1)))
                (thm-cl-set (if easy-winp
                    (list (list thm))
                    (clausify (expand-some-non-rec-fns '(implies) thm wrld)
                      nil
                      t
                      sr-limit)))
                (val (list* (cadr temp) thm-cl-set (cdddr temp)))
                (subsumes (and (not easy-winp)
                    (clause-set-subsumes nil thm-cl-set cl-set)))
                (success (or easy-winp subsumes)))
              (cond (success (sl-let (signal clauses ttree irrel-pspv)
                    (preprocess-clause? constraint-cl
                      nil
                      pspv
                      wrld
                      state
                      step-limit)
                    (declare (ignore irrel-pspv))
                    (cond ((eq signal 'miss) (mv step-limit
                          'hit
                          (conjoin-clause-to-clause-set constraint-cl nil)
                          (add-to-tag-tree! :by val nil)
                          new-pspv))
                      ((or (tag-tree-occur 'hidden-clause t ttree)
                         (and clauses
                           (null (cdr clauses))
                           constraint-cl
                           (null (cdr constraint-cl))
                           (equal (prettyify-clause-simple (car clauses))
                             (car constraint-cl)))) (mv step-limit
                          'hit
                          clauses
                          (add-to-tag-tree! :by val nil)
                          new-pspv))
                      (t (mv step-limit
                          'hit
                          clauses
                          (add-to-tag-tree! :by val
                            (add-to-tag-tree! 'preprocess-ttree ttree nil))
                          new-pspv)))))
                (t (mv step-limit
                    'error
                    (msg "When a :by hint is used to supply a lemma-instance ~
                         for a given goal-spec, the formula denoted by the ~
                         lemma-instance must subsume the goal.  This did not ~
                         happen~@1!  The lemma-instance provided was ~x0, ~
                         which denotes the formula ~p2 (when converted to a ~
                         set of clauses and then printed as a formula).  This ~
                         formula was not found to subsume the goal clause, ~
                         ~p3.~|~%Consider a :use hint instead; see :DOC ~
                         hints."
                      (car lmi-lst)
                      (if (eq subsumes '?)
                        " because our subsumption heuristics were unable ~
                             to decide the question"
                        "")
                      (untranslate thm t wrld)
                      (prettyify-clause-set cl-set (let*-abstractionp state) wrld))
                    nil
                    nil))))))))
    (:cases (prepend-step-limit 4
        (apply-cases-hint-clause temp cl pspv wrld)))
    (:bdd (prepend-step-limit 4
        (bdd-clause (cdr temp)
          cl-id
          cl
          (change prove-spec-var
            pspv
            :hint-settings (remove1-equal temp
              (access prove-spec-var pspv :hint-settings)))
          wrld
          state)))
    (t (mv step-limit
        (er hard
          'apply-top-hints-clause
          "Implementation error: Missing case in apply-top-hints-clause.")
        nil
        nil
        nil))))

(defun tilde-@-lmi-phrase
  (lmi-lst k event-names)
  (let* ((seeds (lmi-seed-lst lmi-lst)) (lemma-names (lmi-seeds-info 'hint-events seeds))
      (thms (lmi-seeds-info nil seeds))
      (techs (lmi-techs-lst lmi-lst)))
    (cond ((null techs) (cond ((null thms) (msg "can be obtained from ~&0" lemma-names))
          ((null lemma-names) (msg "can be obtained from the ~
                        ~#0~[~/constraint~/~n1 constraints~] generated"
              (zero-one-or-more k)
              k))
          (t (msg "can be obtained from ~&0 and the ~
                          ~#1~[~/constraint~/~n2 constraints~] ~
                          generated"
              lemma-names
              (zero-one-or-more k)
              k))))
      ((null event-names) (msg "can be derived from ~&0 via ~*1~#2~[~/, provided we can ~
                 establish the constraint generated~/, provided we can ~
                 establish the ~n3 constraints generated~]"
          seeds
          (list "" "~@*" "~@* and " "~@*, " techs)
          (zero-one-or-more k)
          k))
      (t (msg "can be derived from ~&0 via ~*1, bypassing constraints that ~
                 have been proved when processing ~#2~[events ~
                 including ~/previous events~/the event~#3~[~/s~]~ ~
                 ~]~&3~#4~[~/, provided we can establish the constraint ~
                 generated~/, provided we can establish the ~n5 constraints ~
                 generated~]"
          seeds
          (list "" "~@*" "~@* and " "~@*, " techs)
          (if (member 0 event-names)
            (if (cdr event-names)
              0
              1)
            2)
          (if (member 0 event-names)
            (remove 0 event-names)
            event-names)
          (zero-one-or-more k)
          k)))))

(defun or-hit-msg
  (gag-mode-only-p cl-id ttree)
  (let* ((val (tagged-object :or ttree)) (branch-cnt (length (nth 2 val))))
    (msg "The :OR hint for ~@0 gives rise to ~n1 disjunctive ~
          ~#2~[~/branch~/branches~].  Proving any one of these branches would ~
          suffice to prove ~@0.  We explore them in turn~#3~[~@4~/~].~%"
      (tilde-@-clause-id-phrase cl-id)
      branch-cnt
      (zero-one-or-more branch-cnt)
      (if gag-mode-only-p
        1
        0)
      ", describing their derivations as we go")))

(defun apply-top-hints-clause-msg1
  (signal cl-id clauses speciousp ttree pspv state)
  (cond ((tagged-objectsp :bye ttree) (fms "But we have been asked to pretend that this goal is ~
               subsumed by the yet-to-be-proved ~x0.~|"
        (list (cons #\0 (car (tagged-object :bye ttree))))
        (proofs-co state)
        state
        nil))
    ((tagged-objectsp :by ttree) (let* ((obj (tagged-object :by ttree)) (lmi-lst (car obj))
          (thm-cl-set (cadr obj))
          (k (car (cdddr obj)))
          (event-names (cadr (cdddr obj)))
          (ttree (tagged-object 'preprocess-ttree ttree)))
        (fms "~#0~[But, as~/As~/As~] indicated by the hint, this goal is ~
                 subsumed by ~x1, which ~@2.~#3~[~/  By ~*4 we reduce the ~
                 ~#5~[constraint~/~n6 constraints~] to ~#0~[T~/the following ~
                 conjecture~/the following ~n7 conjectures~].~]~|"
          (list (cons #\0 (zero-one-or-more clauses))
            (cons #\1
              (prettyify-clause-set thm-cl-set
                (let*-abstractionp state)
                (w state)))
            (cons #\2 (tilde-@-lmi-phrase lmi-lst k event-names))
            (cons #\3
              (if (int= k 0)
                0
                1))
            (cons #\4 (tilde-*-preprocess-phrase ttree))
            (cons #\5
              (if (int= k 1)
                0
                1))
            (cons #\6 k)
            (cons #\7 (length clauses)))
          (proofs-co state)
          state
          (term-evisc-tuple nil state))))
    ((tagged-objectsp :use ttree) (let* ((use-obj (tagged-object :use ttree)) (lmi-lst (car (car use-obj)))
          (hyps (cadr (car use-obj)))
          (k (car (cdddr (car use-obj))))
          (event-names (cadr (cdddr (car use-obj))))
          (preprocess-ttree (tagged-object 'preprocess-ttree ttree))
          (len-g (len clauses))
          (len-c k)
          (cases-obj (tagged-object :cases ttree)))
        (fms "~#0~[But we~/We~] ~#x~[split the goal into the cases specified ~
             by the :CASES hint and augment each case~/augment the goal~] ~
             with the ~#1~[hypothesis~/hypotheses~] provided by the :USE ~
             hint. ~#1~[The hypothesis~/These hypotheses~] ~@2~#3~[~/; the ~
             constraint~#4~[~/s~] can be simplified using ~*5~].  ~#6~[This ~
             reduces the goal to T.~/We are left with the following ~
             subgoal.~/We are left with the following ~n7 subgoals.~]~%"
          (list (cons #\x
              (if cases-obj
                0
                1))
            (cons #\0
              (if (> len-g 0)
                1
                0))
            (cons #\1 hyps)
            (cons #\2 (tilde-@-lmi-phrase lmi-lst k event-names))
            (cons #\3
              (if (> len-c 0)
                1
                0))
            (cons #\4
              (if (> len-c 1)
                1
                0))
            (cons #\5 (tilde-*-preprocess-phrase preprocess-ttree))
            (cons #\6
              (if (equal len-g 0)
                0
                (if (equal len-g 1)
                  1
                  2)))
            (cons #\7 len-g))
          (proofs-co state)
          state
          (term-evisc-tuple nil state))))
    ((tagged-objectsp :cases ttree) (let* ((cases-obj (tagged-object :cases ttree)) (new-clauses (cdr cases-obj)))
        (cond (new-clauses (fms "We now split the goal into the cases specified by ~
                   the :CASES hint to produce ~n0 new non-trivial ~
                   subgoal~#1~[~/s~].~|"
              (list (cons #\0 (length new-clauses))
                (cons #\1
                  (if (cdr new-clauses)
                    1
                    0)))
              (proofs-co state)
              state
              (term-evisc-tuple nil state)))
          (t (fms "But the resulting goals are all true by case reasoning."
              nil
              (proofs-co state)
              state
              nil)))))
    ((eq signal 'or-hit) (fms "~@0"
        (list (cons #\0 (or-hit-msg nil cl-id ttree)))
        (proofs-co state)
        state
        nil))
    ((tagged-objectsp 'hidden-clause ttree) state)
    ((tagged-objectsp :clause-processor ttree) (let* ((clause-processor-obj (tagged-object :clause-processor ttree)) (verified-p-msg (cond ((access clause-processor-hint
                 (car clause-processor-obj)
                 :verified-p) "verified")
              (t "trusted")))
          (new-clauses (cddr clause-processor-obj))
          (cl-proc-fn (ffn-symb (access clause-processor-hint
                (car clause-processor-obj)
                :term))))
        (cond (new-clauses (fms "We now apply the ~@0 :CLAUSE-PROCESSOR function ~x1 to ~
                   produce ~n2 new subgoal~#3~[~/s~].~|"
              (list (cons #\0 verified-p-msg)
                (cons #\1 cl-proc-fn)
                (cons #\2 (length new-clauses))
                (cons #\3
                  (if (cdr new-clauses)
                    1
                    0)))
              (proofs-co state)
              state
              (term-evisc-tuple nil state)))
          (t (fms "But the ~@0 :CLAUSE-PROCESSOR function ~x1 replaces this goal ~
                   by T.~|"
              (list (cons #\0 verified-p-msg) (cons #\1 cl-proc-fn))
              (proofs-co state)
              state
              nil)))))
    (t (simplify-clause-msg1 signal
        cl-id
        clauses
        speciousp
        ttree
        pspv
        state))))

(defun previous-process-was-speciousp
  (hist)
  (cond ((null hist) nil)
    ((null (cdr hist)) nil)
    ((consp (access history-entry (cadr hist) :processor)) t)
    ((and (eq (access history-entry (cadr hist) :processor)
         'settled-down-clause)
       (consp (cddr hist))
       (consp (access history-entry (caddr hist) :processor))) t)
    (t nil)))

(defun rune-names-from-assumptions-1
  (assumnotes names)
  (cond ((endp assumnotes) names)
    (t (rune-names-from-assumptions-1 (cdr assumnotes)
        (let* ((rune (access assumnote (car assumnotes) :rune)) (name (and (consp rune) (base-symbol rune))))
          (cond ((and (consp rune) name (not (member-eq name names))) (cons name names))
            (t names)))))))

(defun rune-names-from-assumptions
  (assumptions names)
  (cond ((endp assumptions) names)
    (t (rune-names-from-assumptions (cdr assumptions)
        (rune-names-from-assumptions-1 (access assumption (car assumptions) :assumnotes)
          names)))))

(defun waterfall-update-gag-state
  (cl-id clause proc signal ttree pspv state)
  (let* ((msg-p (not (output-ignored-p 'prove state))) (gagst0 (access prove-spec-var pspv :gag-state))
      (pool-lst (access clause-id cl-id :pool-lst))
      (forcing-round (access clause-id cl-id :forcing-round))
      (stack (cond (pool-lst (access gag-state gagst0 :sub-stack))
          (t (access gag-state gagst0 :top-stack))))
      (active-cl-id (access gag-state gagst0 :active-cl-id))
      (abort-p (eq signal 'abort))
      (push-or-bye-p (or (eq proc 'push-clause)
          (and (eq proc 'apply-top-hints-clause)
            (eq signal 'hit)
            (tagged-objectsp :bye ttree))))
      (new-active-p (and (null active-cl-id)
          (null (cdr pool-lst))
          (or push-or-bye-p
            (member-eq proc (f-get-global 'checkpoint-processors state)))))
      (new-frame (and new-active-p
          (make gag-info :clause-id cl-id :clause clause :pushed nil)))
      (new-stack (cond (new-active-p (cons new-frame stack)) (t stack)))
      (gagst (cond (new-active-p (cond (pool-lst (change gag-state
                  gagst0
                  :sub-stack new-stack
                  :active-cl-id cl-id))
              (t (change gag-state
                  gagst0
                  :top-stack new-stack
                  :active-cl-id cl-id))))
          (t gagst0)))
      (new-forcep (and (not abort-p)
          (not (access gag-state gagst :forcep))
          (tagged-objectsp 'assumption ttree)))
      (gagst (cond (new-forcep (change gag-state gagst :forcep t))
          (t gagst)))
      (forcep-msg (and new-forcep
          msg-p
          (let ((names (rune-names-from-assumptions (tagged-objects 'assumption ttree)
                 nil)))
            (msg "Forcing Round ~x0 is pending (caused first ~
                                  by ~#1~[~/applying ~&2 to ~]~@3)."
              (1+ (access clause-id cl-id :forcing-round))
              (if names
                1
                0)
              names
              (tilde-@-clause-id-phrase cl-id))))))
    (cond (push-or-bye-p (let* ((top-ci (assert$ (consp new-stack) (car new-stack))) (old-pushed (access gag-info top-ci :pushed))
            (top-goal-p (equal cl-id *initial-clause-id*))
            (print-p (not (or (access gag-state gagst :active-printed-p)
                  (cdr pool-lst)
                  top-goal-p)))
            (gagst (cond (print-p (change gag-state gagst :active-printed-p t))
                (t gagst)))
            (top-stack (access gag-state gagst0 :top-stack))
            (msg0 (cond ((and print-p msg-p) (assert$ (null old-pushed)
                    (msg "~@0~|~%~@1~|~Q23~|~%"
                      (gag-start-msg (and pool-lst
                          (assert$ (consp top-stack)
                            (access gag-info (car top-stack) :clause-id)))
                        (and pool-lst
                          (tilde-@-pool-name-phrase forcing-round pool-lst)))
                      (tilde-@-clause-id-phrase (access gag-info top-ci :clause-id))
                      (prettyify-clause (access gag-info top-ci :clause)
                        (let*-abstractionp state)
                        (w state))
                      (term-evisc-tuple nil state))))
                (t nil))))
          (cond (abort-p (mv (cond ((equal (tagged-objects 'abort-cause ttree) '(revert)) (change gag-state gagst :abort-info new-stack))
                  ((equal (tagged-objects 'abort-cause ttree) '(empty-clause)) (update-gag-info-for-abort 'empty-clause gagst))
                  ((member-equal (tagged-objects 'abort-cause ttree)
                     '((do-not-induct) (do-not-induct-otf-flg-override))) (update-gag-info-for-abort 'do-not-induct gagst))
                  ((equal (tagged-objects 'abort-cause ttree)
                     '(induction-depth-limit-exceeded)) (update-gag-info-for-abort 'induction-depth-limit-exceeded
                      gagst))
                  (t gagst))
                (and msg-p
                  (msg "~@0~@1"
                    (or msg0 "")
                    (push-clause-msg1-abort cl-id ttree pspv state)))))
            (t (let* ((old-pspv-pool-lst (pool-lst (cdr (access prove-spec-var pspv :pool)))) (newer-stack (and (assert$ (or (cdr pool-lst)
                          (equal (access gag-state gagst :active-cl-id)
                            (access gag-info top-ci :clause-id)))
                        (if (eq proc 'push-clause)
                          (cons (change gag-info
                              top-ci
                              :pushed (cons (cons cl-id old-pspv-pool-lst) old-pushed))
                            (cdr new-stack))
                          new-stack)))))
                (mv (cond (pool-lst (change gag-state gagst :sub-stack newer-stack))
                    (t (change gag-state gagst :top-stack newer-stack)))
                  (and msg-p
                    (or msg0 forcep-msg (gag-mode))
                    (msg "~@0~#1~[~@2~|~%~/~]~@3"
                      (or msg0 "")
                      (if forcep-msg
                        0
                        1)
                      forcep-msg
                      (cond ((null (gag-mode)) "")
                        (t (let ((msg-finish (cond ((or pool-lst (null active-cl-id)) ".")
                                 (t (msg ":~|~Q01."
                                     (prettyify-clause clause
                                       (let*-abstractionp state)
                                       (w state))
                                     (term-evisc-tuple nil state))))))
                            (cond ((eq proc 'push-clause) (msg "~@0 (~@1) is pushed for proof by ~
                                    induction~@2"
                                  (tilde-@-pool-name-phrase forcing-round old-pspv-pool-lst)
                                  (if top-goal-p
                                    "the initial Goal, a key checkpoint"
                                    (tilde-@-clause-id-phrase cl-id))
                                  msg-finish))
                              (t (msg "~@0 is subsumed by a goal yet to be ~
                                    proved~@1"
                                  (tilde-@-clause-id-phrase cl-id)
                                  msg-finish))))))))))))))
      (t (assert$ (not abort-p)
          (mv (cond ((or new-active-p new-forcep) gagst) (t nil))
            forcep-msg))))))

(defun remove-pool-lst-from-gag-state
  (pool-lst gag-state state)
  (declare (ignore state))
  (cond (t (let* ((sub-stack (access gag-state gag-state :sub-stack)) (stack (or sub-stack (access gag-state gag-state :top-stack))))
        (assert$ (consp stack)
          (let* ((ci (car stack)) (pushed (access gag-info ci :pushed))
              (pop-car-p (null (cdr pushed))))
            (assert$ (and (consp pushed)
                (equal (cdar pushed) pool-lst)
                (not (access gag-state gag-state :active-cl-id)))
              (let ((new-stack (if pop-car-p
                     (cdr stack)
                     (cons (change gag-info ci :pushed (cdr pushed)) (cdr stack)))))
                (mv (cond (sub-stack (change gag-state gag-state :sub-stack new-stack))
                    (t (change gag-state gag-state :top-stack new-stack)))
                  (and pop-car-p (access gag-info ci :clause-id)))))))))))

(defun pop-clause-update-gag-state-pop
  (pool-lsts gag-state msgs msg-p state)
  (cond ((endp pool-lsts) (mv gag-state msgs))
    (t (mv-let (gag-state msgs)
        (pop-clause-update-gag-state-pop (cdr pool-lsts)
          gag-state
          msgs
          msg-p
          state)
        (mv-let (gagst cl-id)
          (remove-pool-lst-from-gag-state (car pool-lsts)
            gag-state
            state)
          (mv gagst
            (if (and msg-p cl-id)
              (cons (msg "~@0" (tilde-@-clause-id-phrase cl-id)) msgs)
              msgs)))))))

(defun gag-mode-jppl-flg
  (gag-state)
  (let ((stack (or (access gag-state gag-state :sub-stack)
         (access gag-state gag-state :top-stack))))
    (cond (stack (let* ((pushed (access gag-info (car stack) :pushed)) (pool-lst (and pushed (cdar pushed))))
          (and (null (cdr pool-lst)) pool-lst)))
      (t nil))))

(defun waterfall-msg1
  (processor cl-id
    signal
    clauses
    new-hist
    msg
    ttree
    pspv
    state)
  (with-output-lock (let ((gag-mode (gag-mode)))
      (pprogn (cond ((and msg gag-mode) (fms "~@0~|"
              (list (cons #\0 msg))
              (proofs-co state)
              state
              nil))
          (t state))
        (cond ((or gag-mode (f-get-global 'raw-proof-format state)) (print-splitter-rules-summary cl-id clauses ttree state))
          (t state))
        (cond (gag-mode state)
          (t (case processor
              (apply-top-hints-clause (apply-top-hints-clause-msg1 signal
                  cl-id
                  clauses
                  (consp (access history-entry (car new-hist) :processor))
                  ttree
                  pspv
                  state))
              (preprocess-clause (preprocess-clause-msg1 signal clauses ttree pspv state))
              (simplify-clause (simplify-clause-msg1 signal
                  cl-id
                  clauses
                  (consp (access history-entry (car new-hist) :processor))
                  ttree
                  pspv
                  state))
              (settled-down-clause (settled-down-clause-msg1 signal clauses ttree pspv state))
              (eliminate-destructors-clause (eliminate-destructors-clause-msg1 signal
                  clauses
                  ttree
                  pspv
                  state))
              (fertilize-clause (fertilize-clause-msg1 signal clauses ttree pspv state))
              (generalize-clause (generalize-clause-msg1 signal clauses ttree pspv state))
              (eliminate-irrelevance-clause (eliminate-irrelevance-clause-msg1 signal
                  clauses
                  ttree
                  pspv
                  state))
              (otherwise (push-clause-msg1 cl-id signal clauses ttree pspv state)))))))))

(defun waterfall-print-clause-body
  (cl-id clause state)
  (with-output-lock (pprogn (increment-timer 'prove-time state)
      (fms "~@0~|~q1.~|"
        (list (cons #\0 (tilde-@-clause-id-phrase cl-id))
          (cons #\1
            (if (eq (f-get-global 'raw-proof-format state) :clause)
              clause
              (prettyify-clause clause
                (let*-abstractionp state)
                (w state)))))
        (proofs-co state)
        state
        (term-evisc-tuple nil state))
      (increment-timer 'print-time state))))

(defun print-clause-id-okp-builtin
  (cl-id)
  (declare (ignore cl-id)
    (xargs :guard (clause-id-p cl-id)))
  t)

(defun put-ttree-into-pspv
  (ttree pspv)
  (change prove-spec-var
    pspv
    :tag-tree (cons-tag-trees ttree
      (access prove-spec-var pspv :tag-tree))))

(defun set-cl-ids-of-assumptions1
  (recs cl-id)
  (cond ((endp recs) nil)
    (t (cons (change assumption
          (car recs)
          :assumnotes (list (change assumnote
              (car (access assumption (car recs) :assumnotes))
              :cl-id cl-id)))
        (set-cl-ids-of-assumptions1 (cdr recs) cl-id)))))

(defun set-cl-ids-of-assumptions
  (ttree cl-id)
  (let ((recs (tagged-objects 'assumption ttree)))
    (cond (recs (extend-tag-tree 'assumption
          (set-cl-ids-of-assumptions1 recs cl-id)
          (remove-tag-from-tag-tree! 'assumption ttree)))
      (t ttree))))

(defun collect-assumptions1
  (recs only-immediatep ans)
  (cond ((endp recs) ans)
    (t (collect-assumptions1 (cdr recs)
        only-immediatep
        (cond ((cond ((eq only-immediatep 'non-nil) (access assumption (car recs) :immediatep))
             ((eq only-immediatep 'case-split) (eq (access assumption (car recs) :immediatep) 'case-split))
             ((eq only-immediatep t) (eq (access assumption (car recs) :immediatep) t))
             (t t)) (add-to-set-equal (car recs) ans))
          (t ans))))))

(defun collect-assumptions
  (ttree only-immediatep)
  (collect-assumptions1 (tagged-objects 'assumption ttree)
    only-immediatep
    nil))

(defun linked-variables1
  (vars direct-links changedp direct-links0)
  (cond ((null direct-links) (cond (changedp (linked-variables1 vars direct-links0 nil direct-links0))
        (t vars)))
    ((and (intersectp-eq (car direct-links) vars)
       (not (subsetp-eq (car direct-links) vars))) (linked-variables1 (union-eq (car direct-links) vars)
        (cdr direct-links)
        t
        direct-links0))
    (t (linked-variables1 vars
        (cdr direct-links)
        changedp
        direct-links0))))

(defun linked-variables
  (vars direct-links)
  (linked-variables1 vars direct-links nil direct-links))

(defun disvar-type-alist1
  (vars type-alist wrld)
  (cond ((null type-alist) nil)
    ((or (intersectp-eq vars (all-vars (caar type-alist)))
       (contains-constrained-constantp (caar type-alist) wrld)) (cons (car type-alist)
        (disvar-type-alist1 vars (cdr type-alist) wrld)))
    (t (disvar-type-alist1 vars (cdr type-alist) wrld))))

(defun collect-all-vars
  (lst)
  (cond ((null lst) nil)
    (t (cons (all-vars (car lst)) (collect-all-vars (cdr lst))))))

(defun disvar-type-alist
  (type-alist term wrld)
  (let* ((vars (all-vars term)) (direct-links (collect-all-vars (strip-cars type-alist)))
      (vars* (linked-variables vars direct-links)))
    (disvar-type-alist1 vars* type-alist wrld)))

(defun unencumber-type-alist
  (type-alist term rewrittenp wrld)
  (declare (ignore rewrittenp))
  (disvar-type-alist type-alist term wrld))

(defun unencumber-assumption
  (assn wrld)
  (declare (ignore wrld))
  assn)

(defun unencumber-assumptions
  (assumptions wrld ans)
  (cond ((null assumptions) ans)
    (t (unencumber-assumptions (cdr assumptions)
        wrld
        (cons (unencumber-assumption (car assumptions) wrld) ans)))))

(defun dumb-type-alist-implicationp1
  (type-alist1 type-alist2 seen)
  (cond ((null type-alist1) t)
    ((member-equal (caar type-alist1) seen) (dumb-type-alist-implicationp1 (cdr type-alist1)
        type-alist2
        seen))
    (t (let ((ts1 (cadar type-alist1)) (ts2 (or (cadr (assoc-equal (caar type-alist1) type-alist2))
              *ts-unknown*)))
        (and (ts-subsetp ts1 ts2)
          (dumb-type-alist-implicationp1 (cdr type-alist1)
            type-alist2
            (cons (caar type-alist1) seen)))))))

(defun dumb-type-alist-implicationp2
  (type-alist1 type-alist2)
  (cond ((null type-alist2) t)
    (t (and (assoc-equal (caar type-alist2) type-alist1)
        (dumb-type-alist-implicationp2 type-alist1
          (cdr type-alist2))))))

(defun dumb-type-alist-implicationp
  (type-alist1 type-alist2)
  (and (dumb-type-alist-implicationp1 type-alist1 type-alist2 nil)
    (dumb-type-alist-implicationp2 type-alist1 type-alist2)))

(defun partition-according-to-assumption-term
  (assumptions alist)
  (cond ((null assumptions) alist)
    (t (partition-according-to-assumption-term (cdr assumptions)
        (put-assoc-equal (access assumption (car assumptions) :term)
          (cons (car assumptions)
            (cdr (assoc-equal (access assumption (car assumptions) :term)
                alist)))
          alist)))))

(defun exists-assumption-with-weaker-type-alist
  (assumption assumptions i)
  (cond ((null assumptions) (mv nil nil))
    ((dumb-type-alist-implicationp (access assumption assumption :type-alist)
       (access assumption (car assumptions) :type-alist)) (mv i (car assumptions)))
    (t (exists-assumption-with-weaker-type-alist assumption
        (cdr assumptions)
        (1+ i)))))

(defun add-assumption-with-weak-type-alist
  (assumption assumptions ans)
  (cond ((null assumptions) (cons assumption ans))
    ((dumb-type-alist-implicationp (access assumption (car assumptions) :type-alist)
       (access assumption assumption :type-alist)) (add-assumption-with-weak-type-alist (change assumption
          assumption
          :assumnotes (union-equal (access assumption assumption :assumnotes)
            (access assumption (car assumptions) :assumnotes)))
        (cdr assumptions)
        ans))
    (t (add-assumption-with-weak-type-alist assumption
        (cdr assumptions)
        (cons (car assumptions) ans)))))

(defun dumb-keep-assumptions-with-weakest-type-alists
  (assumptions kept)
  (cond ((null assumptions) kept)
    (t (mv-let (i assn)
        (exists-assumption-with-weaker-type-alist (car assumptions)
          kept
          0)
        (cond (i (dumb-keep-assumptions-with-weakest-type-alists (cdr assumptions)
              (update-nth i
                (change assumption
                  assn
                  :assumnotes (union-equal (access assumption (car assumptions) :assumnotes)
                    (access assumption assn :assumnotes)))
                kept)))
          (t (dumb-keep-assumptions-with-weakest-type-alists (cdr assumptions)
              (add-assumption-with-weak-type-alist (car assumptions)
                kept
                nil))))))))

(defun dumb-assumption-subsumption1
  (partitions ans)
  (cond ((null partitions) ans)
    (t (dumb-assumption-subsumption1 (cdr partitions)
        (append (dumb-keep-assumptions-with-weakest-type-alists (cdr (car partitions))
            nil)
          ans)))))

(defun dumb-assumption-subsumption
  (assumptions)
  (dumb-assumption-subsumption1 (partition-according-to-assumption-term assumptions nil)
    nil))

(defun clausify-type-alist
  (type-alist cl ens w seen ttree)
  (cond ((null type-alist) (mv cl ttree))
    ((member-equal (caar type-alist) seen) (clausify-type-alist (cdr type-alist) cl ens w seen ttree))
    (t (mv-let (term ttree)
        (convert-type-set-to-term1 (caar type-alist)
          (cadar type-alist)
          t
          ens
          w
          ttree)
        (clausify-type-alist (cdr type-alist)
          (cons (dumb-negate-lit term) cl)
          ens
          w
          (cons (caar type-alist) seen)
          ttree)))))

(defun clausify-assumption
  (assumption ens wrld)
  (clausify-type-alist (access assumption assumption :type-alist)
    (list (access assumption assumption :term))
    ens
    wrld
    nil
    nil))

(defun clausify-assumptions
  (assumptions ens wrld pairs ttree)
  (cond ((null assumptions) (mv pairs ttree))
    (t (mv-let (clause ttree1)
        (clausify-assumption (car assumptions) ens wrld)
        (clausify-assumptions (cdr assumptions)
          ens
          wrld
          (cons (cons (access assumption (car assumptions) :assumnotes)
              clause)
            pairs)
          (cons-tag-trees ttree1 ttree))))))

(defun strip-assumption-terms
  (lst)
  (cond ((endp lst) nil)
    (t (add-to-set-equal (access assumption (car lst) :term)
        (strip-assumption-terms (cdr lst))))))

(defun add-splitters-to-ttree1
  (assumnotes tag ttree)
  (cond ((endp assumnotes) ttree)
    (t (add-splitters-to-ttree1 (cdr assumnotes)
        tag
        (add-to-tag-tree tag
          (access assumnote (car assumnotes) :rune)
          ttree)))))

(defun add-splitters-to-ttree
  (immediatep tag assumptions ttree)
  (cond ((endp assumptions) ttree)
    (t (add-splitters-to-ttree immediatep
        tag
        (cdr assumptions)
        (cond ((eq immediatep
             (access assumption (car assumptions) :immediatep)) (add-splitters-to-ttree1 (access assumption (car assumptions) :assumnotes)
              tag
              ttree))
          (t ttree))))))

(defun maybe-add-splitters-to-ttree
  (splitter-output immediatep tag assumptions ttree)
  (cond (splitter-output (add-splitters-to-ttree immediatep tag assumptions ttree))
    (t ttree)))

(defun extract-and-clausify-assumptions
  (cl ttree only-immediatep ens wrld splitter-output)
  (cond ((eq only-immediatep nil) (let* ((raw-assumptions (collect-assumptions ttree only-immediatep)) (cleaned-assumptions (dumb-assumption-subsumption (unencumber-assumptions raw-assumptions wrld nil))))
        (mv-let (pairs ttree1)
          (clausify-assumptions cleaned-assumptions ens wrld nil nil)
          (mv (length raw-assumptions)
            cleaned-assumptions
            pairs
            (cons-tag-trees (cond ((tagged-objectsp 'assumption ttree1) (er hard
                    'extract-and-clausify-assumptions
                    "Convert-type-set-to-term apparently returned a ttree that ~
                    contained an 'assumption tag.  This violates the ~
                    assumption in this function."))
                (t ttree1))
              (delete-assumptions ttree only-immediatep))))))
    ((eq only-immediatep 'non-nil) (let* ((case-split-assumptions (collect-assumptions ttree 'case-split)) (assumed-terms (strip-assumption-terms case-split-assumptions))
          (case-split-clauses (split-on-assumptions assumed-terms cl nil))
          (case-split-pairs (pairlis2 nil case-split-clauses))
          (raw-assumptions (collect-assumptions ttree t))
          (cleaned-assumptions (dumb-assumption-subsumption (unencumber-assumptions raw-assumptions wrld nil))))
        (mv-let (pairs ttree1)
          (clausify-assumptions cleaned-assumptions ens wrld nil nil)
          (mv 'ignored
            assumed-terms
            (append case-split-pairs pairs)
            (maybe-add-splitters-to-ttree splitter-output
              'case-split
              'splitter-case-split
              case-split-assumptions
              (maybe-add-splitters-to-ttree splitter-output
                t
                'splitter-immed-forced
                raw-assumptions
                (cons-tag-trees (cond ((tagged-objectsp 'assumption ttree1) (er hard
                        'extract-and-clausify-assumptions
                        "Convert-type-set-to-term apparently returned a ttree ~
                     that contained an 'assumption tag.  This violates the ~
                     assumption in this function."))
                    (t ttree1))
                  (delete-assumptions ttree 'non-nil))))))))
    (t (mv 0
        nil
        (er hard
          'extract-and-clausify-assumptions
          "We only implemented two cases for only-immediatep:  'non-nil ~
               and nil.  But you now call it on ~p0."
          only-immediatep)
        nil))))

(defun set-rw-cache-state-in-pspv
  (pspv val)
  (declare (xargs :guard (member-eq val *legal-rw-cache-states*)))
  (change prove-spec-var
    pspv
    :rewrite-constant (change rewrite-constant
      (access prove-spec-var pspv :rewrite-constant)
      :rw-cache-state val)))

(defun maybe-set-rw-cache-state-disabled
  (pspv)
  (cond ((eq (access rewrite-constant
         (access prove-spec-var pspv :rewrite-constant)
         :rw-cache-state)
       t) (set-rw-cache-state-in-pspv pspv :disabled))
    (t pspv)))

(defun maybe-set-rw-cache-state-enabled
  (pspv)
  (cond ((eq (access rewrite-constant
         (access prove-spec-var pspv :rewrite-constant)
         :rw-cache-state)
       :disabled) (set-rw-cache-state-in-pspv pspv t))
    (t pspv)))

(defun accumulate-rw-cache-into-pspv
  (processor ttree pspv)
  (cond ((and (eq processor 'simplify-clause)
       ttree
       (eq (access rewrite-constant
           (access prove-spec-var pspv :rewrite-constant)
           :rw-cache-state)
         t)) (let ((new-ttree-or-nil (accumulate-rw-cache? nil
             ttree
             (access prove-spec-var pspv :tag-tree))))
        (cond (new-ttree-or-nil (change prove-spec-var pspv :tag-tree new-ttree-or-nil))
          (t pspv))))
    (t pspv)))

(defun erase-rw-cache-from-pspv
  (pspv)
  (let ((ttree (access prove-spec-var pspv :tag-tree)))
    (cond ((tagged-objectsp 'rw-cache-any-tag ttree) (change prove-spec-var
          pspv
          :tag-tree (remove-tag-from-tag-tree 'rw-cache-nil-tag
            (remove-tag-from-tag-tree! 'rw-cache-any-tag ttree))))
      ((tagged-objectsp 'rw-cache-nil-tag ttree) (change prove-spec-var
          pspv
          :tag-tree (remove-tag-from-tag-tree! 'rw-cache-nil-tag ttree)))
      (t pspv))))

(defun too-many-proc-cl-occurrences1
  (proc cl hist cnt)
  (cond ((endp hist) nil)
    ((and (eq proc (access history-entry (car hist) :processor))
       (equal cl (access history-entry (car hist) :clause))) (if (= cnt 0)
        t
        (too-many-proc-cl-occurrences1 proc cl (cdr hist) (- cnt 1))))
    (t (too-many-proc-cl-occurrences1 proc cl (cdr hist) cnt))))

(defun too-many-proc-cl-occurrences
  (proc cl hist cnt)
  (cond ((or (eq proc 'apply-top-hints-clause)
       (eq proc 'preprocess-clause)
       (eq proc 'settled-down-clause)
       (eq proc 'fertilize-clause)) nil)
    (t (too-many-proc-cl-occurrences1 proc cl hist cnt))))

(defun waterfall-loop-detector
  (subgoal-loop-limits history)
  (cond ((null (car subgoal-loop-limits)) (cond ((null (cdr subgoal-loop-limits)) nil)
        ((too-many-proc-cl-occurrences (access history-entry (car history) :processor)
           (access history-entry (car history) :clause)
           history
           (cdr subgoal-loop-limits)) (cdr subgoal-loop-limits))
        (t nil)))
    ((length-exceedsp history (car subgoal-loop-limits)) t)
    ((null (cdr subgoal-loop-limits)) nil)
    ((too-many-proc-cl-occurrences (access history-entry (car history) :processor)
       (access history-entry (car history) :clause)
       history
       (cdr subgoal-loop-limits)) (cdr subgoal-loop-limits))
    (t nil)))

(defun collect-proc-cl-clause-id-strings
  (proc cl hist cnt ans)
  (cond ((endp hist) ans)
    ((and (eq proc (access history-entry (car hist) :processor))
       (equal cl (access history-entry (car hist) :clause))) (let ((new-ans (cons (string-for-tilde-@-clause-id-phrase (access history-entry (car hist) :cl-id))
             ans)))
        (if (= cnt 0)
          new-ans
          (collect-proc-cl-clause-id-strings proc
            cl
            (cdr hist)
            (- cnt 1)
            new-ans))))
    (t (collect-proc-cl-clause-id-strings proc
        cl
        (cdr hist)
        cnt
        ans))))

(defun helpful-subgoal-loop-data1
  (proc cl hist cnt runes goal2 ans)
  (cond ((endp hist) ans)
    ((and (eq proc (access history-entry (car hist) :processor))
       (equal cl (access history-entry (car hist) :clause))) (let* ((goal1 (string-for-tilde-@-clause-id-phrase (access history-entry (car hist) :cl-id))) (new-ans (cons (list goal1 (merge-sort-runes runes) goal2) ans)))
        (if (= cnt 0)
          new-ans
          (helpful-subgoal-loop-data1 proc
            cl
            (cdr hist)
            (- cnt 1)
            (all-runes-in-ttree (access history-entry (car hist) :ttree)
              nil)
            goal1
            new-ans))))
    (t (helpful-subgoal-loop-data1 proc
        cl
        (cdr hist)
        cnt
        (all-runes-in-ttree (access history-entry (car hist) :ttree)
          runes)
        goal2
        ans))))

(defun helpful-subgoal-loop-data
  (hist cnt)
  (helpful-subgoal-loop-data1 (access history-entry (car hist) :processor)
    (access history-entry (car hist) :clause)
    (cdr hist)
    cnt
    (all-runes-in-ttree (access history-entry (car hist) :ttree)
      nil)
    (string-for-tilde-@-clause-id-phrase (access history-entry (car hist) :cl-id))
    nil))

(defun lmi-name-or-rune
  (lmi)
  (cond ((atom lmi) lmi)
    ((member-eq (car lmi)
       '(:theorem :termination-theorem :termination-theorem! :guard-theorem :functional-instance)) nil)
    ((eq (car lmi) :instance) (lmi-name-or-rune (cadr lmi)))
    (t lmi)))

(defun enabled-lmi-names1
  (ens pairs)
  (cond ((null pairs) nil)
    ((and (or (eq (cadr (car pairs)) :definition)
         (eq (cadr (car pairs)) :rewrite))
       (enabled-numep (car (car pairs)) ens)) (add-to-set-equal (cdr (car pairs))
        (enabled-lmi-names1 ens (cdr pairs))))
    (t (enabled-lmi-names1 ens (cdr pairs)))))

(defun enabled-lmi-names
  (ens lmi-lst wrld)
  (cond ((null lmi-lst) nil)
    (t (let ((x (lmi-name-or-rune (car lmi-lst))))
        (cond ((null x) (enabled-lmi-names ens (cdr lmi-lst) wrld))
          ((symbolp x) (union-equal (enabled-lmi-names1 ens
                (getpropc x 'runic-mapping-pairs nil wrld))
              (enabled-lmi-names ens (cdr lmi-lst) wrld)))
          (t (let ((x (if (and (consp x) (eq (car x) :executable-counterpart))
                   (list :definition (cadr x))
                   x)))
              (cond ((enabled-runep x ens wrld) (add-to-set-equal x
                    (enabled-lmi-names ens (cdr lmi-lst) wrld)))
                (t (enabled-lmi-names ens (cdr lmi-lst) wrld))))))))))

(defun waterfall-or-hit-msg-a
  (cl-id user-hinti d-cl-id i branch-cnt state)
  (cond ((gag-mode) state)
    (t (fms "---~%~@0~%( same formula as ~@1 ).~%~%The ~n2 disjunctive branch ~
          (of ~x3) for ~@1 can be created by applying the hint:~%~y4.~%"
        (list (cons #\0 (tilde-@-clause-id-phrase d-cl-id))
          (cons #\1 (tilde-@-clause-id-phrase cl-id))
          (cons #\2 (list i))
          (cons #\3 branch-cnt)
          (cons #\4
            (cons (string-for-tilde-@-clause-id-phrase d-cl-id)
              user-hinti)))
        (proofs-co state)
        state
        nil))))

(defun waterfall-or-hit-msg-b
  (cl-id d-cl-id branch-cnt state)
  (cond ((gag-mode) state)
    (t (fms "---~%~@0 has succeeded!  All of its subgoals have been proved ~
               (modulo any forced assumptions).  Recall that it was one of ~
               ~n1 disjunctive branches generated by the :OR hint to prove ~
               ~@2.   We therefore abandon work on the other branches.~%"
        (list (cons #\0 (tilde-@-clause-id-phrase d-cl-id))
          (cons #\1 branch-cnt)
          (cons #\2 (tilde-@-clause-id-phrase cl-id)))
        (proofs-co state)
        state
        nil))))

(defun tilde-*-or-hit-summary-phrase1
  (summary)
  (cond ((endp summary) nil)
    (t (let ((cl-id (car (car summary))) (subgoals (cadr (car summary)))
          (difficulty (caddr (car summary))))
        (cons (msg "~@0~t1   ~c2   ~c3~%"
            (tilde-@-clause-id-phrase cl-id)
            20
            (cons subgoals 5)
            (cons difficulty 10))
          (tilde-*-or-hit-summary-phrase1 (cdr summary)))))))

(defun tilde-*-or-hit-summary-phrase
  (summary)
  (list ""
    "~@*"
    "~@*"
    "~@*"
    (tilde-*-or-hit-summary-phrase1 summary)))

(defun waterfall-or-hit-msg-c
  (parent-cl-id results revert-d-cl-id cl-id summary state)
  (cond ((null results) (cond (revert-d-cl-id (fms "---~%None of the branches we tried for ~@0 led to a plausible set ~
            of subgoals, and at least one, ~@1, led to the suggestion that we ~
            focus on the original conjecture.  We therefore abandon our ~
            previous work on this conjecture and reassign the name *1 to the ~
            original conjecture.  (See :DOC otf-flg.)~%"
            (list (cons #\0 (tilde-@-clause-id-phrase parent-cl-id))
              (cons #\1 (tilde-@-clause-id-phrase revert-d-cl-id)))
            (proofs-co state)
            state
            nil))
        (t (fms "---~%None of the branches we tried for ~@0 led to a plausible set ~
            of subgoals.  The proof attempt has failed.~|"
            (list (cons #\0 (tilde-@-clause-id-phrase parent-cl-id)))
            (proofs-co state)
            state
            nil))))
    ((endp (cdr results)) (fms "---~%Even though we saw a disjunctive split for ~@0, it ~
          turns out there is only one viable branch to pursue, the ~
          one named ~@1.~%"
        (list (cons #\0 (tilde-@-clause-id-phrase parent-cl-id))
          (cons #\1 (tilde-@-clause-id-phrase cl-id)))
        (proofs-co state)
        state
        nil))
    (t (let* ((temp (assoc-equal cl-id summary)) (n (cadr temp))
          (d (caddr temp)))
        (fms "---~%After simplifying every branch of the disjunctive ~
              split for ~@0 we choose to pursue the branch named ~@1, ~
              which gave rise to ~x2 *-named formula~#3~[s~/~/s~] ~
              with total estimated difficulty of ~x4.  The complete ~
              list of branches considered is shown below.~%~%~
              clause id              subgoals    estimated~%~
              ~                        pushed     difficulty~%~*5"
          (list (cons #\0 (tilde-@-clause-id-phrase parent-cl-id))
            (cons #\1 (tilde-@-clause-id-phrase cl-id))
            (cons #\2 n)
            (cons #\3 (zero-one-or-more n))
            (cons #\4 d)
            (cons #\5 (tilde-*-or-hit-summary-phrase summary)))
          (proofs-co state)
          state
          nil)))))

(defun term-difficulty
  (term wrld)
  (term-difficulty1 term wrld 0))

(defun clause-difficulty
  (cl wrld)
  (term-difficulty1-lst cl wrld 0))

(defun clause-set-difficulty
  (cl-set wrld)
  (cond ((null cl-set) 0)
    (t (+ (clause-difficulty (car cl-set) wrld)
        (clause-set-difficulty (cdr cl-set) wrld)))))

(defun pool-difficulty
  (element0 pool wrld)
  (cond ((endp pool) 0)
    ((equal (car pool) element0) 0)
    ((not (eq (access pool-element (car pool) :tag)
         'to-be-proved-by-induction)) 0)
    (t (+ (clause-set-difficulty (access pool-element (car pool) :clause-set)
          wrld)
        (pool-difficulty element0 (cdr pool) wrld)))))

(defun how-many-to-be-proved
  (element0 pool)
  (cond ((endp pool) 0)
    ((equal (car pool) element0) 0)
    ((not (eq (access pool-element (car pool) :tag)
         'to-be-proved-by-induction)) 0)
    (t (+ 1 (how-many-to-be-proved element0 (cdr pool))))))

(defun pick-best-pspv-for-waterfall0-or-hit1
  (results element0 wrld ans ans-difficulty summary)
  (cond ((endp results) (mv ans summary))
    (t (let* ((cl-id (car (car results))) (pspv (cdr (car results)))
          (new-difficulty (pool-difficulty element0
              (access prove-spec-var pspv :pool)
              wrld))
          (new-summary (cons (list cl-id
                (how-many-to-be-proved element0
                  (access prove-spec-var pspv :pool))
                new-difficulty)
              summary)))
        (if (or (null ans) (< new-difficulty ans-difficulty))
          (pick-best-pspv-for-waterfall0-or-hit1 (cdr results)
            element0
            wrld
            (car results)
            new-difficulty
            new-summary)
          (pick-best-pspv-for-waterfall0-or-hit1 (cdr results)
            element0
            wrld
            ans
            ans-difficulty
            new-summary))))))

(defun pick-best-pspv-for-waterfall0-or-hit
  (results pspv0 wrld)
  (pick-best-pspv-for-waterfall0-or-hit1 results
    (car (access prove-spec-var pspv0 :pool))
    wrld
    nil
    nil
    nil))

(defun change-or-hit-history-entry
  (i hist cl-id)
  (let* ((val (tagged-object :or (access history-entry (car hist) :ttree))) (parent-cl-id (nth 0 val))
      (uhs-lst (nth 2 val)))
    (cons (make history-entry
        :signal 'or-hit
        :processor 'apply-top-hints-clause
        :clause (access history-entry (car hist) :clause)
        :ttree (add-to-tag-tree! :or (list parent-cl-id i uhs-lst) nil)
        :cl-id cl-id)
      (cdr hist))))

(defun apply-reorder-hint-front
  (indices len clauses acc)
  (cond ((endp indices) acc)
    (t (apply-reorder-hint-front (cdr indices)
        len
        clauses
        (cons (nth (- len (car indices)) clauses) acc)))))

(defun apply-reorder-hint-back
  (indices current-index clauses acc)
  (cond ((endp clauses) acc)
    (t (apply-reorder-hint-back indices
        (1- current-index)
        (cdr clauses)
        (if (member current-index indices)
          acc
          (cons (car clauses) acc))))))

(defun filter->
  (lst max)
  (cond ((endp lst) nil)
    ((> (car lst) max) (cons (car lst) (filter-> (cdr lst) max)))
    (t (filter-> (cdr lst) max))))

(defun erase-rw-cache-any-tag-from-pspv
  (pspv)
  (let ((ttree (access prove-spec-var pspv :tag-tree)))
    (cond ((tagged-objectsp 'rw-cache-any-tag ttree) (change prove-spec-var
          pspv
          :tag-tree (rw-cache-enter-context ttree)))
      (t pspv))))

(defun restore-rw-cache-state-in-pspv
  (new-pspv old-pspv)
  (let* ((old-rcnst (access prove-spec-var old-pspv :rewrite-constant)) (old-rw-cache-state (access rewrite-constant old-rcnst :rw-cache-state))
      (new-rcnst (access prove-spec-var new-pspv :rewrite-constant))
      (new-rw-cache-state (access rewrite-constant new-rcnst :rw-cache-state)))
    (cond ((eq old-rw-cache-state new-rw-cache-state) new-pspv)
      (t (change prove-spec-var
          new-pspv
          :rewrite-constant (change rewrite-constant
            new-rcnst
            :rw-cache-state old-rw-cache-state))))))

(defun waterfall
  (forcing-round pool-lst
    x
    pspv
    hints
    ens
    wrld
    ctx
    state
    step-limit)
  (let ((parent-clause-id (cond ((and (= forcing-round 0) (null pool-lst)) *initial-clause-id*)
         (t (make clause-id
             :forcing-round forcing-round
             :pool-lst pool-lst
             :case-lst nil
             :primes 0)))) (clauses (cond ((and (not (= forcing-round 0)) (null pool-lst)) (strip-cdrs x))
          (t x)))
      (pspv (maybe-set-rw-cache-state-disabled (erase-rw-cache-from-pspv pspv))))
    (pprogn (cond ((output-ignored-p 'proof-tree state) state)
        (t (initialize-proof-tree parent-clause-id x ctx state)))
      (sl-let (signal new-pspv new-jppl-flg state)
        (waterfall1-lst (cond ((null clauses) 0)
            ((null (cdr clauses)) 'settled-down-clause)
            (t (length clauses)))
          parent-clause-id
          clauses
          nil
          pspv
          nil
          hints
          (and (eql forcing-round 0) (null pool-lst))
          ens
          wrld
          ctx
          state
          step-limit)
        (cond ((eq signal 'error) (mv step-limit t nil nil state))
          (t (mv step-limit nil new-pspv new-jppl-flg state)))))))

(defun some-pool-member-subsumes
  (pool clause-set)
  (cond ((null pool) nil)
    ((eq (clause-set-subsumes *init-subsumes-count*
         (access pool-element (car pool) :clause-set)
         clause-set)
       t) pool)
    (t (some-pool-member-subsumes (cdr pool) clause-set))))

(defun add-to-pop-history
  (action cl-set pool-lst subsumer-pool-lst pop-history)
  (cond ((eq action 'pop) (cond ((and pop-history (eq (caar pop-history) 'pop)) (cons (cons 'pop (cons pool-lst (cdar pop-history)))
            (cdr pop-history)))
        (t (cons (list 'pop pool-lst) pop-history))))
    ((eq action 'consider) (cons (list 'consider cl-set pool-lst) pop-history))
    ((eq action 'qed) (cons '(qed) pop-history))
    (t (cons (list action cl-set pool-lst subsumer-pool-lst)
        pop-history))))

(defun pop-clause1
  (pool pop-history)
  (cond ((null pool) (mv 'win
        nil
        nil
        nil
        (add-to-pop-history 'qed nil nil nil pop-history)
        nil))
    ((eq (access pool-element (car pool) :tag)
       'being-proved-by-induction) (pop-clause1 (cdr pool)
        (add-to-pop-history 'pop
          nil
          (pool-lst (cdr pool))
          nil
          pop-history)))
    ((equal (access pool-element (car pool) :clause-set) '(nil)) (mv 'lose nil nil nil nil pool))
    (t (let ((pool-lst (pool-lst (cdr pool))) (sub-pool (some-pool-member-subsumes (cdr pool)
              (access pool-element (car pool) :clause-set))))
        (cond ((null sub-pool) (mv 'continue
              pool-lst
              (access pool-element (car pool) :clause-set)
              (access pool-element (car pool) :hint-settings)
              (add-to-pop-history 'consider
                (access pool-element (car pool) :clause-set)
                pool-lst
                nil
                pop-history)
              (cons (change pool-element
                  (car pool)
                  :tag 'being-proved-by-induction)
                (cdr pool))))
          ((eq (access pool-element (car sub-pool) :tag)
             'being-proved-by-induction) (mv 'lose
              nil
              nil
              nil
              (add-to-pop-history 'subsumed-by-parent
                (access pool-element (car pool) :clause-set)
                pool-lst
                (pool-lst (cdr sub-pool))
                pop-history)
              pool))
          (t (pop-clause1 (cdr pool)
              (add-to-pop-history 'subsumed-below
                (access pool-element (car pool) :clause-set)
                pool-lst
                (pool-lst (cdr sub-pool))
                pop-history))))))))

(defun make-defthm-forms-for-byes
  (byes wrld)
  (cond ((null byes) nil)
    (t (cons (list 'defthm
          (caar byes)
          (prettyify-clause (cdar byes) nil wrld)
          :rule-classes nil)
        (make-defthm-forms-for-byes (cdr byes) wrld)))))

(defun pop-clause-msg1
  (forcing-round lst
    jppl-flg
    prev-action
    gag-state
    msg-p
    state)
  (cond ((null lst) (pprogn (increment-timer 'print-time state)
        (mv gag-state state)))
    (t (let ((entry (car lst)))
        (mv-let (gag-state state)
          (case-match entry
            (('pop . pool-lsts) (mv-let (gagst msgs)
                (pop-clause-update-gag-state-pop pool-lsts
                  gag-state
                  nil
                  msg-p
                  state)
                (pprogn (io? prove
                    nil
                    state
                    (prev-action pool-lsts forcing-round msgs)
                    (pprogn (fms (cond ((gag-mode) (assert$ pool-lsts "~*1 ~#0~[is~/are~] COMPLETED!~|"))
                          ((null prev-action) "That completes the proof~#0~[~/s~] of ~*1.~|")
                          (t "That, in turn, completes the proof~#0~[~/s~] of ~
                             ~*1.~|"))
                        (list (cons #\0 pool-lsts)
                          (cons #\1
                            (list ""
                              "~@*"
                              "~@* and "
                              "~@*, "
                              (tilde-@-pool-name-phrase-lst forcing-round
                                (reverse pool-lsts)))))
                        (proofs-co state)
                        state
                        nil)
                      (cond ((and msgs (gag-mode)) (mv-let (col state)
                            (fmt1 "Thus key checkpoint~#1~[~ ~*0 is~/s ~*0 are~] ~
                            COMPLETED!~|"
                              (list (cons #\0 (list "" "~@*" "~@* and " "~@*, " (reverse msgs)))
                                (cons #\1 msgs))
                              0
                              (proofs-co state)
                              state
                              nil)
                            (declare (ignore col))
                            state))
                        (t state))))
                  (mv gagst state))))
            (('qed) (mv gag-state state))
            (& (let ((pool-lst (caddr entry)))
                (mv-let (gagst cl-id)
                  (cond ((eq (car entry) 'consider) (mv gag-state nil))
                    (t (remove-pool-lst-from-gag-state pool-lst gag-state state)))
                  (pprogn (io? prove
                      nil
                      state
                      (prev-action forcing-round
                        pool-lst
                        entry
                        cl-id
                        jppl-flg
                        gag-state)
                      (let* ((cl-set (cadr entry)) (jppl-flg (if (gag-mode)
                              (gag-mode-jppl-flg gag-state)
                              jppl-flg))
                          (push-pop-flg (and jppl-flg (equal jppl-flg pool-lst))))
                        (pprogn (cond (push-pop-flg state)
                            (t (fms (cond ((eq prev-action 'pop) "We therefore turn our attention to ~@1, ~
                                  which is~|~%~q0.~|")
                                  ((null prev-action) "So we now return to ~@1, which is~|~%~q0.~|")
                                  (t "We next consider ~@1, which is~|~%~q0.~|"))
                                (list (cons #\0
                                    (prettyify-clause-set cl-set
                                      (let*-abstractionp state)
                                      (w state)))
                                  (cons #\1 (tilde-@-pool-name-phrase forcing-round pool-lst)))
                                (proofs-co state)
                                state
                                (term-evisc-tuple nil state))))
                          (case-match entry
                            (('subsumed-below & & subsumer-pool-lst) (pprogn (fms "But the formula above is subsumed by ~@1, ~
                                which we'll try to prove later.  We therefore ~
                                regard ~@0 as proved (pending the proof of ~
                                the more general ~@1).~|"
                                  (list (cons #\0 (tilde-@-pool-name-phrase forcing-round pool-lst))
                                    (cons #\1
                                      (tilde-@-pool-name-phrase forcing-round subsumer-pool-lst)))
                                  (proofs-co state)
                                  state
                                  nil)
                                (cond ((and cl-id (gag-mode)) (fms "~@0 COMPLETED!~|"
                                      (list (cons #\0 (tilde-@-clause-id-phrase cl-id)))
                                      (proofs-co state)
                                      state
                                      nil))
                                  (t state))))
                            (('subsumed-by-parent & & subsumer-pool-lst) (fms "The formula above is subsumed by one of its ~
                               parents, ~@0, which we're in the process of ~
                               trying to prove by induction.  When an ~
                               inductive proof pushes a subgoal for induction ~
                               that is less general than the original goal, ~
                               it may be a sign that either an inappropriate ~
                               induction was chosen or that the original goal ~
                               is insufficiently general.  In any case, our ~
                               proof attempt has failed.~|"
                                (list (cons #\0
                                    (tilde-@-pool-name-phrase forcing-round subsumer-pool-lst)))
                                (proofs-co state)
                                state
                                nil))
                            (& state)))))
                    (mv gagst state))))))
          (pop-clause-msg1 forcing-round
            (cdr lst)
            jppl-flg
            (caar lst)
            gag-state
            msg-p
            state))))))

(defun pop-clause-msg
  (forcing-round pop-history jppl-flg pspv state)
  (pprogn (increment-timer 'prove-time state)
    (mv-let (gag-state state)
      (let ((gag-state0 (access prove-spec-var pspv :gag-state)))
        (pop-clause-msg1 forcing-round
          (reverse pop-history)
          jppl-flg
          nil
          gag-state0
          (not (output-ignored-p 'prove state))
          state))
      (pprogn (record-gag-state gag-state state)
        (increment-timer 'print-time state)
        (mv (change prove-spec-var pspv :gag-state gag-state) state)))))

(defun subsumed-clause-ids-from-pop-history
  (forcing-round pop-history)
  (cond ((endp pop-history) nil)
    ((eq (car (car pop-history)) 'subsumed-below) (cons (make clause-id
          :forcing-round forcing-round
          :pool-lst (caddr (car pop-history))
          :case-lst nil
          :primes 0)
        (subsumed-clause-ids-from-pop-history forcing-round
          (cdr pop-history))))
    (t (subsumed-clause-ids-from-pop-history forcing-round
        (cdr pop-history)))))

(defun increment-proof-tree-pop-clause
  (forcing-round pop-history state)
  (let ((old-proof-tree (f-get-global 'proof-tree state)) (dead-clause-ids (subsumed-clause-ids-from-pop-history forcing-round
          pop-history)))
    (if dead-clause-ids
      (pprogn (f-put-global 'proof-tree
          (prune-proof-tree forcing-round
            dead-clause-ids
            old-proof-tree)
          state)
        (print-proof-tree state))
      state)))

(defun pop-clause
  (forcing-round pspv jppl-flg state)
  (mv-let (signal pool-lst cl-set hint-settings pop-history new-pool)
    (pop-clause1 (access prove-spec-var pspv :pool) nil)
    (mv-let (new-pspv state)
      (pop-clause-msg forcing-round
        pop-history
        jppl-flg
        pspv
        state)
      (pprogn (io? proof-tree
          nil
          state
          (forcing-round pop-history)
          (pprogn (increment-timer 'prove-time state)
            (increment-proof-tree-pop-clause forcing-round
              pop-history
              state)
            (increment-timer 'proof-tree-time state)))
        (mv signal
          pool-lst
          cl-set
          hint-settings
          (change prove-spec-var new-pspv :pool new-pool)
          state)))))

(defun tilde-@-assumnotes-phrase-lst
  (lst wrld)
  (cond ((null lst) nil)
    (t (cons (cons (cond ((null (cdr lst)) (cond ((and (consp (access assumnote (car lst) :rune))
                   (null (base-symbol (access assumnote (car lst) :rune)))) " ~@0~%  by primitive type reasoning about~%  ~q2.~|")
                ((eq (access assumnote (car lst) :rune) 'equal) " ~@0~%  by the use of linear arithmetic on~%  ~q2.~|")
                ((symbolp (access assumnote (car lst) :rune)) " ~@0~%  by assuming the guard for ~x1 in~%  ~q2.~|")
                (t " ~@0~%  by applying ~x1 to~%  ~q2.~|")))
            ((null (cddr lst)) (cond ((and (consp (access assumnote (car lst) :rune))
                   (null (base-symbol (access assumnote (car lst) :rune)))) " ~@0~%  by primitive type reasoning about~%  ~q2,~| and~|")
                ((eq (access assumnote (car lst) :rune) 'equal) " ~@0~%  by the linearization of~%  ~q2,~| and~|")
                ((symbolp (access assumnote (car lst) :rune)) " ~@0~%  by assuming the guard for ~x1 in~%  ~q2,~| and~|")
                (t " ~@0~%  by applying ~x1 to~%  ~q2,~| and~|")))
            (t (cond ((and (consp (access assumnote (car lst) :rune))
                   (null (base-symbol (access assumnote (car lst) :rune)))) " ~@0~%  by primitive type reasoning about~%  ~q2,~|")
                ((eq (access assumnote (car lst) :rune) 'equal) " ~@0~%  by the linearization of~%  ~q2,~|")
                ((symbolp (access assumnote (car lst) :rune)) " ~@0~%  by assuming the guard for ~x1 in~%  ~q2,~|")
                (t " ~@0~%  by applying ~x1 to~%  ~q2,~|"))))
          (list (cons #\0
              (tilde-@-clause-id-phrase (access assumnote (car lst) :cl-id)))
            (cons #\1 (access assumnote (car lst) :rune))
            (cons #\2
              (untranslate (access assumnote (car lst) :target) nil wrld))))
        (tilde-@-assumnotes-phrase-lst (cdr lst) wrld)))))

(defun tilde-*-assumnotes-column-phrase
  (assumnotes wrld)
  (list ""
    "~@*"
    "~@*"
    "~@*"
    (tilde-@-assumnotes-phrase-lst assumnotes wrld)))

(defun tilde-@-assumnotes-phrase-lst-gag-mode
  (lst acc)
  (cond ((null lst) (cond ((null acc) acc)
        ((null (cdr acc)) (list (msg "in~@0.~|" (car acc))))
        (t (reverse (list* (msg "in~@0.~|" (car acc))
              (msg "in~@0, and " (cadr acc))
              (pairlis-x1 "in~@0, ~|"
                (pairlis$ (pairlis-x1 #\0 (cddr acc)) nil)))))))
    (t (tilde-@-assumnotes-phrase-lst-gag-mode (cdr lst)
        (let* ((cl-id-phrase (tilde-@-clause-id-phrase (access assumnote (car lst) :cl-id))) (rune (access assumnote (car lst) :rune))
            (x (cond ((and (consp rune) (null (base-symbol rune))) (list " ~@0 by primitive type reasoning"
                    (cons #\0 cl-id-phrase)))
                ((eq rune 'equal) (list " ~@0 by linearization" (cons #\0 cl-id-phrase)))
                (t (assert$ (not (symbolp rune))
                    (list " ~@0 by applying ~x1"
                      (cons #\0 cl-id-phrase)
                      (cons #\1 rune)))))))
          (add-to-set-equal x acc))))))

(defun tilde-*-assumnotes-column-phrase-gag-mode
  (assumnotes)
  (list ""
    "~@*"
    "~@*"
    "~@*"
    (tilde-@-assumnotes-phrase-lst-gag-mode assumnotes nil)))

(defun process-assumptions-msg1
  (forcing-round n pairs state)
  (cond ((null pairs) state)
    (t (pprogn (let ((cl-id-phrase (tilde-@-clause-id-phrase (make clause-id
                 :forcing-round (1+ forcing-round)
                 :pool-lst nil
                 :case-lst (if n
                   (list n)
                   nil)
                 :primes 0))))
          (cond ((gag-mode) (fms "~@0 was forced ~*1"
                (list (cons #\0 cl-id-phrase)
                  (cons #\1
                    (tilde-*-assumnotes-column-phrase-gag-mode (car (car pairs)))))
                (proofs-co state)
                state
                (term-evisc-tuple nil state)))
            (t (fms "~@0, below, will focus on~%~q1,~|which was forced in~%~*2"
                (list (cons #\0 cl-id-phrase)
                  (cons #\1
                    (untranslate (car (last (cdr (car pairs)))) t (w state)))
                  (cons #\2
                    (tilde-*-assumnotes-column-phrase (car (car pairs))
                      (w state))))
                (proofs-co state)
                state
                (term-evisc-tuple nil state)))))
        (process-assumptions-msg1 forcing-round
          (if n
            (1- n)
            nil)
          (cdr pairs)
          state)))))

(defun process-assumptions-msg
  (forcing-round n0 n pairs state)
  (io? prove
    nil
    state
    (n0 forcing-round n pairs)
    (pprogn (fms "Modulo~#g~[ the following~/ one~/~]~#0~[~/ ~n1~]~#2~[~/ newly~] ~
          forced goal~#0~[~/s~], that completes ~#2~[the proof of the input ~
          Goal~/Forcing Round ~x3~].~#4~[~/  For what it is worth, the~#0~[~/ ~
          ~n1~] new goal~#0~[ was~/s were~] generated by cleaning up ~n5 ~
          forced hypotheses.~]  See :DOC forcing-round.~%"
        (list (cons #\g
            (if (gag-mode)
              (if (cdr pairs)
                2
                1)
              0))
          (cons #\0
            (if (cdr pairs)
              1
              0))
          (cons #\1 n)
          (cons #\2
            (if (= forcing-round 0)
              0
              1))
          (cons #\3 forcing-round)
          (cons #\4
            (if (= n0 n)
              0
              1))
          (cons #\5 n0))
        (proofs-co state)
        state
        nil)
      (process-assumptions-msg1 forcing-round
        (if (= n 1)
          nil
          n)
        pairs
        state)
      (fms "We now undertake Forcing Round ~x0.~%"
        (list (cons #\0 (1+ forcing-round)))
        (proofs-co state)
        state
        nil))))

(defun count-assumptions
  (ttree)
  (length (tagged-objects 'assumption ttree)))

(defun add-type-alist-runes-to-ttree1
  (type-alist runes)
  (cond ((endp type-alist) runes)
    (t (add-type-alist-runes-to-ttree1 (cdr type-alist)
        (all-runes-in-ttree (cddr (car type-alist)) runes)))))

(defun add-type-alist-runes-to-ttree
  (type-alist ttree)
  (let* ((runes0 (tagged-objects 'lemma ttree)) (runes1 (add-type-alist-runes-to-ttree1 type-alist runes0)))
    (cond ((null runes1) ttree)
      ((null runes0) (extend-tag-tree 'lemma runes1 ttree))
      (t (extend-tag-tree 'lemma
          runes1
          (remove-tag-from-tag-tree! 'lemma ttree))))))

(defun process-assumptions-ttree
  (assns ttree)
  (cond ((endp assns) ttree)
    (t (process-assumptions-ttree (cdr assns)
        (add-type-alist-runes-to-ttree (access assumption (car assns) :type-alist)
          ttree)))))

(defun process-assumptions
  (forcing-round pspv wrld state)
  (let ((n (count-assumptions (access prove-spec-var pspv :tag-tree))))
    (pprogn (cond ((= n 0) (pprogn (if (and (saved-output-token-p 'prove state)
                (member-eq 'prove (f-get-global 'inhibit-output-lst state))
                (not (member-eq 'summary
                    (f-get-global 'inhibit-output-lst state))))
              (fms "Q.E.D.~%" nil (proofs-co state) state nil)
              state)
            (io? prove
              nil
              state
              nil
              (fms "Q.E.D.~%" nil (proofs-co state) state nil))))
        (t (io? prove
            nil
            state
            (n)
            (fms "q.e.d. (given ~n0 forced ~#1~[hypothesis~/hypotheses~])~%"
              (list (cons #\0 n)
                (cons #\1
                  (if (= n 1)
                    0
                    1)))
              (proofs-co state)
              state
              nil))))
      (mv-let (n0 assns pairs ttree1)
        (extract-and-clausify-assumptions nil
          (access prove-spec-var pspv :tag-tree)
          nil
          (access rewrite-constant
            (access prove-spec-var pspv :rewrite-constant)
            :current-enabled-structure)
          wrld
          (access rewrite-constant
            (access prove-spec-var pspv :rewrite-constant)
            :splitter-output))
        (cond ((= n0 0) (mv nil pspv state))
          (t (pprogn (process-assumptions-msg forcing-round
                n0
                (length assns)
                pairs
                state)
              (mv pairs
                (change prove-spec-var
                  pspv
                  :tag-tree (process-assumptions-ttree assns ttree1)
                  :otf-flg t)
                state))))))))

(defun do-not-induct-msg
  (forcing-round pool-lst state)
  (io? prove
    nil
    state
    (forcing-round pool-lst)
    (pprogn (increment-timer 'prove-time state)
      (fms "Normally we would attempt to prove ~@0 by induction.  However, a ~
             :DO-NOT-INDUCT hint was supplied to abort the proof attempt.~|"
        (list (cons #\0 (tilde-@-pool-name-phrase forcing-round pool-lst)))
        (proofs-co state)
        state
        nil)
      (increment-timer 'print-time state))))

(defun prove-loop2
  (forcing-round pool-lst
    clauses
    pspv
    hints
    ens
    wrld
    ctx
    state
    step-limit)
  (sl-let (erp pspv jppl-flg state)
    (pstk (waterfall forcing-round
        pool-lst
        clauses
        pspv
        hints
        ens
        wrld
        ctx
        state
        step-limit))
    (cond (erp (mv step-limit t nil state))
      (t (mv-let (signal pool-lst clauses hint-settings pspv state)
          (pstk (pop-clause forcing-round pspv jppl-flg state))
          (cond ((eq signal 'win) (mv-let (pairs new-pspv state)
                (pstk (process-assumptions forcing-round pspv wrld state))
                (mv-let (erp ttree state)
                  (accumulate-ttree-and-step-limit-into-state (access prove-spec-var new-pspv :tag-tree)
                    step-limit
                    state)
                  (assert$ (null erp)
                    (cond ((null pairs) (mv step-limit nil ttree state))
                      (t (prove-loop2 (1+ forcing-round)
                          nil
                          pairs
                          (change prove-spec-var
                            new-pspv
                            :gag-state *initial-gag-state*)
                          hints
                          ens
                          wrld
                          ctx
                          state
                          step-limit)))))))
            ((eq signal 'bye) (mv step-limit
                t
                (er hard
                  ctx
                  "Surprising case in prove-loop2; please contact the ACL2 ~
                     implementors!")
                state))
            ((eq signal 'lose) (mv step-limit t nil state))
            ((and (cdr (assoc-eq :do-not-induct hint-settings))
               (not (assoc-eq :induct hint-settings))) (pprogn (do-not-induct-msg forcing-round pool-lst state)
                (mv step-limit t nil state)))
            (t (mv-let (signal clauses pspv state)
                (pstk (induct forcing-round
                    pool-lst
                    clauses
                    hint-settings
                    pspv
                    wrld
                    ctx
                    state))
                (cond ((eq signal 'lose) (mv step-limit t nil state))
                  (t (prove-loop2 forcing-round
                      pool-lst
                      clauses
                      pspv
                      hints
                      ens
                      wrld
                      ctx
                      state
                      step-limit)))))))))))

(defun prove-loop1
  (forcing-round pool-lst
    clauses
    pspv
    hints
    ens
    wrld
    ctx
    state)
  (sl-let (erp val state)
    (catch-step-limit (prove-loop2 forcing-round
        pool-lst
        clauses
        pspv
        hints
        ens
        wrld
        ctx
        state
        (initial-step-limit wrld state)))
    (pprogn (f-put-global 'last-step-limit step-limit state)
      (mv erp val state))))

(defun prove-loop0
  (clauses pspv hints ens wrld ctx state)
  (state-global-let* ((guard-checking-on nil) (in-prove-flg t))
    (prove-loop1 0 nil clauses pspv hints ens wrld ctx state)))

(defun prove-loop
  (clauses pspv hints ens wrld ctx state)
  (prog2$ (clear-pstk)
    (pprogn (increment-timer 'other-time state)
      (f-put-global 'bddnotes nil state)
      (pprogn (f-put-global 'gag-state *initial-gag-state* state)
        (f-put-global 'gag-state-saved nil state))
      (mv-let (erp ttree state)
        (bind-acl2-time-limit (prove-loop0 clauses pspv hints ens wrld ctx state))
        (pprogn (increment-timer 'prove-time state)
          (cond (erp (mv erp nil state)) (t (value ttree))))))))

(defun chk-assumption-free-ttree
  (ttree ctx state)
  (cond ((tagged-objectsp 'assumption ttree) (mv t
        (er hard
          ctx
          "The 'assumption ~x0 was found in the final ttree!"
          (car (tagged-objects 'assumption ttree)))
        state))
    ((tagged-objectsp 'fc-derivation ttree) (mv t
        (er hard
          ctx
          "The 'fc-derivation ~x0 was found in the final ttree!"
          (car (tagged-objects 'fc-derivation ttree)))
        state))
    (t (value nil))))

(defun push-current-acl2-world
  (name state)
  (declare (xargs :guard (and (symbolp name)
        (alistp (f-get-global 'acl2-world-alist state)))))
  (prog2$ (or (symbolp name)
      (er hard
        'push-current-acl2-world
        "It is illegal to call push-current-acl2-world with ~x0, ~
                   because it is not a symbol."
        name))
    (f-put-global 'acl2-world-alist
      (acons name
        (w state)
        (f-get-global 'acl2-world-alist state))
      state)))

(defun pop-current-acl2-world
  (name state)
  (declare (xargs :guard (and (symbolp name)
        (alistp (f-get-global 'acl2-world-alist state))
        (assoc-eq name (f-get-global 'acl2-world-alist state)))))
  (prog2$ (or (symbolp name)
      (er hard
        'pop-current-acl2-world
        "It is illegal to call pop-current-acl2-world with ~x0, because ~
            it is not a symbol."
        name))
    (let ((pair (assoc-eq name (f-get-global 'acl2-world-alist state))))
      (cond ((null pair) (prog2$ (er hard
              'pop-current-acl2-world
              "Attempted to pop the name ~x0, which is not bound in ~x1."
              name
              '(@ acl2-world-alist))
            state))
        (t (pprogn (set-w! (cdr pair) state)
            (f-put-global 'acl2-world-alist
              (remove1-assoc-eq name
                (f-get-global 'acl2-world-alist state))
              state)))))))

(defun prove
  (term pspv hints ens wrld ctx state)
  (cond ((ld-skip-proofsp state) (value nil))
    (t (prog2$ (initialize-fc-wormhole-sites)
        (pprogn (f-put-global 'saved-output-reversed nil state)
          (push-current-acl2-world 'saved-output-reversed state)
          (f-put-global 'saved-output-p
            (not (member-eq 'prove (f-get-global 'inhibit-output-lst state)))
            state)
          (push-io-record :ctx (list 'mv-let
              '(col state)
              '(fmt "Output replay for: "
                nil
                (standard-co state)
                state
                nil)
              (list 'mv-let
                '(col state)
                (list 'fmt-ctx
                  (list 'quote ctx)
                  'col
                  '(standard-co state)
                  'state)
                '(declare (ignore col))
                '(newline (standard-co state) state)))
            state)
          (er-let* ((ttree1 (prove-loop (list (list term))
                 (change prove-spec-var
                   pspv
                   :user-supplied-term term
                   :orig-hints hints)
                 hints
                 ens
                 wrld
                 ctx
                 state)))
            (er-progn (chk-assumption-free-ttree ttree1 ctx state)
              (let ((byes (tagged-objects :bye ttree1)))
                (cond (byes (pprogn (io? prove
                        nil
                        state
                        (wrld byes)
                        (fms "To complete this proof you could try to admit the ~
                        following event~#0~[~/s~]:~|~%~*1~%See the discussion ~
                        of :by hints in :DOC hints regarding the ~
                        name~#0~[~/s~] displayed above.~|"
                          (list (cons #\0 byes)
                            (cons #\1
                              (list ""
                                "~|~     ~q*."
                                "~|~     ~q*,~|and~|"
                                "~|~     ~q*,~|~%"
                                (make-defthm-forms-for-byes byes wrld))))
                          (proofs-co state)
                          state
                          (term-evisc-tuple nil state)))
                      (silent-error state)))
                  (t (value ttree1)))))))))))