induct

(defun abbreviationp
  (lambda-flg vars term2)
  (not (eq (abbreviationp1 lambda-flg vars term2) t)))

(defun find-abbreviation-lemma
  (term geneqv lemmas ens wrld)
  (cond ((null lemmas) (mv nil nil nil nil))
    ((and (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
       (eq (access rewrite-rule (car lemmas) :subclass)
         'abbreviation)
       (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
         geneqv
         wrld)) (mv-let (wonp unify-subst)
        (one-way-unify (access rewrite-rule (car lemmas) :lhs) term)
        (cond (wonp (mv t
              (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
                geneqv
                wrld)
              (car lemmas)
              unify-subst))
          (t (find-abbreviation-lemma term geneqv (cdr lemmas) ens wrld)))))
    (t (find-abbreviation-lemma term geneqv (cdr lemmas) ens wrld))))

(defun and-orp
  (term bool lambda-okp)
  (case-match term
    (('if & c2 c3) (if bool
        (or (equal c2 *t*) (equal c3 *t*))
        (or (equal c2 *nil*) (equal c3 *nil*))))
    ((('lambda & body) . &) (and lambda-okp (and-orp body bool lambda-okp)))))

(defun find-and-or-lemma
  (term bool lemmas ens wrld)
  (cond ((null lemmas) (mv nil nil nil nil))
    ((and (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
       (or (eq (access rewrite-rule (car lemmas) :subclass) 'backchain)
         (eq (access rewrite-rule (car lemmas) :subclass)
           'abbreviation))
       (null (access rewrite-rule (car lemmas) :hyps))
       (null (access rewrite-rule (car lemmas) :heuristic-info))
       (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
         *geneqv-iff*
         wrld)
       (and-orp (access rewrite-rule (car lemmas) :rhs) bool t)) (mv-let (wonp unify-subst)
        (one-way-unify (access rewrite-rule (car lemmas) :lhs) term)
        (cond (wonp (mv t
              (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
                *geneqv-iff*
                wrld)
              (car lemmas)
              unify-subst))
          (t (find-and-or-lemma term bool (cdr lemmas) ens wrld)))))
    (t (find-and-or-lemma term bool (cdr lemmas) ens wrld))))

(defun expand-and-or
  (term bool
    fns-to-be-ignored-by-rewrite
    ens
    wrld
    state
    ttree
    step-limit)
  (cond ((variablep term) (mv step-limit nil term ttree))
    ((fquotep term) (mv step-limit nil term ttree))
    ((member-equal (ffn-symb term) fns-to-be-ignored-by-rewrite) (mv step-limit nil term ttree))
    ((flambda-applicationp term) (cond ((and-orp (lambda-body (ffn-symb term)) bool nil) (sl-let (term ttree)
            (expand-abbreviations (subcor-var (lambda-formals (ffn-symb term))
                (fargs term)
                (lambda-body (ffn-symb term)))
              nil
              *geneqv-iff*
              nil
              fns-to-be-ignored-by-rewrite
              (rewrite-stack-limit wrld)
              step-limit
              ens
              wrld
              state
              ttree)
            (mv step-limit t term ttree)))
        (t (mv step-limit nil term ttree))))
    (t (let ((def-body (def-body (ffn-symb term) wrld)))
        (cond ((and def-body
             (null (access def-body def-body :recursivep))
             (null (access def-body def-body :hyp))
             (member-eq (access def-body def-body :equiv) '(equal iff))
             (enabled-numep (access def-body def-body :nume) ens)
             (and-orp (access def-body def-body :concl) bool nil)) (sl-let (term ttree)
              (with-accumulated-persistence (access def-body def-body :rune)
                ((the (signed-byte 61) step-limit) term ttree)
                t
                (expand-abbreviations (subcor-var (access def-body def-body :formals)
                    (fargs term)
                    (access def-body def-body :concl))
                  nil
                  *geneqv-iff*
                  nil
                  fns-to-be-ignored-by-rewrite
                  (rewrite-stack-limit wrld)
                  step-limit
                  ens
                  wrld
                  state
                  (push-lemma? (access def-body def-body :rune) ttree)))
              (mv step-limit t term ttree)))
          (t (mv-let (wonp cr-rune lemma unify-subst)
              (find-and-or-lemma term
                bool
                (getpropc (ffn-symb term) 'lemmas nil wrld)
                ens
                wrld)
              (cond (wonp (sl-let (term ttree)
                    (with-accumulated-persistence (access rewrite-rule lemma :rune)
                      ((the (signed-byte 61) step-limit) term ttree)
                      t
                      (expand-abbreviations (sublis-var unify-subst (access rewrite-rule lemma :rhs))
                        nil
                        *geneqv-iff*
                        nil
                        fns-to-be-ignored-by-rewrite
                        (rewrite-stack-limit wrld)
                        step-limit
                        ens
                        wrld
                        state
                        (push-lemma cr-rune
                          (push-lemma (access rewrite-rule lemma :rune) ttree))))
                    (mv step-limit t term ttree)))
                (t (mv step-limit nil term ttree))))))))))

(defun clausify-input1
  (term bool
    fns-to-be-ignored-by-rewrite
    ens
    wrld
    state
    ttree
    step-limit)
  (cond ((equal term
       (if bool
         *nil*
         *t*)) (mv step-limit nil ttree))
    ((ffn-symb-p term 'if) (let ((t1 (fargn term 1)) (t2 (fargn term 2))
          (t3 (fargn term 3)))
        (cond (bool (cond ((equal t3 *t*) (sl-let (cl1 ttree)
                  (clausify-input1 t1
                    nil
                    fns-to-be-ignored-by-rewrite
                    ens
                    wrld
                    state
                    ttree
                    step-limit)
                  (sl-let (cl2 ttree)
                    (clausify-input1 t2
                      t
                      fns-to-be-ignored-by-rewrite
                      ens
                      wrld
                      state
                      ttree
                      step-limit)
                    (mv step-limit (disjoin-clauses cl1 cl2) ttree))))
              ((equal t2 *t*) (sl-let (cl1 ttree)
                  (clausify-input1 t1
                    t
                    fns-to-be-ignored-by-rewrite
                    ens
                    wrld
                    state
                    ttree
                    step-limit)
                  (sl-let (cl2 ttree)
                    (clausify-input1 t3
                      t
                      fns-to-be-ignored-by-rewrite
                      ens
                      wrld
                      state
                      ttree
                      step-limit)
                    (mv step-limit (disjoin-clauses cl1 cl2) ttree))))
              (t (mv step-limit (list term) ttree))))
          ((equal t3 *nil*) (sl-let (cl1 ttree)
              (clausify-input1 t1
                nil
                fns-to-be-ignored-by-rewrite
                ens
                wrld
                state
                ttree
                step-limit)
              (sl-let (cl2 ttree)
                (clausify-input1 t2
                  nil
                  fns-to-be-ignored-by-rewrite
                  ens
                  wrld
                  state
                  ttree
                  step-limit)
                (mv step-limit (disjoin-clauses cl1 cl2) ttree))))
          ((equal t2 *nil*) (sl-let (cl1 ttree)
              (clausify-input1 t1
                t
                fns-to-be-ignored-by-rewrite
                ens
                wrld
                state
                ttree
                step-limit)
              (sl-let (cl2 ttree)
                (clausify-input1 t3
                  nil
                  fns-to-be-ignored-by-rewrite
                  ens
                  wrld
                  state
                  ttree
                  step-limit)
                (mv step-limit (disjoin-clauses cl1 cl2) ttree))))
          (t (mv step-limit (list (dumb-negate-lit term)) ttree)))))
    (t (sl-let (wonp term ttree)
        (expand-and-or term
          bool
          fns-to-be-ignored-by-rewrite
          ens
          wrld
          state
          ttree
          step-limit)
        (cond (wonp (clausify-input1 term
              bool
              fns-to-be-ignored-by-rewrite
              ens
              wrld
              state
              ttree
              step-limit))
          (bool (mv step-limit (list term) ttree))
          (t (mv step-limit (list (dumb-negate-lit term)) ttree)))))))

(defun clausify-input1-lst
  (lst fns-to-be-ignored-by-rewrite
    ens
    wrld
    state
    ttree
    step-limit)
  (cond ((null lst) (mv step-limit nil ttree))
    (t (sl-let (clause ttree)
        (clausify-input1 (car lst)
          t
          fns-to-be-ignored-by-rewrite
          ens
          wrld
          state
          ttree
          step-limit)
        (sl-let (clauses ttree)
          (clausify-input1-lst (cdr lst)
            fns-to-be-ignored-by-rewrite
            ens
            wrld
            state
            ttree
            step-limit)
          (mv step-limit
            (conjoin-clause-to-clause-set clause clauses)
            ttree))))))

(defun clausify-input
  (term fns-to-be-ignored-by-rewrite
    ens
    wrld
    state
    ttree
    step-limit)
  (sl-let (neg-clause ttree)
    (clausify-input1 term
      nil
      fns-to-be-ignored-by-rewrite
      ens
      wrld
      state
      ttree
      step-limit)
    (clausify-input1-lst (dumb-negate-lit-lst neg-clause)
      fns-to-be-ignored-by-rewrite
      ens
      wrld
      state
      ttree
      step-limit)))

(defun expand-some-non-rec-fns-in-clauses
  (fns clauses wrld)
  (cond ((null clauses) nil)
    (t (let ((cl (expand-some-non-rec-fns-lst fns (car clauses) wrld)))
        (cond ((trivial-clause-p cl wrld) (expand-some-non-rec-fns-in-clauses fns (cdr clauses) wrld))
          (t (cons cl
              (expand-some-non-rec-fns-in-clauses fns (cdr clauses) wrld))))))))

(defun no-op-histp
  (hist)
  (or (null hist)
    (and hist
      (member-eq (access history-entry (car hist) :processor)
        '(apply-top-hints-clause preprocess-clause))
      (tag-tree-occur 'hidden-clause
        t
        (access history-entry (car hist) :ttree)))
    (and hist
      (eq (access history-entry (car hist) :processor)
        'settled-down-clause)
      (cdr hist)
      (member-eq (access history-entry (cadr hist) :processor)
        '(apply-top-hints-clause preprocess-clause))
      (tag-tree-occur 'hidden-clause
        t
        (access history-entry (cadr hist) :ttree)))))

(defun expand-any-final-implies
  (cl wrld)
  (cond ((null cl) nil)
    ((null (cdr cl)) (list (expand-any-final-implies1 (car cl) wrld)))
    (t (cons (car cl) (expand-any-final-implies (cdr cl) wrld)))))

(defun rw-cache-state
  (wrld)
  (let ((pair (assoc-eq t (table-alist 'rw-cache-state-table wrld))))
    (cond (pair (cdr pair)) (t *default-rw-cache-state*))))

(defun cheap-type-alist-and-pot-lst
  (cl ens wrld state)
  (mv-let (contradictionp type-alist ttree)
    (type-alist-clause cl nil nil nil ens wrld nil nil)
    (cond ((or (tagged-objectsp 'assumption ttree)
         (tagged-objectsp 'fc-derivation ttree)) (mv (er hard
            'cheap-type-alist-and-pot-lst
            "Assumptions and/or fc-derivations were found in the ~
                     ttree constructed by CHEAP-TYPE-ALIST-AND-POT-LST.  This ~
                     is supposedly impossible!")
          nil
          nil))
      (contradictionp (mv t nil nil))
      (t (mv-let (new-step-limit provedp pot-lst)
          (setup-simplify-clause-pot-lst1 cl
            nil
            type-alist
            (make-rcnst ens
              wrld
              state
              :force-info 'weak
              :heavy-linearp nil)
            wrld
            state
            *default-step-limit*)
          (declare (ignore new-step-limit))
          (cond (provedp (mv t nil nil))
            (t (mv nil type-alist pot-lst))))))))

(defun tau-clausep
  (clause ens wrld state calist)
  (cond ((enabled-numep *tau-system-xnume* ens) (mv-let (contradictionp type-alist pot-lst)
        (cheap-type-alist-and-pot-lst clause ens wrld state)
        (cond (contradictionp (mv t *tau-ttree* calist))
          (t (let ((triples (merge-sort-car-< (annotate-clause-with-key-numbers clause
                     (len clause)
                     0
                     wrld))))
              (mv-let (flg calist)
                (tau-clause1p triples
                  nil
                  type-alist
                  pot-lst
                  ens
                  wrld
                  calist)
                (cond ((eq flg t) (mv t *tau-ttree* calist))
                  (t (mv nil nil calist)))))))))
    (t (mv nil nil calist))))

(defun tau-clausep-lst-rec
  (clauses ens wrld ans ttree state calist)
  (cond ((endp clauses) (mv (revappend ans nil) ttree calist))
    (t (mv-let (flg1 ttree1 calist)
        (tau-clausep (car clauses) ens wrld state calist)
        (prog2$ (time-tracker :tau :print?)
          (tau-clausep-lst-rec (cdr clauses)
            ens
            wrld
            (if flg1
              ans
              (cons (car clauses) ans))
            (or ttree1 ttree)
            state
            calist))))))

(defun tau-clausep-lst
  (clauses ens wrld ans ttree state calist)
  (prog2$ (time-tracker :tau :start!)
    (mv-let (clauses ttree calist)
      (tau-clausep-lst-rec clauses
        ens
        wrld
        ans
        ttree
        state
        calist)
      (prog2$ (time-tracker :tau :stop) (mv clauses ttree calist)))))

(defun prettyify-clause-simple
  (cl)
  (cond ((null cl) nil)
    ((null (cdr cl)) cl)
    ((null (cddr cl)) (fcons-term* 'implies (dumb-negate-lit (car cl)) (cadr cl)))
    (t (fcons-term* 'implies
        (conjoin (dumb-negate-lit-lst (butlast cl 1)))
        (car (last cl))))))

(defun preprocess-clause
  (cl hist pspv wrld state step-limit)
  (let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
    (mv-let (built-in-clausep ttree)
      (cond ((or (eq (car (car hist)) 'simplify-clause)
           (eq (car (car hist)) 'settled-down-clause)) (mv nil nil))
        (t (built-in-clausep 'preprocess-clause
            cl
            (access rewrite-constant rcnst :current-enabled-structure)
            (access rewrite-constant rcnst :oncep-override)
            wrld
            state)))
      (cond (built-in-clausep (mv step-limit 'hit nil ttree pspv))
        (t (let ((term (disjoin (expand-any-final-implies cl wrld))))
            (sl-let (term ttree)
              (expand-abbreviations term
                nil
                *geneqv-iff*
                nil
                (access rewrite-constant
                  rcnst
                  :fns-to-be-ignored-by-rewrite)
                (rewrite-stack-limit wrld)
                step-limit
                (access rewrite-constant rcnst :current-enabled-structure)
                wrld
                state
                nil)
              (sl-let (clauses ttree)
                (clausify-input term
                  (access rewrite-constant
                    rcnst
                    :fns-to-be-ignored-by-rewrite)
                  (access rewrite-constant rcnst :current-enabled-structure)
                  wrld
                  state
                  ttree
                  step-limit)
                (let ((tau-completion-alist (access prove-spec-var pspv :tau-completion-alist)))
                  (mv-let (clauses1 ttree1 new-tau-completion-alist)
                    (if (or (null hist)
                        (null (cdr hist))
                        (null (cddr hist))
                        (eq (car (car hist)) 'settled-down-clause))
                      (let ((ens (access rewrite-constant rcnst :current-enabled-structure)))
                        (if (enabled-numep *tau-system-xnume* ens)
                          (tau-clausep-lst clauses
                            ens
                            wrld
                            nil
                            nil
                            state
                            tau-completion-alist)
                          (mv clauses nil tau-completion-alist)))
                      (mv clauses nil tau-completion-alist))
                    (let ((pspv (if (equal tau-completion-alist new-tau-completion-alist)
                           pspv
                           (change prove-spec-var
                             pspv
                             :tau-completion-alist new-tau-completion-alist))))
                      (cond ((equal clauses1 (list cl)) (mv step-limit 'miss nil nil nil))
                        ((and (consp clauses1)
                           (null (cdr clauses1))
                           (no-op-histp hist)
                           (equal (prettyify-clause-simple (car clauses1))
                             (access prove-spec-var pspv :user-supplied-term))) (mv step-limit
                            'hit
                            clauses1
                            (add-to-tag-tree 'hidden-clause
                              t
                              (cons-tag-trees ttree1 ttree))
                            pspv))
                        (t (mv step-limit
                            'hit
                            clauses1
                            (cons-tag-trees ttree1 ttree)
                            pspv))))))))))))))

(defun tilde-*-preprocess-phrase
  (ttree)
  (mv-let (message-lst char-alist)
    (tilde-*-simp-phrase1 (extract-and-classify-lemmas ttree '(implies not iff) nil)
      t)
    (list* "case analysis"
      "~@*"
      "~@* and "
      "~@*, "
      message-lst
      char-alist)))

(defun tilde-*-raw-preprocess-phrase
  (ttree punct)
  (let ((runes (all-runes-in-ttree ttree nil)))
    (mv-let (message-lst char-alist)
      (tilde-*-raw-simp-phrase1 runes
        nil
        punct
        '(implies not iff)
        ""
        nil)
      (list* (concatenate 'string
          "case analysis"
          (case punct (#\, ",") (#\. ".") (otherwise "")))
        "~@*"
        "~@* and "
        "~@*, "
        message-lst
        char-alist))))

(defun preprocess-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal pspv))
  (let ((raw-proof-format (f-get-global 'raw-proof-format state)))
    (cond ((tag-tree-occur 'hidden-clause t ttree) state)
      ((and raw-proof-format (null clauses)) (fms "But preprocess reduces the conjecture to T, by ~*0~|"
          (list (cons #\0 (tilde-*-raw-preprocess-phrase ttree #\.)))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      ((null clauses) (fms "But we reduce the conjecture to T, by ~*0.~|"
          (list (cons #\0 (tilde-*-preprocess-phrase ttree)))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      (raw-proof-format (fms "Preprocess reduces the conjecture to ~#1~[~x2~/the ~
                 following~/the following ~n3 conjectures~], by ~*0~|"
          (list (cons #\0 (tilde-*-raw-preprocess-phrase ttree #\.))
            (cons #\1 (zero-one-or-more clauses))
            (cons #\2 t)
            (cons #\3 (length clauses)))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      (t (fms "By ~*0 we reduce the conjecture to~#1~[~x2.~/~/ the ~
                 following ~n3 conjectures.~]~|"
          (list (cons #\0 (tilde-*-preprocess-phrase ttree))
            (cons #\1 (zero-one-or-more clauses))
            (cons #\2 t)
            (cons #\3 (length clauses)))
          (proofs-co state)
          state
          (term-evisc-tuple nil state))))))

(defun select-x-cl-set
  (cl-set induct-hint-val)
  (cond ((null induct-hint-val) cl-set)
    ((equal induct-hint-val *t*) cl-set)
    (t (list (list induct-hint-val)))))

(defun unchangeables
  (formals args quick-block-info subset ans)
  (cond ((null formals) ans)
    ((and (member-eq (car formals) subset)
       (eq (car quick-block-info) 'unchanging)) (unchangeables (cdr formals)
        (cdr args)
        (cdr quick-block-info)
        subset
        (all-vars1 (car args) ans)))
    (t (unchangeables (cdr formals)
        (cdr args)
        (cdr quick-block-info)
        subset
        ans))))

(defun changeables
  (formals args quick-block-info subset ans)
  (cond ((null formals) ans)
    ((and (member-eq (car formals) subset)
       (not (eq (car quick-block-info) 'unchanging))) (changeables (cdr formals)
        (cdr args)
        (cdr quick-block-info)
        subset
        (cons (car args) ans)))
    (t (changeables (cdr formals)
        (cdr args)
        (cdr quick-block-info)
        subset
        ans))))

(defun sound-induction-principle-mask1
  (formals args
    quick-block-info
    subset
    unchangeables
    changeables)
  (cond ((null formals) nil)
    (t (let ((var (car formals)) (arg (car args))
          (q (car quick-block-info)))
        (mv-let (mask-ele new-unchangeables new-changeables)
          (cond ((member-eq var subset) (cond ((eq q 'unchanging) (mv 'unchangeable unchangeables changeables))
                (t (mv 'changeable unchangeables changeables))))
            ((and (variablep arg) (eq q 'unchanging)) (cond ((member-eq arg changeables) (mv nil unchangeables changeables))
                (t (mv 'unchangeable
                    (add-to-set-eq arg unchangeables)
                    changeables))))
            ((and (variablep arg)
               (not (member-eq arg changeables))
               (not (member-eq arg unchangeables))) (mv 'changeable unchangeables (cons arg changeables)))
            (t (mv nil unchangeables changeables)))
          (cons mask-ele
            (sound-induction-principle-mask1 (cdr formals)
              (cdr args)
              (cdr quick-block-info)
              subset
              new-unchangeables
              new-changeables)))))))

(defun sound-induction-principle-mask
  (term formals quick-block-info subset)
  (let ((unchangeables (unchangeables formals
         (fargs term)
         quick-block-info
         subset
         nil)) (changeables (changeables formals
          (fargs term)
          quick-block-info
          subset
          nil)))
    (cond ((or (not (no-duplicatesp-equal changeables))
         (not (all-variablep changeables))
         (intersectp-eq changeables unchangeables)) nil)
      (t (sound-induction-principle-mask1 formals
          (fargs term)
          quick-block-info
          subset
          unchangeables
          changeables)))))

(defun count-non-nils
  (lst)
  (cond ((null lst) 0)
    ((car lst) (1+ (count-non-nils (cdr lst))))
    (t (count-non-nils (cdr lst)))))

(defun controllers
  (formals args subset ans)
  (cond ((null formals) ans)
    ((member (car formals) subset) (controllers (cdr formals)
        (cdr args)
        subset
        (all-vars1 (car args) ans)))
    (t (controllers (cdr formals) (cdr args) subset ans))))

(defun changed/unchanged-vars
  (x args mask ans)
  (cond ((null mask) ans)
    ((eq (car mask) x) (changed/unchanged-vars x
        (cdr args)
        (cdr mask)
        (all-vars1 (car args) ans)))
    (t (changed/unchanged-vars x (cdr args) (cdr mask) ans))))

(defun tests-and-alists/alist
  (alist args mask call-args)
  (cond ((null mask) nil)
    ((null (car mask)) (tests-and-alists/alist alist
        (cdr args)
        (cdr mask)
        (cdr call-args)))
    ((eq (car mask) 'changeable) (cons (cons (car args) (sublis-var alist (car call-args)))
        (tests-and-alists/alist alist
          (cdr args)
          (cdr mask)
          (cdr call-args))))
    (t (let ((vars (all-vars (car args))))
        (append (pairlis$ vars vars)
          (tests-and-alists/alist alist
            (cdr args)
            (cdr mask)
            (cdr call-args)))))))

(defun tests-and-alists/alists
  (alist args mask calls)
  (cond ((null calls) nil)
    (t (cons (tests-and-alists/alist alist args mask (fargs (car calls)))
        (tests-and-alists/alists alist args mask (cdr calls))))))

(defun tests-and-alists
  (alist args mask tc)
  (make tests-and-alists
    :tests (sublis-var-lst alist (access tests-and-calls tc :tests))
    :alists (tests-and-alists/alists alist
      args
      mask
      (access tests-and-calls tc :calls))))

(defun tests-and-alists-lst
  (alist args mask machine)
  (cond ((null machine) nil)
    (t (cons (tests-and-alists alist args mask (car machine))
        (tests-and-alists-lst alist args mask (cdr machine))))))

(defun flesh-out-induction-principle
  (term formals justification mask machine xterm ttree)
  (make candidate
    :score (/ (count-non-nils mask) (length mask))
    :controllers (controllers formals
      (fargs term)
      (access justification justification :subset)
      nil)
    :changed-vars (changed/unchanged-vars 'changeable (fargs term) mask nil)
    :unchangeable-vars (changed/unchanged-vars 'unchangeable (fargs term) mask nil)
    :tests-and-alists-lst (tests-and-alists-lst (pairlis$ formals (fargs term))
      (fargs term)
      mask
      machine)
    :justification justification
    :induction-term term
    :xinduction-term xterm
    :other-terms nil
    :xother-terms nil
    :xancestry nil
    :ttree ttree))

(defun formal-alist-to-alist-on-vars
  (term)
  (cond ((variablep term) (mv nil nil))
    ((equal term *nil*) (mv t nil))
    (t (mv-let (flg pair rest)
        (formal-cons-to-components term)
        (cond ((null flg) (mv nil nil))
          (t (mv-let (flg key val)
              (formal-cons-to-components pair)
              (cond ((null flg) (mv nil nil))
                ((not (quotep key)) (mv nil nil))
                (t (mv-let (flg alist)
                    (formal-alist-to-alist-on-vars rest)
                    (cond ((null flg) (mv nil nil))
                      (t (mv t
                          (cons (cons (unquote key) (eliminate-cdr-assoc-eq-safe val))
                            alist))))))))))))))

(defun decompile-formal-do$-triple
  (formals term)
  (mv-let (flg formal-exit-flg term1)
    (formal-cons-to-components term)
    (cond ((null flg) (mv nil nil))
      (t (mv-let (flg formal-val term2)
          (formal-cons-to-components term1)
          (declare (ignore formal-val))
          (cond ((null flg) (mv nil nil))
            (t (mv-let (flg formal-alist term3)
                (formal-cons-to-components term2)
                (cond ((null flg) (mv nil nil))
                  ((not (equal term3 *nil*)) (mv nil nil))
                  (t (mv-let (flg alist)
                      (formal-alist-to-alist-on-vars formal-alist)
                      (cond ((null flg) (mv nil nil))
                        ((not (equal (strip-cars alist) formals)) (mv nil nil))
                        (t (cond ((eq (unquote formal-exit-flg) nil) (mv t (sublis-var alist (cons *do$-induction-fn* formals))))
                            (t (mv t (cons 'list formals)))))))))))))))))

(defun decompile-do$-body
  (formals term)
  (cond ((variablep term) (mv nil nil))
    ((fquotep term) (decompile-formal-do$-triple formals term))
    ((eq (ffn-symb term) 'if) (mv-let (flg tb)
        (decompile-do$-body formals (fargn term 2))
        (cond ((null flg) (mv nil nil))
          (t (mv-let (flg fb)
              (decompile-do$-body formals (fargn term 3))
              (cond ((null flg) (mv nil nil))
                (t (mv t
                    (list 'if
                      (eliminate-cdr-assoc-eq-safe (fargn term 1))
                      tb
                      fb)))))))))
    (t (decompile-formal-do$-triple formals term))))

(defun quoted-lambda-to-body
  (x)
  (case-match x
    (('quote ('lambda ('alist) body)) (mv t body))
    (& (mv nil nil))))

(defun decompile-do$
  (term wrld)
  (let ((cleaned-term (possibly-clean-up-dirty-lambda-objects :all (remove-guard-holders-weak term (remove-guard-holders-lamp))
         wrld
         (remove-guard-holders-lamp))))
    (mv-let (flg formal-mterm)
      (quoted-lambda-to-body (fargn cleaned-term 1))
      (cond ((null flg) nil)
        (t (mv-let (flg alist)
            (formal-alist-to-alist-on-vars (fargn cleaned-term 2))
            (let* ((formals (strip-cars alist)) (call (cons *do$-induction-fn* (strip-cdrs alist))))
              (cond ((null flg) nil)
                (t (mv-let (flg formal-body)
                    (quoted-lambda-to-body (fargn cleaned-term 3))
                    (cond ((null flg) nil)
                      (t (mv-let (flg body)
                          (decompile-do$-body formals formal-body)
                          (cond ((null flg) nil)
                            (t (let ((mterm (eliminate-cdr-assoc-eq-safe formal-mterm)))
                                (list formals call mterm body)))))))))))))))))

(defun intrinsic-suggested-induction-cand1
  (induction-rune term
    formals
    quick-block-info
    justification
    machine
    xterm
    ttree)
  (let ((mask (sound-induction-principle-mask term
         formals
         quick-block-info
         (access justification justification :subset))))
    (cond (mask (list (flesh-out-induction-principle term
            formals
            justification
            mask
            machine
            xterm
            (push-lemma induction-rune ttree))))
      (t nil))))

(defun get-ruler-extenders1
  (r edcls default ctx wrld state)
  (cond ((null edcls) (value (if (eq r *no-ruler-extenders*)
          default
          r)))
    ((eq (caar edcls) 'xargs) (let ((temp (assoc-keyword :ruler-extenders (cdar edcls))))
        (cond ((null temp) (get-ruler-extenders1 r (cdr edcls) default ctx wrld state))
          (t (let ((r0 (cadr temp)))
              (cond ((eq r *no-ruler-extenders*) (er-let* ((r1 (cond ((eq r0 :basic) (value *basic-ruler-extenders*))
                         ((eq r0 :lambdas) (value *basic-ruler-extenders-plus-lambdas*))
                         ((eq r0 :all) (value :all))
                         (t (er-progn (chk-ruler-extenders r0 soft ctx wrld) (value r0))))))
                    (get-ruler-extenders1 r1 (cdr edcls) default ctx wrld state)))
                ((equal r r0) (get-ruler-extenders1 r (cdr edcls) default ctx wrld state))
                (t (er soft
                    ctx
                    "It is illegal to declare two different ~
                             ruler-extenders for the admission of a single ~
                             function.  But you have specified ~
                             :RULER-EXTENDERS ~x0 and :RULER-EXTENDERS ~x1."
                    r
                    r0))))))))
    (t (get-ruler-extenders1 r (cdr edcls) default ctx wrld state))))

(defun get-ruler-extenders2
  (lst default ctx wrld state)
  (cond ((null lst) (value nil))
    (t (er-let* ((r (get-ruler-extenders1 *no-ruler-extenders*
             (fourth (car lst))
             default
             ctx
             wrld
             state)) (rst (get-ruler-extenders2 (cdr lst) default ctx wrld state)))
        (value (cons r rst))))))

(defun default-ruler-extenders
  (wrld)
  (default-ruler-extenders-from-table (table-alist 'acl2-defaults-table wrld)))

(defun get-ruler-extenders-lst
  (symbol-class lst ctx wrld state)
  (cond ((eq symbol-class :program) (value (make-list (length lst)
          :initial-element *no-ruler-extenders*)))
    (t (get-ruler-extenders2 lst
        (default-ruler-extenders wrld)
        ctx
        wrld
        state))))

(defun member-eq-all
  (a lst)
  (or (eq lst :all) (member-eq a lst)))

(defun termination-machine1
  (tests calls ans)
  (cond ((null calls) ans)
    (t (termination-machine1 tests
        (cdr calls)
        (cons (make tests-and-call :tests tests :call (car calls))
          ans)))))

(defun term-equated-to-constant
  (term)
  (case-match term
    ((rel x y) (cond ((or (eq rel 'equal) (member-eq rel *equality-aliases*)) (cond ((quotep x) (mv y x))
            ((quotep y) (mv x y))
            (t (mv nil nil))))
        (t (mv nil nil))))
    (& (mv nil nil))))

(defun term-equated-to-constant-in-termlist
  (lst)
  (cond ((endp lst) (mv nil nil))
    (t (mv-let (var const)
        (term-equated-to-constant (car lst))
        (cond (var (mv var const))
          (t (term-equated-to-constant-in-termlist (cdr lst))))))))

(defun simplify-tests
  (var const tests)
  (cond ((endp tests) (mv nil nil))
    (t (mv-let (changedp rest)
        (simplify-tests var const (cdr tests))
        (mv-let (flg term)
          (strip-not (car tests))
          (mv-let (var2 const2)
            (term-equated-to-constant term)
            (cond ((and flg (equal var var2) (not (equal const const2))) (mv t rest))
              (changedp (mv t (cons (car tests) rest)))
              (t (mv nil tests)))))))))

(defun add-test-smart
  (test tests)
  (mv-let (term const)
    (term-equated-to-constant test)
    (cons test
      (cond (term (mv-let (changedp new-tests)
            (simplify-tests term const tests)
            (if changedp
              new-tests
              tests)))
        (t tests)))))

(defun choke-on-loop$-recursion
  (loop$-recursion-checkedp names body sysfn)
  (cond ((or loop$-recursion-checkedp (cdr names)) nil)
    (t (choke-on-loop$-recursion1 (car names) body sysfn))))

(defun termination-machine
  (loop$-recursion-checkedp loop$-recursion
    names
    formals
    body
    alist
    tests
    ruler-extenders)
  (prog2$ (choke-on-loop$-recursion loop$-recursion-checkedp
      names
      body
      'termination-machine)
    (termination-machine-rec loop$-recursion
      names
      body
      alist
      tests
      ruler-extenders
      (if (and loop$-recursion-checkedp loop$-recursion)
        formals
        nil))))

(defun termination-machines
  (loop$-recursion-checkedp loop$-recursion
    names
    arglists
    bodies
    ruler-extenders-lst)
  (cond ((null bodies) nil)
    (t (cons (termination-machine loop$-recursion-checkedp
          loop$-recursion
          names
          (car arglists)
          (car bodies)
          nil
          nil
          (car ruler-extenders-lst))
        (termination-machines loop$-recursion-checkedp
          loop$-recursion
          names
          (cdr arglists)
          (cdr bodies)
          (cdr ruler-extenders-lst))))))

(defun quick-block-initial-settings
  (formals)
  (cond ((null formals) nil)
    (t (cons 'un-initialized
        (quick-block-initial-settings (cdr formals))))))

(defun quick-block-info1
  (var term)
  (cond ((eq var term) 'unchanging)
    ((dumb-occur var term) 'self-reflexive)
    (t 'questionable)))

(defun quick-block-info2
  (setting info1)
  (case setting
    (questionable 'questionable)
    (un-initialized info1)
    (otherwise (cond ((eq setting info1) setting) (t 'questionable)))))

(defun quick-block-settings
  (settings formals args)
  (cond ((null settings) nil)
    (t (cons (quick-block-info2 (car settings)
          (quick-block-info1 (car formals) (car args)))
        (quick-block-settings (cdr settings)
          (cdr formals)
          (cdr args))))))

(defun quick-block-down-t-machine
  (name settings formals t-machine)
  (cond ((null t-machine) settings)
    ((not (eq name
         (ffn-symb (access tests-and-call (car t-machine) :call)))) (er hard
        'quick-block-down-t-machine
        "When you add induction on mutually recursive functions don't ~
              forget about QUICK-BLOCK-INFO!"))
    (t (quick-block-down-t-machine name
        (quick-block-settings settings
          formals
          (fargs (access tests-and-call (car t-machine) :call)))
        formals
        (cdr t-machine)))))

(defun quick-block-info
  (name formals t-machine)
  (quick-block-down-t-machine name
    (quick-block-initial-settings formals)
    formals
    t-machine))

(defun sublis-tests-rev
  (test-alist acc)
  (cond ((endp test-alist) acc)
    (t (sublis-tests-rev (cdr test-alist)
        (let* ((test (caar test-alist)) (alist (cdar test-alist))
            (inst-test (cond ((or (eq alist :no-calls) (null alist)) test)
                (t (sublis-expr alist test)))))
          (cons inst-test acc))))))

(defun all-calls-test-alist
  (names test-alist acc)
  (cond ((endp test-alist) acc)
    (t (all-calls-test-alist names
        (cdr test-alist)
        (let* ((test (caar test-alist)) (alist (cdar test-alist)))
          (cond ((eq alist :no-calls) acc)
            (t (all-calls names test alist acc))))))))

(defun union-equal-to-end
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (cond ((intersectp-equal x y) (append x (set-difference-equal y x)))
    (t (append x y))))

(defun cross-tests-and-calls3
  (tacs tacs-lst)
  (cond ((endp tacs-lst) nil)
    (t (let ((tests1 (access tests-and-calls tacs :tests)) (tests2 (access tests-and-calls (car tacs-lst) :tests)))
        (cond ((some-element-member-complement-term tests1 tests2) (cross-tests-and-calls3 tacs (cdr tacs-lst)))
          (t (cons (make tests-and-calls
                :tests (union-equal-to-end tests1 tests2)
                :calls (union-equal (access tests-and-calls tacs :calls)
                  (access tests-and-calls (car tacs-lst) :calls)))
              (cross-tests-and-calls3 tacs (cdr tacs-lst)))))))))

(defun cross-tests-and-calls2
  (tacs-lst1 tacs-lst2)
  (cond ((endp tacs-lst1) nil)
    (t (append (cross-tests-and-calls3 (car tacs-lst1) tacs-lst2)
        (cross-tests-and-calls2 (cdr tacs-lst1) tacs-lst2)))))

(defun cross-tests-and-calls1
  (tacs-lst-lst acc)
  (cond ((endp tacs-lst-lst) acc)
    (t (cross-tests-and-calls1 (cdr tacs-lst-lst)
        (cross-tests-and-calls2 (car tacs-lst-lst) acc)))))

(defun cross-tests-and-calls
  (names top-test-alist top-calls tacs-lst-lst)
  (let ((full-tacs-lst-lst (append tacs-lst-lst
         (list (list (make tests-and-calls
               :tests (sublis-tests-rev top-test-alist nil)
               :calls (all-calls-test-alist names top-test-alist top-calls)))))))
    (cross-tests-and-calls1 (cdr full-tacs-lst-lst)
      (car full-tacs-lst-lst))))

(defun mark-loop$-recursion-nugget
  (nugget)
  `(return-last 'progn 'loop$-recursion-nugget ,NUGGET))

(defun marked-loop$-recursion-nuggetp
  (term)
  (and (nvariablep term)
    (not (fquotep term))
    (eq (ffn-symb term) 'return-last)
    (quotep (fargn term 1))
    (eq (unquote (fargn term 1)) 'progn)
    (quotep (fargn term 2))
    (eq (unquote (fargn term 2)) 'loop$-recursion-nugget)))

(defun simplify-tests-and-calls
  (tc)
  (let* ((tests0 (remove-guard-holders-weak-lst (access tests-and-calls tc :tests)
         nil)))
    (mv-let (var const)
      (term-equated-to-constant-in-termlist tests0)
      (let ((tests (cond (var (mv-let (changedp tests)
                 (simplify-tests var const tests0)
                 (declare (ignore changedp))
                 tests))
             (t tests0))))
        (make tests-and-calls
          :tests tests
          :calls (remove-guard-holders-weak-lst (access tests-and-calls tc :calls)
            nil))))))

(defun simplify-tests-and-calls-lst
  (tc-list)
  (cond ((endp tc-list) nil)
    (t (cons (simplify-tests-and-calls (car tc-list))
        (simplify-tests-and-calls-lst (cdr tc-list))))))

(defun induction-machine-for-fn
  (names body ruler-extenders)
  (mv-let (flg ans)
    (induction-machine-for-fn1 names
      body
      nil
      nil
      nil
      ruler-extenders
      nil)
    (declare (ignore flg))
    (simplify-tests-and-calls-lst ans)))

(defun intrinsic-suggested-induction-cand-do$
  (term wrld)
  (let ((four-tuple (decompile-do$ term wrld)))
    (case-match four-tuple
      ((formals call measure body) (let* ((ruler-extenders (default-ruler-extenders wrld)) (t-machine (termination-machine t
                nil
                (list *do$-induction-fn*)
                (list formals)
                body
                nil
                nil
                ruler-extenders))
            (quick-block-info (quick-block-info *do$-induction-fn* formals t-machine))
            (formals-to-actuals-alist (pairlis$ formals (fargs call)))
            (justification (make justification
                :subset (all-vars (sublis-var formals-to-actuals-alist measure))
                :subversive-p nil
                :mp 'lexp
                :rel 'l<
                :measure `(lex-fix ,(SUBLIS-VAR FORMALS-TO-ACTUALS-ALIST MEASURE))
                :ruler-extenders ruler-extenders))
            (induction-machine (induction-machine-for-fn (list *do$-induction-fn*)
                body
                ruler-extenders)))
          (intrinsic-suggested-induction-cand1 '(:induction do$)
            call
            formals
            quick-block-info
            justification
            induction-machine
            term
            nil)))
      (& nil))))

(defun intrinsic-suggested-induction-cand
  (induction-rune term
    formals
    quick-block-info
    justification
    machine
    xterm
    ttree
    wrld)
  (cond ((and (nvariablep term)
       (not (fquotep term))
       (eq (ffn-symb term) 'do$)) (or (intrinsic-suggested-induction-cand-do$ term wrld)
        (intrinsic-suggested-induction-cand1 induction-rune
          term
          formals
          quick-block-info
          justification
          machine
          xterm
          ttree)))
    (t (intrinsic-suggested-induction-cand1 induction-rune
        term
        formals
        quick-block-info
        justification
        machine
        xterm
        ttree))))

(defun relieve-induction-condition-terms
  (rune pattern terms alist type-alist ens wrld)
  (cond ((endp terms) t)
    ((or (variablep (car terms))
       (fquotep (car terms))
       (not (eq (ffn-symb (car terms)) 'synp))) (mv-let (ts ttree1)
        (type-set (sublis-var alist (car terms))
          t
          nil
          type-alist
          ens
          wrld
          nil
          nil
          nil)
        (declare (ignore ttree1))
        (cond ((ts-intersectp *ts-nil* ts) nil)
          (t (relieve-induction-condition-terms rune
              pattern
              (cdr terms)
              alist
              type-alist
              ens
              wrld)))))
    (t (mv-let (erp val)
        (ev-w (get-evg (fargn (car terms) 3)
            'relieve-induction-condition-terms)
          alist
          wrld
          nil
          t
          nil
          nil
          nil)
        (cond (erp (er hard
              'relieve-induction-condition-terms
              "The form ~x0 caused the error, ~@1.  That SYNTAXP form ~
                 occurs as a :condition governing the :induction rule ~x2, ~
                 which we tried to fire after matching the :pattern ~x3 using ~
                 the unifying substitution ~x4."
              (get-evg (fargn (car terms) 2)
                'relieve-induction-condition-terms)
              val
              rune
              pattern
              alist))
          (val (relieve-induction-condition-terms rune
              pattern
              (cdr terms)
              alist
              type-alist
              ens
              wrld)))))))

(defun get-induction-cands-from-cl-set1
  (cl-set ens oncep-override wrld state ans)
  (cond ((null cl-set) ans)
    (t (mv-let (contradictionp type-alist fc-pairs)
        (forward-chain-top 'induct
          (car cl-set)
          nil
          t
          nil
          wrld
          ens
          oncep-override
          state)
        (declare (ignore contradictionp fc-pairs))
        (get-induction-cands-lst (car cl-set)
          type-alist
          ens
          wrld
          (get-induction-cands-from-cl-set1 (cdr cl-set)
            ens
            oncep-override
            wrld
            state
            ans))))))

(defun get-induction-cands-from-cl-set
  (cl-set pspv wrld state)
  (let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
    (get-induction-cands-from-cl-set1 cl-set
      (access rewrite-constant rcnst :current-enabled-structure)
      (access rewrite-constant rcnst :oncep-override)
      wrld
      state
      nil)))

(defun flush-cand1-down-cand2
  (cand1 cand2)
  (cond ((and (subsetp-eq (access candidate cand1 :changed-vars)
         (access candidate cand2 :changed-vars))
       (subsetp-eq (access candidate cand1 :unchangeable-vars)
         (access candidate cand2 :unchangeable-vars))
       (pigeon-holep (access candidate cand1 :tests-and-alists-lst)
         (access candidate cand2 :tests-and-alists-lst)
         nil
         'tests-and-alists-fitp)) (change candidate
        cand2
        :score (+ (access candidate cand1 :score)
          (access candidate cand2 :score))
        :controllers (union-eq (access candidate cand1 :controllers)
          (access candidate cand2 :controllers))
        :other-terms (add-to-set-equal (access candidate cand1 :induction-term)
          (union-equal (access candidate cand1 :other-terms)
            (access candidate cand2 :other-terms)))
        :xother-terms (add-to-set-equal (access candidate cand1 :xinduction-term)
          (union-equal (access candidate cand1 :xother-terms)
            (access candidate cand2 :xother-terms)))
        :ttree (cons-tag-trees (access candidate cand1 :ttree)
          (access candidate cand2 :ttree))))
    (t nil)))

(defun flush-candidates
  (cand1 cand2)
  (or (flush-cand1-down-cand2 cand1 cand2)
    (flush-cand1-down-cand2 cand2 cand1)))

(defun alists-agreep
  (alist1 alist2 vars)
  (cond ((null vars) t)
    ((equal (let ((temp (assoc-eq (car vars) alist1)))
         (cond (temp (cdr temp)) (t (car vars))))
       (let ((temp (assoc-eq (car vars) alist2)))
         (cond (temp (cdr temp)) (t (car vars))))) (alists-agreep alist1 alist2 (cdr vars)))
    (t nil)))

(defun irreconcilable-alistsp
  (alist1 alist2)
  (cond ((null alist1) nil)
    (t (let ((temp (assoc-eq (caar alist1) alist2)))
        (cond ((null temp) (irreconcilable-alistsp (cdr alist1) alist2))
          ((equal (cdar alist1) (cdr temp)) (irreconcilable-alistsp (cdr alist1) alist2))
          (t t))))))

(defun affinity
  (aff alist1 alist2 vars)
  (and (alists-agreep alist1 alist2 vars)
    (eq (irreconcilable-alistsp alist1 alist2)
      (eq aff 'antagonists))))

(defun member-affinity
  (aff alist alist-lst vars)
  (cond ((null alist-lst) nil)
    ((affinity aff alist (car alist-lst) vars) t)
    (t (member-affinity aff alist (cdr alist-lst) vars))))

(defun occur-affinity
  (aff alist lst vars)
  (cond ((null lst) nil)
    ((member-affinity aff
       alist
       (access tests-and-alists (car lst) :alists)
       vars) t)
    (t (occur-affinity aff alist (cdr lst) vars))))

(defun some-occur-affinity
  (aff alists lst vars)
  (cond ((null alists) nil)
    (t (or (occur-affinity aff (car alists) lst vars)
        (some-occur-affinity aff (cdr alists) lst vars)))))

(defun all-occur-affinity
  (aff alists lst vars)
  (cond ((null alists) t)
    (t (and (occur-affinity aff (car alists) lst vars)
        (all-occur-affinity aff (cdr alists) lst vars)))))

(defun contains-affinity
  (aff lst vars)
  (cond ((null lst) nil)
    ((member-affinity aff (car lst) (cdr lst) vars) t)
    (t (contains-affinity aff (cdr lst) vars))))

(defun antagonistic-tests-and-alists-lstp
  (lst vars)
  (cond ((null lst) nil)
    (t (or (contains-affinity 'antagonists
          (access tests-and-alists (car lst) :alists)
          vars)
        (some-occur-affinity 'antagonists
          (access tests-and-alists (car lst) :alists)
          (cdr lst)
          vars)
        (antagonistic-tests-and-alists-lstp (cdr lst) vars)))))

(defun antagonistic-tests-and-alists-lstsp
  (lst1 lst2 vars)
  (cond ((null lst1) nil)
    (t (or (some-occur-affinity 'antagonists
          (access tests-and-alists (car lst1) :alists)
          lst2
          vars)
        (antagonistic-tests-and-alists-lstsp (cdr lst1) lst2 vars)))))

(defun every-alist1-matedp
  (lst1 lst2 vars)
  (cond ((null lst1) t)
    (t (and (all-occur-affinity 'mates
          (access tests-and-alists (car lst1) :alists)
          lst2
          vars)
        (every-alist1-matedp (cdr lst1) lst2 vars)))))

(defun merge-alist1-into-alist2
  (alist1 alist2 vars)
  (cond ((alists-agreep alist1 alist2 vars) (union-equal alist1 alist2))
    (t alist2)))

(defun merge-alist1-lst-into-alist2
  (alist1-lst alist2 vars)
  (cond ((null alist1-lst) alist2)
    (t (merge-alist1-lst-into-alist2 (cdr alist1-lst)
        (merge-alist1-into-alist2 (car alist1-lst) alist2 vars)
        vars))))

(defun merge-lst1-into-alist2
  (lst1 alist2 vars)
  (cond ((null lst1) alist2)
    (t (merge-lst1-into-alist2 (cdr lst1)
        (merge-alist1-lst-into-alist2 (access tests-and-alists (car lst1) :alists)
          alist2
          vars)
        vars))))

(defun merge-lst1-into-alist2-lst
  (lst1 alist2-lst vars)
  (cond ((null alist2-lst) nil)
    (t (cons (merge-lst1-into-alist2 lst1 (car alist2-lst) vars)
        (merge-lst1-into-alist2-lst lst1 (cdr alist2-lst) vars)))))

(defun merge-lst1-into-lst2
  (lst1 lst2 vars)
  (cond ((null lst2) nil)
    (t (cons (change tests-and-alists
          (car lst2)
          :alists (merge-lst1-into-alist2-lst lst1
            (access tests-and-alists (car lst2) :alists)
            vars))
        (merge-lst1-into-lst2 lst1 (cdr lst2) vars)))))

(defun merge-tests-and-alists-lsts
  (lst1 lst2 vars)
  (cond ((antagonistic-tests-and-alists-lstp lst1 vars) nil)
    ((antagonistic-tests-and-alists-lstsp lst1 lst2 vars) nil)
    ((not (every-alist1-matedp lst1 lst2 vars)) nil)
    (t (merge-lst1-into-lst2 lst1 lst2 vars))))

(defun merge-cand1-into-cand2
  (cand1 cand2)
  (let ((vars (or (intersection-eq (access candidate cand1 :controllers)
           (intersection-eq (access candidate cand2 :controllers)
             (intersection-eq (access candidate cand1 :changed-vars)
               (access candidate cand2 :changed-vars))))
         (intersection-eq (access candidate cand1 :changed-vars)
           (access candidate cand2 :changed-vars)))))
    (cond ((and vars
         (not (intersectp-eq (access candidate cand1 :unchangeable-vars)
             (access candidate cand2 :changed-vars)))
         (not (intersectp-eq (access candidate cand2 :unchangeable-vars)
             (access candidate cand1 :changed-vars)))) (let ((temp (merge-tests-and-alists-lsts (access candidate cand1 :tests-and-alists-lst)
               (access candidate cand2 :tests-and-alists-lst)
               vars)))
          (cond (temp (make candidate
                :score (+ (access candidate cand1 :score)
                  (access candidate cand2 :score))
                :controllers (union-eq (access candidate cand1 :controllers)
                  (access candidate cand2 :controllers))
                :changed-vars (union-eq (access candidate cand1 :changed-vars)
                  (access candidate cand2 :changed-vars))
                :unchangeable-vars (union-eq (access candidate cand1 :unchangeable-vars)
                  (access candidate cand2 :unchangeable-vars))
                :tests-and-alists-lst temp
                :justification (access candidate cand2 :justification)
                :induction-term (access candidate cand2 :induction-term)
                :other-terms (add-to-set-equal (access candidate cand1 :induction-term)
                  (union-equal (access candidate cand1 :other-terms)
                    (access candidate cand2 :other-terms)))
                :xinduction-term (access candidate cand2 :xinduction-term)
                :xother-terms (add-to-set-equal (access candidate cand1 :xinduction-term)
                  (union-equal (access candidate cand1 :xother-terms)
                    (access candidate cand2 :xother-terms)))
                :xancestry (cond ((equal temp (access candidate cand2 :tests-and-alists-lst)) (access candidate cand2 :xancestry))
                  (t (add-to-set-equal (access candidate cand1 :xinduction-term)
                      (union-equal (access candidate cand1 :xancestry)
                        (access candidate cand2 :xancestry)))))
                :ttree (cons-tag-trees (access candidate cand1 :ttree)
                  (access candidate cand2 :ttree))))
            (t nil))))
      (t nil))))

(defun merge-candidates
  (cand1 cand2)
  (or (merge-cand1-into-cand2 cand1 cand2)
    (merge-cand1-into-cand2 cand2 cand1)))

(defun controller-variables1
  (args controller-pocket)
  (cond ((null controller-pocket) nil)
    ((and (car controller-pocket) (variablep (car args))) (add-to-set-eq (car args)
        (controller-variables1 (cdr args) (cdr controller-pocket))))
    (t (controller-variables1 (cdr args) (cdr controller-pocket)))))

(defun controller-variables
  (term controller-alist)
  (controller-variables1 (fargs term)
    (cdr (assoc-eq (ffn-symb term) controller-alist))))

(defun induct-vars1
  (lst wrld)
  (cond ((null lst) nil)
    (t (union-eq (controller-variables (car lst)
          (access def-body
            (original-def-body (ffn-symb (car lst)) wrld)
            :controller-alist))
        (induct-vars1 (cdr lst) wrld)))))

(defun induct-vars
  (cand wrld)
  (induct-vars1 (cons (access candidate cand :induction-term)
      (access candidate cand :other-terms))
    wrld))

(defun vetoedp
  (cand vars lst changed-vars-flg)
  (cond ((null lst) nil)
    ((equal cand (car lst)) (vetoedp cand vars (cdr lst) changed-vars-flg))
    ((and changed-vars-flg
       (intersectp-eq vars
         (access candidate (car lst) :changed-vars))) t)
    ((intersectp-eq vars
       (access candidate (car lst) :unchangeable-vars)) t)
    (t (vetoedp cand vars (cdr lst) changed-vars-flg))))

(defun compute-vetoes1
  (lst cand-lst wrld)
  (cond ((null lst) nil)
    ((vetoedp (car lst)
       (intersection-eq (access candidate (car lst) :changed-vars)
         (induct-vars (car lst) wrld))
       cand-lst
       t) (compute-vetoes1 (cdr lst) cand-lst wrld))
    (t (cons (car lst) (compute-vetoes1 (cdr lst) cand-lst wrld)))))

(defun compute-vetoes2
  (lst cand-lst)
  (cond ((null lst) nil)
    ((vetoedp (car lst)
       (access candidate (car lst) :changed-vars)
       cand-lst
       nil) (compute-vetoes2 (cdr lst) cand-lst))
    (t (cons (car lst) (compute-vetoes2 (cdr lst) cand-lst)))))

(defun compute-vetoes
  (cand-lst wrld)
  (or (compute-vetoes1 cand-lst cand-lst wrld)
    (compute-vetoes2 cand-lst cand-lst)
    cand-lst))

(defun induction-complexity1
  (lst wrld)
  (cond ((null lst) 0)
    ((getpropc (ffn-symb (car lst))
       'primitive-recursive-defunp
       nil
       wrld) (induction-complexity1 (cdr lst) wrld))
    (t (1+ (induction-complexity1 (cdr lst) wrld)))))

(defun maximal-elements-apply
  (fn x wrld)
  (case fn
    (induction-complexity (induction-complexity1 (cons (access candidate x :induction-term)
          (access candidate x :other-terms))
        wrld))
    (score (access candidate x :score))
    (otherwise 0)))

(defun maximal-elements1
  (lst winners maximum fn wrld)
  (cond ((null lst) winners)
    (t (let ((temp (maximal-elements-apply fn (car lst) wrld)))
        (cond ((> temp maximum) (maximal-elements1 (cdr lst) (list (car lst)) temp fn wrld))
          ((= temp maximum) (maximal-elements1 (cdr lst)
              (cons (car lst) winners)
              maximum
              fn
              wrld))
          (t (maximal-elements1 (cdr lst) winners maximum fn wrld)))))))

(defun maximal-elements
  (lst fn wrld)
  (cond ((null lst) nil)
    ((null (cdr lst)) lst)
    (t (reverse (maximal-elements1 (cdr lst)
          (list (car lst))
          (maximal-elements-apply fn (car lst) wrld)
          fn
          wrld)))))

(defun intersectp-eq/union-equal
  (x y)
  (cond ((intersectp-eq (car x) (car y)) (cons (union-eq (car x) (car y))
        (union-equal (cdr x) (cdr y))))
    (t nil)))

(defun equal/union-equal
  (x y)
  (cond ((equal (car x) (car y)) (cons (car x) (union-equal (cdr x) (cdr y))))
    (t nil)))

(defun subsetp-equal/smaller
  (x y)
  (cond ((subsetp-equal x y) x)
    ((subsetp-equal y x) y)
    (t nil)))

(defun m&m-apply
  (fn x y)
  (case fn
    (intersectp-eq/union-equal (intersectp-eq/union-equal x y))
    (equal/union-equal (equal/union-equal x y))
    (flush-candidates (flush-candidates x y))
    (merge-candidates (merge-candidates x y))
    (subsetp-equal/smaller (subsetp-equal/smaller x y))))

(defun count-off
  (n lst)
  (cond ((null lst) nil)
    (t (cons (cons n (car lst)) (count-off (1+ n) (cdr lst))))))

(defun m&m-search
  (x y-lst del fn)
  (cond ((null y-lst) (mv nil nil))
    ((member (caar y-lst) del) (m&m-search x (cdr y-lst) del fn))
    (t (let ((z (m&m-apply fn x (cdar y-lst))))
        (cond (z (mv z (caar y-lst)))
          (t (m&m-search x (cdr y-lst) del fn)))))))

(defun m&m1
  (pairs del ans n fn)
  (cond ((null pairs) ans)
    ((member (caar pairs) del) (m&m1 (cdr pairs) del ans n fn))
    (t (mv-let (mrg y-id)
        (m&m-search (cdar pairs) (cdr pairs) del fn)
        (cond ((null mrg) (m&m1 (cdr pairs) del (cons (cdar pairs) ans) n fn))
          (t (m&m1 (cons (cons n mrg) (cdr pairs))
              (cons y-id del)
              ans
              (1+ n)
              fn)))))))

(defun m&m
  (bag fn)
  (m&m1 (count-off 0 bag) nil nil (length bag) fn))

(defun cons-subset-tree
  (x y)
  (if (eq x t)
    (if (eq y t)
      t
      (if y
        (cons x y)
        '(t)))
    (if x
      (cons x y)
      (if (eq y t)
        '(nil . t)
        (if y
          (cons x y)
          nil)))))

(defun or-subset-trees
  (tree1 tree2)
  (cond ((or (eq tree1 t) (eq tree2 t)) t)
    ((null tree1) tree2)
    ((null tree2) tree1)
    (t (cons-subset-tree (or-subset-trees (car-subset-tree tree1)
          (car-subset-tree tree2))
        (or-subset-trees (cdr-subset-tree tree1)
          (cdr-subset-tree tree2))))))

(defun m&m-over-powerset1
  (st subset stree ans fn)
  (cond ((eq stree t) (mv t ans))
    ((null st) (let ((z (m&m subset fn)))
        (cond ((and z (null (cdr z))) (mv t (cons (car z) ans)))
          (t (mv nil ans)))))
    (t (mv-let (stree1 ans1)
        (m&m-over-powerset1 (cdr st)
          (cons (car st) subset)
          (cdr-subset-tree stree)
          ans
          fn)
        (mv-let (stree2 ans2)
          (m&m-over-powerset1 (cdr st)
            subset
            (or-subset-trees (car-subset-tree stree) stree1)
            ans1
            fn)
          (mv (cons-subset-tree stree2 stree1) ans2))))))

(defun m&m-over-powerset
  (st fn)
  (mv-let (stree ans)
    (m&m-over-powerset1 st nil nil nil fn)
    (declare (ignore stree))
    ans))

(defun select-do$-induction-q-seedp1
  (lit xterms)
  (cond ((endp xterms) t)
    ((occur (car xterms) lit) nil)
    (t (select-do$-induction-q-seedp1 lit (cdr xterms)))))

(defun select-do$-induction-q-seedp
  (lit xterms mvars)
  (and (subsetp-eq (all-vars lit) mvars)
    (if (eq xterms :do$)
      (not (ffnnamep 'do$ lit))
      (select-do$-induction-q-seedp1 lit xterms))))

(defun select-do$-induction-q-seed
  (cl xterms mvars)
  (cond ((endp cl) nil)
    ((select-do$-induction-q-seedp (car cl) xterms mvars) (cons (car cl)
        (select-do$-induction-q-seed (cdr cl) xterms mvars)))
    (t (select-do$-induction-q-seed (cdr cl) xterms mvars))))

(defun select-do$-induction-q-filterp
  (lit cl-set)
  (cond ((endp cl-set) t)
    ((member-equal lit (car cl-set)) (select-do$-induction-q-filterp lit (cdr cl-set)))
    (t nil)))

(defun select-do$-induction-q-filter
  (seed cl-set)
  (cond ((endp seed) nil)
    ((select-do$-induction-q-filterp (car seed) cl-set) (cons (car seed)
        (select-do$-induction-q-filter (cdr seed) cl-set)))
    (t (select-do$-induction-q-filter (cdr seed) cl-set))))

(defun select-do$-induction-q
  (cl-set xterms mterm)
  (let* ((mvars (all-vars mterm)) (seed (select-do$-induction-q-seed (car cl-set) xterms mvars)))
    (select-do$-induction-q-filter seed (cdr cl-set))))

(defun do$-induction-measure-clauses1
  (negated-tests alist-lst mterm)
  (cond ((endp alist-lst) nil)
    (t (cons (append negated-tests
          (list (cons-term* 'l< (sublis-var (car alist-lst) mterm) mterm)))
        (do$-induction-measure-clauses1 negated-tests
          (cdr alist-lst)
          mterm)))))

(defun do$-induction-measure-clauses
  (ta-lst q-lst mterm)
  (cond ((endp ta-lst) nil)
    (t (append (do$-induction-measure-clauses1 (union-equal q-lst
            (dumb-negate-lit-lst (access tests-and-alists (car ta-lst) :tests)))
          (access tests-and-alists (car ta-lst) :alists)
          mterm)
        (do$-induction-measure-clauses (cdr ta-lst) q-lst mterm)))))

(defun all-picks2
  (pocket pick ans)
  (cond ((null pocket) ans)
    (t (cons (cons (car pocket) pick)
        (all-picks2 (cdr pocket) pick ans)))))

(defun all-picks2r
  (pocket pick ans)
  (cond ((null pocket) ans)
    (t (all-picks2r (cdr pocket)
        pick
        (cons (cons (car pocket) pick) ans)))))

(defun all-picks1
  (pocket picks ans rflg)
  (cond ((null picks) ans)
    (t (all-picks1 pocket
        (cdr picks)
        (if rflg
          (all-picks2r pocket (car picks) ans)
          (all-picks2 pocket (car picks) ans))
        rflg))))

(defun all-picks
  (pockets rflg)
  (cond ((null pockets) '(nil))
    (t (all-picks1 (car pockets)
        (all-picks (cdr pockets) (not rflg))
        nil
        rflg))))

(defun dumb-negate-lit-lst-lst
  (cl-set)
  (cond ((null cl-set) nil)
    (t (cons (dumb-negate-lit-lst (car cl-set))
        (dumb-negate-lit-lst-lst (cdr cl-set))))))

(defun induction-hyp-clause-segments2
  (alists cl ans)
  (cond ((null alists) ans)
    (t (cons (sublis-var-lst (car alists) cl)
        (induction-hyp-clause-segments2 (cdr alists) cl ans)))))

(defun induction-hyp-clause-segments1
  (alists cl-set ans)
  (cond ((null cl-set) ans)
    (t (induction-hyp-clause-segments2 alists
        (car cl-set)
        (induction-hyp-clause-segments1 alists (cdr cl-set) ans)))))

(defun induction-hyp-clause-segments
  (alists cl-set)
  (all-picks (induction-hyp-clause-segments1 alists
      (dumb-negate-lit-lst-lst cl-set)
      nil)
    nil))

(defun induction-formula3
  (neg-tests hyp-segments cl ans)
  (cond ((null hyp-segments) ans)
    (t (induction-formula3 neg-tests
        (cdr hyp-segments)
        cl
        (conjoin-clause-to-clause-set (disjoin-clauses neg-tests
            (disjoin-clauses (car hyp-segments) cl))
          ans)))))

(defun induction-formula2
  (cl cl-set ta-lst ans)
  (cond ((null ta-lst) ans)
    (t (induction-formula2 cl
        cl-set
        (cdr ta-lst)
        (induction-formula3 (dumb-negate-lit-lst (access tests-and-alists (car ta-lst) :tests))
          (induction-hyp-clause-segments (access tests-and-alists (car ta-lst) :alists)
            cl-set)
          cl
          ans)))))

(defun induction-formula1
  (lst cl-set ta-lst ans)
  (cond ((null lst) ans)
    (t (induction-formula1 (cdr lst)
        cl-set
        ta-lst
        (induction-formula2 (car lst) cl-set ta-lst ans)))))

(defun induction-formula
  (cl-set induction-term xterms measure-term ta-lst)
  (let* ((ans1 (reverse (induction-formula1 cl-set cl-set ta-lst nil))) (ans2 (if (and (consp induction-term)
            (eq (ffn-symb induction-term) *do$-induction-fn*))
          (append (do$-induction-measure-clauses ta-lst
              (select-do$-induction-q cl-set xterms measure-term)
              measure-term)
            ans1)
          ans1)))
    (m&m ans2 'subsetp-equal/smaller)))

(defun all-picks-size
  (cl-set)
  (cond ((null cl-set) 1)
    (t (* (length (car cl-set)) (all-picks-size (cdr cl-set))))))

(defun induction-formula-size1
  (hyps-size concl-size ta-lst)
  (cond ((null ta-lst) 0)
    (t (+ (* concl-size
          (expt hyps-size
            (length (access tests-and-alists (car ta-lst) :alists))))
        (induction-formula-size1 hyps-size concl-size (cdr ta-lst))))))

(defun induction-formula-size
  (cl-set ta-lst)
  (induction-formula-size1 (all-picks-size cl-set)
    (length cl-set)
    ta-lst))

(defun termify-clause-set
  (clauses)
  (declare (xargs :guard (pseudo-term-list-listp clauses)))
  (cond ((null clauses) *t*)
    ((null (cdr clauses)) (disjoin (car clauses)))
    (t (mcons-term* 'if
        (disjoin (car clauses))
        (termify-clause-set (cdr clauses))
        *nil*))))

(defun inform-simplify3
  (alist terms ans)
  (cond ((null terms) ans)
    (t (inform-simplify3 alist
        (cdr terms)
        (add-to-set-equal (sublis-var alist (car terms)) ans)))))

(defun inform-simplify2
  (alists terms ans)
  (cond ((null alists) ans)
    (t (inform-simplify2 (cdr alists)
        terms
        (inform-simplify3 (car alists) terms ans)))))

(defun inform-simplify1
  (ta-lst terms ans)
  (cond ((null ta-lst) ans)
    (t (inform-simplify1 (cdr ta-lst)
        terms
        (inform-simplify2 (access tests-and-alists (car ta-lst) :alists)
          terms
          ans)))))

(defun inform-simplify
  (ta-lst terms pspv)
  (change prove-spec-var
    pspv
    :induction-concl-terms terms
    :induction-hyp-terms (inform-simplify1 ta-lst terms nil)))

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

(defun gen-new-name1
  (char-lst wrld i)
  (let ((name (intern (coerce (append char-lst (explode-nonnegative-integer i 10 nil))
           'string)
         "ACL2")))
    (cond ((new-namep name wrld) name)
      (t (gen-new-name1 char-lst wrld (1+ i))))))

(defun gen-new-name
  (root wrld)
  (cond ((new-namep root wrld) root)
    (t (gen-new-name1 (coerce (symbol-name root) 'list) wrld 0))))

(defun unmeasured-variables3
  (vars alist)
  (cond ((null alist) nil)
    ((or (member-eq (caar alist) vars)
       (eq (caar alist) (cdar alist))) (unmeasured-variables3 vars (cdr alist)))
    (t (cons (caar alist) (unmeasured-variables3 vars (cdr alist))))))

(defun unmeasured-variables2
  (vars alists)
  (cond ((null alists) nil)
    (t (union-eq (unmeasured-variables3 vars (car alists))
        (unmeasured-variables2 vars (cdr alists))))))

(defun unmeasured-variables1
  (vars ta-lst)
  (cond ((null ta-lst) nil)
    (t (union-eq (unmeasured-variables2 vars
          (access tests-and-alists (car ta-lst) :alists))
        (unmeasured-variables1 vars (cdr ta-lst))))))

(defun unmeasured-variables
  (measured-vars cand)
  (unmeasured-variables1 measured-vars
    (access candidate cand :tests-and-alists-lst)))

(defun tilde-@-well-founded-relation-phrase
  (rel wrld)
  (let* ((temp (assoc-eq rel
         (global-val 'well-founded-relation-alist wrld))) (mp (cadr temp))
      (base-symbol (base-symbol (cddr temp))))
    (msg "the relation ~x0 (which~#1~[ ~/, by ~x2, ~]is known to be ~
          well-founded~#3~[~/ on the domain recognized by ~x4~])"
      rel
      (if (null base-symbol)
        0
        1)
      base-symbol
      (if (eq mp t)
        0
        1)
      mp)))

(defun measured-variables
  (cand wrld)
  (if (eq (ffn-symb (access candidate cand :induction-term))
      *do$-induction-fn*)
    (all-vars (access justification
        (access candidate cand :justification)
        :measure))
    (all-vars1-lst (subcor-var-lst (formals (ffn-symb (access candidate cand :induction-term))
          wrld)
        (fargs (access candidate cand :induction-term))
        (access justification
          (access candidate cand :justification)
          :subset))
      nil)))

(defun induct-msg/continue
  (pool-lst forcing-round
    cl-set
    induct-hint-val
    len-candidates
    len-flushed-candidates
    len-merged-candidates
    len-unvetoed-candidates
    len-complicated-candidates
    len-high-scoring-candidates
    winning-candidate
    estimated-size
    clauses
    wrld
    state)
  (declare (xargs :normalize nil))
  (cond ((and (gag-mode)
       (or (eq (gag-mode-evisc-tuple state) t) (cdr pool-lst))) state)
    (t (pprogn (increment-timer 'prove-time state)
        (let* ((pool-name (tilde-@-pool-name-phrase forcing-round pool-lst)) (p (cons :p (merge-sort-term-order (all-vars1-lst-lst cl-set nil))))
            (measured-variables (measured-variables winning-candidate wrld))
            (unmeasured-variables (unmeasured-variables measured-variables winning-candidate))
            (attribution-phrase (tilde-*-simp-phrase (access candidate winning-candidate :ttree))))
          (fms "~#H~[We have been told to use induction.  ~N0 induction ~
                scheme~#1~[ is~/s are~] suggested by the induction ~
                hint.~/~

                We have been told to use induction.  ~N0 induction ~
                scheme~#1~[ is~/s are~] suggested by this ~
                conjecture.~/~

                Perhaps we can prove ~@n by induction.  ~

                ~N0 induction scheme~#1~[ is~/s are~] suggested by this ~
                conjecture.~]  ~

          ~#a~[~/Subsumption reduces that number to ~n2.  ~]~

          ~#b~[~/These merge into ~n3 derived induction scheme~#4~[~/s~].  ~]~

          ~#c~[~/However, ~n5 of these ~#6~[is~/are~] flawed and so we are ~
           left with ~nq viable ~#r~[~/candidate~/candidates~].  ~]~

          ~#d~[~/By considering those suggested by the largest number of ~
                 non-primitive recursive functions, we narrow the field ~
                 to ~n7.  ~]~

          ~#e~[~/~N8 of these ~
                 ~#9~[has a score higher than the other~#A~[~/s~].  ~/~
                      are tied for the highest score.  ~]~]~

          ~#f~[~/We will choose arbitrarily among these.  ~]~

          ~|~%We will induct according to a scheme suggested by ~
          ~#h~[~xg.~/~xg, while ac~-com~-mo~-dating ~*i~]~

          ~|~%~#w~[~/~#h~[This suggestion was~/These suggestions were~] ~
          produced using ~*x.~]  ~

          If we let ~xp denote ~@n above then the induction scheme ~
          we'll use is~|~

          ~Qsy.~

          ~#J~[Note that one or more measure conjectures included in ~
          the scheme above justify this induction if they are provable.  ~/~
          This induction is justified by the same argument used to ~
          admit ~xj.  ~]~

          ~#l~[~/Note, however, that the unmeasured ~
                 variable~#m~[ ~&m is~/s ~&m are~] being instantiated.  ~]~

          When applied to the goal at hand the above induction scheme ~
          produces ~#v~[no nontautological subgoals~/one nontautological ~
          subgoal~/~no nontautological subgoals~].~

          ~#t~[~/  However, to achieve this relatively small number of ~
          cases we had to termify ~@n (see :DOC termify).  Otherwise, this ~
          induction would have produced approximately ~nu cases!~]~|"
            (list (cons #\H
                (cond ((null induct-hint-val) 2)
                  ((equal induct-hint-val *t*) 1)
                  (t 0)))
              (cons #\n pool-name)
              (cons #\0 len-candidates)
              (cons #\1
                (if (int= len-candidates 1)
                  0
                  1))
              (cons #\a
                (if (< len-flushed-candidates len-candidates)
                  1
                  0))
              (cons #\2 len-flushed-candidates)
              (cons #\b
                (if (< len-merged-candidates len-flushed-candidates)
                  1
                  0))
              (cons #\3 len-merged-candidates)
              (cons #\4
                (if (int= len-merged-candidates 1)
                  0
                  1))
              (cons #\c
                (if (< len-unvetoed-candidates len-merged-candidates)
                  1
                  0))
              (cons #\5 (- len-merged-candidates len-unvetoed-candidates))
              (cons #\q len-unvetoed-candidates)
              (cons #\y (gag-mode-evisc-tuple state))
              (cons #\r (zero-one-or-more len-unvetoed-candidates))
              (cons #\6
                (if (int= (- len-merged-candidates len-unvetoed-candidates) 1)
                  0
                  1))
              (cons #\d
                (if (< len-complicated-candidates len-unvetoed-candidates)
                  1
                  0))
              (cons #\7 len-complicated-candidates)
              (cons #\e
                (if (< len-high-scoring-candidates len-complicated-candidates)
                  1
                  0))
              (cons #\8 len-high-scoring-candidates)
              (cons #\9
                (if (int= len-high-scoring-candidates 1)
                  0
                  1))
              (cons #\A
                (if (int= (- len-complicated-candidates len-high-scoring-candidates)
                    1)
                  0
                  1))
              (cons #\f
                (if (int= len-high-scoring-candidates 1)
                  0
                  1))
              (cons #\p p)
              (cons #\s
                (prettyify-clause-set (induction-formula (list (cond ((eq (ffn-symb (access candidate winning-candidate :induction-term))
                           *do$-induction-fn*) (append (select-do$-induction-q cl-set
                              (cons (access candidate winning-candidate :xinduction-term)
                                (access candidate winning-candidate :xother-terms))
                              (access justification
                                (access candidate winning-candidate :justification)
                                :measure))
                            (list p)))
                        (t (list p))))
                    (access candidate winning-candidate :induction-term)
                    (list p)
                    (access justification
                      (access candidate winning-candidate :justification)
                      :measure)
                    (access candidate winning-candidate :tests-and-alists-lst))
                  (let*-abstractionp state)
                  wrld))
              (cons #\g
                (untranslate (access candidate winning-candidate :xinduction-term)
                  nil
                  wrld))
              (cons #\h
                (if (access candidate winning-candidate :xother-terms)
                  1
                  0))
              (cons #\i
                (tilde-*-untranslate-lst-phrase (access candidate winning-candidate :xother-terms)
                  #\.
                  nil
                  wrld))
              (cons #\J
                (if (eq (ffn-symb (access candidate winning-candidate :induction-term))
                    *do$-induction-fn*)
                  0
                  1))
              (cons #\j
                (ffn-symb (access candidate winning-candidate :xinduction-term)))
              (cons #\l
                (if unmeasured-variables
                  1
                  0))
              (cons #\m unmeasured-variables)
              (cons #\o (length clauses))
              (cons #\t
                (if estimated-size
                  1
                  0))
              (cons #\u estimated-size)
              (cons #\v
                (if (null clauses)
                  0
                  (if (cdr clauses)
                    2
                    1)))
              (cons #\w
                (if (nth 4 attribution-phrase)
                  1
                  0))
              (cons #\x attribution-phrase))
            (proofs-co state)
            state
            (term-evisc-tuple nil state)))
        (increment-timer 'print-time state)))))

(defun induct-msg/lose
  (pool-name induct-hint-val pspv state)
  (pprogn (increment-timer 'prove-time state)
    (fms "No induction schemes are suggested by ~#H~[the induction ~
         hint.~@?~/~@n.~]  Consequently, the proof attempt has failed.~|"
      (list (cons #\H (cond (induct-hint-val 0) (t 1)))
        (cons #\n pool-name)
        (cons #\?
          (and induct-hint-val
            (let* ((wrld (w state)) (all-fns (all-fnnames induct-hint-val))
                (rec-fns (rec-fnnames induct-hint-val wrld)))
              (cond ((null all-fns) "  (Note that there is no function symbol ~
                              occurring in that hint.)")
                ((and (null rec-fns) (null (cdr all-fns))) (msg "  (Note that ~x0 is not defined ~
                                   recursively, so it cannot suggest an ~
                                   induction scheme.)"
                    (car all-fns)))
                ((null rec-fns) "  (Note that none of its function symbols is ~
                              defined recursively, so they cannot suggest ~
                              induction schemes.)")
                ((and (all-variablep (fargs induct-hint-val))
                   (let ((ens (ens-from-pspv pspv)))
                     (and (not (enabled-runep (list :induction (car rec-fns)) ens wrld))
                       (not (enabled-runep (list :definition (car rec-fns)) ens wrld))))) (msg "  (Note that ~x0 (including its :induction ~
                                   rune) is disabled, so it cannot suggest an ~
                                   induction scheme.  Consider providing an ~
                                   :in-theory hint that enables ~x0 or ~x1.)"
                    (car all-fns)
                    (list :induction (car all-fns))))
                (t ""))))))
      (proofs-co state)
      state
      (term-evisc-tuple nil state))
    (increment-timer 'print-time state)))

(defun set-difference-augmented-theories
  (lst1 lst2 ans)
  (cond ((endp lst1) (reverse ans))
    ((endp lst2) (revappend ans lst1))
    ((= (car (car lst1)) (car (car lst2))) (set-difference-augmented-theories (cdr lst1)
        (cdr lst2)
        ans))
    ((> (car (car lst1)) (car (car lst2))) (set-difference-augmented-theories (cdr lst1)
        lst2
        (cons (car lst1) ans)))
    (t (set-difference-augmented-theories lst1 (cdr lst2) ans))))

(defun update-hint-settings
  (new-hint-settings old-hint-settings)
  (cond ((endp new-hint-settings) old-hint-settings)
    ((assoc-eq (caar new-hint-settings) old-hint-settings) (update-hint-settings (cdr new-hint-settings)
        (cons (car new-hint-settings)
          (remove1-assoc-eq (caar new-hint-settings)
            old-hint-settings))))
    (t (update-hint-settings (cdr new-hint-settings)
        (cons (car new-hint-settings) old-hint-settings)))))

(defun restore-hint-settings-in-pspv
  (new-pspv old-pspv)
  (let* ((old-rcnst (access prove-spec-var old-pspv :rewrite-constant)) (old-ens (access rewrite-constant
          old-rcnst
          :current-enabled-structure))
      (old-name (access enabled-structure old-ens :array-name))
      (new-rcnst (access prove-spec-var new-pspv :rewrite-constant))
      (new-ens (access rewrite-constant
          new-rcnst
          :current-enabled-structure))
      (new-name (access enabled-structure new-ens :array-name)))
    (prog2$ (cond ((equal old-name new-name) nil)
        (t (flush-compress new-name)))
      (change prove-spec-var
        new-pspv
        :rewrite-constant old-rcnst
        :hint-settings (access prove-spec-var old-pspv :hint-settings)))))

(defun remove-trivial-clauses
  (clauses wrld)
  (cond ((null clauses) nil)
    ((trivial-clause-p (car clauses) wrld) (remove-trivial-clauses (cdr clauses) wrld))
    (t (cons (car clauses)
        (remove-trivial-clauses (cdr clauses) wrld)))))

(defun remove-adjacent-duplicates-eq
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
    ((atom (cdr x)) (list (car x)))
    ((eq (car x) (cadr x)) (remove-adjacent-duplicates-eq (cdr x)))
    (t (cons (car x) (remove-adjacent-duplicates-eq (cdr x))))))

(defun induct
  (forcing-round pool-lst
    cl-set
    hint-settings
    pspv
    wrld
    ctx
    state)
  (let ((cl-set (remove-guard-holders-lst-lst cl-set wrld)) (pool-name (tilde-@-pool-name-phrase forcing-round pool-lst))
      (induct-hint-val (let ((induct-hint-val0 (cdr (assoc-eq :induct hint-settings))))
          (and induct-hint-val0
            (remove-guard-holders induct-hint-val0 wrld)))))
    (mv-let (erp new-pspv state)
      (load-hint-settings-into-pspv nil
        (if induct-hint-val
          (remove1-assoc-eq :induct hint-settings)
          hint-settings)
        pspv
        nil
        wrld
        ctx
        state)
      (cond (erp (mv 'lose nil pspv state))
        (t (let* ((candidates (get-induction-cands-from-cl-set (select-x-cl-set cl-set induct-hint-val)
                 new-pspv
                 wrld
                 state)) (flushed-candidates (m&m candidates 'flush-candidates))
              (merged-candidates (cond ((< (length flushed-candidates) 10) (m&m-over-powerset flushed-candidates 'merge-candidates))
                  (t (m&m flushed-candidates 'merge-candidates))))
              (unvetoed-candidates (compute-vetoes merged-candidates wrld))
              (complicated-candidates (maximal-elements unvetoed-candidates
                  'induction-complexity
                  wrld))
              (high-scoring-candidates (maximal-elements complicated-candidates 'score wrld))
              (winning-candidate (car high-scoring-candidates)))
            (cond (winning-candidate (mv-let (erp candidate-ttree state)
                  (accumulate-ttree-and-step-limit-into-state (access candidate winning-candidate :ttree)
                    :skip state)
                  (declare (ignore erp))
                  (let ((estimated-size (induction-formula-size cl-set
                         (access candidate winning-candidate :tests-and-alists-lst))))
                    (mv-let (step-limit00 clauses00 ttree00)
                      (cond ((and (> estimated-size *maximum-induct-size*)
                           (not (and (equal (len cl-set) 1) (equal (len (car cl-set)) 1)))) (mv nil (list (list (termify-clause-set cl-set))) nil))
                        ((and (eq (ffn-symb (access candidate winning-candidate :induction-term))
                             *do$-induction-fn*)
                           (equal (len cl-set) 1)
                           (equal (len (car cl-set)) 1)) (clausify-input (car (car cl-set))
                            (access rewrite-constant
                              (access prove-spec-var new-pspv :rewrite-constant)
                              :fns-to-be-ignored-by-rewrite)
                            (ens-from-pspv new-pspv)
                            wrld
                            state
                            nil
                            (initial-step-limit wrld state)))
                        (t (mv nil cl-set nil)))
                      (declare (ignore step-limit00))
                      (let* ((termifiedp (and (> estimated-size *maximum-induct-size*)
                             (not (and (equal (len cl-set) 1) (equal (len (car cl-set)) 1))))) (clauses0 (induction-formula clauses00
                              (access candidate winning-candidate :induction-term)
                              (if (and induct-hint-val (not (equal induct-hint-val *t*)))
                                :do$ (cons (access candidate winning-candidate :xinduction-term)
                                  (access candidate winning-candidate :xother-terms)))
                              (access justification
                                (access candidate winning-candidate :justification)
                                :measure)
                              (access candidate winning-candidate :tests-and-alists-lst)))
                          (clauses1 clauses0)
                          (clauses (cond ((> estimated-size *maximum-induct-size*) clauses1)
                              (t (remove-trivial-clauses clauses1 wrld))))
                          (newer-pspv (inform-simplify (access candidate winning-candidate :tests-and-alists-lst)
                              (add-to-set-equal (access candidate winning-candidate :xinduction-term)
                                (access candidate winning-candidate :xother-terms))
                              (change prove-spec-var
                                new-pspv
                                :tag-tree (cons-tag-trees ttree00
                                  (cons-tag-trees candidate-ttree
                                    (access prove-spec-var new-pspv :tag-tree)))))))
                        (let ((state (io? prove
                               nil
                               state
                               (wrld clauses
                                 termifiedp
                                 estimated-size
                                 winning-candidate
                                 high-scoring-candidates
                                 complicated-candidates
                                 unvetoed-candidates
                                 merged-candidates
                                 flushed-candidates
                                 candidates
                                 induct-hint-val
                                 forcing-round
                                 pool-lst)
                               (induct-msg/continue pool-lst
                                 forcing-round
                                 clauses
                                 induct-hint-val
                                 (length candidates)
                                 (length flushed-candidates)
                                 (length merged-candidates)
                                 (length unvetoed-candidates)
                                 (length complicated-candidates)
                                 (length high-scoring-candidates)
                                 winning-candidate
                                 (if termifiedp
                                   estimated-size
                                   nil)
                                 clauses
                                 wrld
                                 state))))
                          (mv 'continue clauses newer-pspv state)))))))
              (t (pprogn (io? prove
                    nil
                    state
                    (induct-hint-val pool-name new-pspv)
                    (induct-msg/lose pool-name induct-hint-val new-pspv state))
                  (mv 'lose nil pspv state))))))))))

(defun pair-vars-with-lits
  (cl)
  (cond ((null cl) nil)
    (t (cons (cons (all-vars (car cl)) (list (car cl)))
        (pair-vars-with-lits (cdr cl))))))

(defun probably-not-validp
  (cl)
  (or (ffnnames-subsetp-listp cl
      '(not consp
        integerp
        rationalp
        acl2-numberp
        true-listp
        complex-rationalp
        stringp
        characterp
        symbolp
        cons
        car
        cdr
        equal
        binary-+
        unary--
        <
        apply))
    (case-match cl
      ((('not (& . args))) (and args (all-variablep args) (no-duplicatesp-eq args)))
      (((& . args)) (and args (all-variablep args) (no-duplicatesp-eq args)))
      (& nil))))

(defun irrelevant-lits
  (alist)
  (cond ((null alist) nil)
    ((probably-not-validp (cdar alist)) (append (cdar alist) (irrelevant-lits (cdr alist))))
    (t (irrelevant-lits (cdr alist)))))

(defun eliminate-irrelevance-clause
  (cl hist pspv wrld state)
  (declare (ignore hist wrld state))
  (cond ((not (assoc-eq 'being-proved-by-induction
         (access prove-spec-var pspv :pool))) (mv 'miss nil nil nil))
    (t (let* ((partitioning (m&m (pair-vars-with-lits cl) 'intersectp-eq/union-equal)) (irrelevant-lits (irrelevant-lits partitioning)))
        (cond ((null irrelevant-lits) (mv 'miss nil nil nil))
          (t (mv 'hit
              (list (set-difference-equal cl irrelevant-lits))
              (add-to-tag-tree! 'irrelevant-lits
                irrelevant-lits
                (add-to-tag-tree! 'clause cl nil))
              pspv)))))))

(defun eliminate-irrelevance-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal pspv clauses))
  (let* ((lits (tagged-object 'irrelevant-lits ttree)) (clause (tagged-object 'clause ttree))
      (concl (car (last clause))))
    (cond ((equal (length lits) (length clause)) (fms "We suspect that this conjecture is not a theorem.  We ~
            might as well be trying to prove~|"
          nil
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      (t (let ((iterms (cond ((member-equal concl lits) (append (dumb-negate-lit-lst (remove1-equal concl lits))
                   (list concl)))
               (t (dumb-negate-lit-lst lits)))))
          (fms "We suspect that the term~#0~[ ~*1 is~/s ~*1 are~] irrelevant to ~
              the truth of this conjecture and throw ~#0~[it~/them~] out.  We ~
              will thus try to prove~|"
            (list (cons #\0 iterms)
              (cons #\1
                (tilde-*-untranslate-lst-phrase iterms nil t (w state))))
            (proofs-co state)
            state
            (term-evisc-tuple nil state)))))))