rewrite

(defun warranted-fns-of-world1
  (x wrld)
  (declare (xargs :mode :logic :guard (plist-worldp wrld)))
  (cond ((atom x) nil)
    ((and (weak-badge-userfn-structure-tuplep (car x))
       (access-badge-userfn-structure-tuple-warrantp (car x))
       (symbolp (car (car x)))
       (function-symbolp (car (car x)) wrld)) (cons (car (car x)) (warranted-fns-of-world1 (cdr x) wrld)))
    (t nil)))

(defun warranted-fns-of-world
  (wrld)
  (declare (xargs :mode :logic :guard (plist-worldp wrld)
      :verify-guards nil))
  (and (alistp (table-alist 'badge-table wrld))
    (warranted-fns-of-world1 (cdr (assoc-eq :badge-userfn-structure (table-alist 'badge-table wrld)))
      wrld)))

(defun ev-fncall+-w
  (fn args w safe-mode gc-off strictp)
  (let* ((big-n (big-n)) (fns (ev-fncall+-fns fn args w big-n safe-mode gc-off strictp)))
    (mv-let (erp val latches)
      (ev-fncall-rec-logical fn
        args
        nil
        w
        nil
        big-n
        safe-mode
        gc-off
        nil
        t
        nil
        (and (not strictp) fns))
      (declare (ignore latches))
      (mv erp val fns))))

(defun ev-fncall+
  (fn args strictp state)
  (ev-fncall+-w fn
    args
    (w state)
    (f-get-global 'safe-mode state)
    (gc-off state)
    strictp))

(defun refinementp
  (equiv1 equiv2 wrld)
  (cond ((eq equiv1 'equal) t)
    ((eq equiv2 'equal) nil)
    ((eq equiv1 equiv2) t)
    (t (member-eq equiv2
        (cdr (getpropc equiv1 'coarsenings nil wrld))))))

(defun geneqv-refinementp1
  (coarsenings geneqv)
  (cond ((null geneqv) nil)
    ((member-eq (access congruence-rule (car geneqv) :equiv)
       coarsenings) (access congruence-rule (car geneqv) :rune))
    (t (geneqv-refinementp1 coarsenings (cdr geneqv)))))

(defun geneqv-refinementp
  (equiv geneqv wrld)
  (cond ((eq equiv 'equal) *fake-rune-for-anonymous-enabled-rule*)
    ((null geneqv) nil)
    (t (geneqv-refinementp1 (getpropc equiv 'coarsenings nil wrld)
        geneqv))))

(defun some-congruence-rule-disabledp
  (geneqv ens)
  (cond ((null geneqv) nil)
    ((enabled-numep (access congruence-rule (car geneqv) :nume)
       ens) (some-congruence-rule-disabledp (cdr geneqv) ens))
    (t t)))

(defun filter-geneqv1
  (geneqv ens)
  (cond ((null geneqv) nil)
    ((enabled-numep (access congruence-rule (car geneqv) :nume)
       ens) (cons (car geneqv) (filter-geneqv1 (cdr geneqv) ens)))
    (t (filter-geneqv1 (cdr geneqv) ens))))

(defun filter-geneqv
  (geneqv ens)
  (cond ((some-congruence-rule-disabledp geneqv ens) (filter-geneqv1 geneqv ens))
    (t geneqv)))

(defun some-geneqv-disabledp
  (lst ens)
  (cond ((null lst) nil)
    ((some-congruence-rule-disabledp (car lst) ens) t)
    (t (some-geneqv-disabledp (cdr lst) ens))))

(defun filter-geneqv-lst1
  (lst ens)
  (cond ((null lst) nil)
    (t (cons (filter-geneqv (car lst) ens)
        (filter-geneqv-lst1 (cdr lst) ens)))))

(defun filter-geneqv-lst
  (lst ens)
  (cond ((null ens) lst)
    ((some-geneqv-disabledp lst ens) (filter-geneqv-lst1 lst ens))
    (t lst)))

(defun refinementp1
  (equiv1 coarsenings1 equiv2)
  (cond ((eq equiv1 'equal) t)
    ((eq equiv2 'equal) nil)
    ((eq equiv1 equiv2) t)
    (t (member-eq equiv2 coarsenings1))))

(defun pair-congruence-rules-with-coarsenings
  (geneqv wrld)
  (cond ((null geneqv) nil)
    (t (cons (cons (car geneqv)
          (cdr (getpropc (access congruence-rule (car geneqv) :equiv)
              'coarsenings
              nil
              wrld)))
        (pair-congruence-rules-with-coarsenings (cdr geneqv) wrld)))))

(defun add-to-cr-and-coarsenings
  (new-cr new-cr-coarsenings
    old-crs-and-coarsenings
    both-tests-flg)
  (cond ((null old-crs-and-coarsenings) (list (cons new-cr (cdr new-cr-coarsenings))))
    ((and both-tests-flg
       (refinementp1 (car new-cr-coarsenings)
         (cdr new-cr-coarsenings)
         (access congruence-rule
           (car (car old-crs-and-coarsenings))
           :equiv))) old-crs-and-coarsenings)
    ((refinementp1 (access congruence-rule
         (car (car old-crs-and-coarsenings))
         :equiv)
       (cdr (car old-crs-and-coarsenings))
       (car new-cr-coarsenings)) (add-to-cr-and-coarsenings new-cr
        new-cr-coarsenings
        (cdr old-crs-and-coarsenings)
        nil))
    (t (cons (car old-crs-and-coarsenings)
        (add-to-cr-and-coarsenings new-cr
          new-cr-coarsenings
          (cdr old-crs-and-coarsenings)
          both-tests-flg)))))

(defun union-geneqv1
  (geneqv1 old-crs-and-coarsenings wrld)
  (cond ((null geneqv1) old-crs-and-coarsenings)
    (t (union-geneqv1 (cdr geneqv1)
        (add-to-cr-and-coarsenings (car geneqv1)
          (getpropc (access congruence-rule (car geneqv1) :equiv)
            'coarsenings
            nil
            wrld)
          old-crs-and-coarsenings
          t)
        wrld))))

(defun union-geneqv
  (geneqv1 geneqv2 wrld)
  (strip-cars (union-geneqv1 geneqv1
      (pair-congruence-rules-with-coarsenings geneqv2 wrld)
      wrld)))

(defun pairwise-union-geneqv
  (lst1 lst2 wrld)
  (cond ((null lst1) nil)
    (t (cons (union-geneqv (car lst1) (car lst2) wrld)
        (pairwise-union-geneqv (cdr lst1) (cdr lst2) wrld)))))

(defun geneqv-lst1
  (congruences geneqv ens wrld)
  (cond ((null congruences) nil)
    (t (let ((ans (geneqv-lst1 (cdr congruences) geneqv ens wrld)))
        (cond ((geneqv-refinementp (caar congruences) geneqv wrld) (cond ((null ans) (filter-geneqv-lst (cdar congruences) ens))
              (t (pairwise-union-geneqv (filter-geneqv-lst (cdar congruences) ens)
                  ans
                  wrld))))
          (t ans))))))

(defun geneqv-lst
  (fn geneqv ens wrld)
  (cond ((flambdap fn) nil)
    ((eq fn 'if) (list *geneqv-iff* geneqv geneqv))
    (t (let ((congruences (getpropc fn 'congruences nil wrld)))
        (cond ((null congruences) nil)
          ((null geneqv) (filter-geneqv-lst (cdr (assoc-eq 'equal congruences)) ens))
          (t (geneqv-lst1 congruences geneqv ens wrld)))))))

(defun subst-expr-error
  (const)
  (declare (xargs :guard nil))
  (er hard
    'subst-expr-error
    "An attempt was made to substitute for the explicit value ~x0.  ~
       The substitution functions were optimized to disallow this."
    const))

(defun subst-expr
  (new old term)
  (declare (xargs :guard (and (pseudo-termp new)
        (pseudo-termp old)
        (not (quotep old))
        (pseudo-termp term))))
  (cond ((variablep old) (subst-var new old term))
    ((fquotep old) (subst-expr-error old))
    (t (subst-expr1 new old term))))

(defun comment-fn
  (x y)
  (declare (xargs :guard t))
  `(return-last 'progn '(:comment . ,X) ,Y))

(defun hide-with-comment
  (reason term wrld state)
  (declare (xargs :mode :program :stobjs state))
  (cond ((or (null reason) (null (hide-with-comment-p))) (fcons-term* 'hide term))
    (t (flet ((comment-fn+ (x y)
           (comment-fn (concatenate 'string
               x
               ";
see :DOC comment")
             y)) (reason-string (erp scons-term-p wrld state)
            (let* ((fn (and (consp erp)
                   (eq (car erp) 'ev-fncall-null-body-er)
                   (symbolp (cdr erp))
                   (cdr erp))) (fn (if (eq fn :non-exec)
                    'non-exec
                    fn)))
              (and fn
                (let* ((non-executablep (getpropc fn 'non-executablep nil wrld)) (skip-pkg-prefix (symbol-in-current-package-p fn state))
                    (str0 (if scons-term-p
                        "Failed attempt (during substitution) to call "
                        "Failed attempt to call "))
                    (str1 (cond ((eq fn 'non-exec) "")
                        (non-executablep "non-executable function ")
                        (t "constrained function ")))
                    (str2 (cond ((or (eq fn 'non-exec) (null (attachment-pair fn wrld))) "")
                        ((warrant-function-namep fn wrld) ":
warrant functions are not executable during proofs")
                        (t ":
its attachment is ignored during proofs"))))
                  (if skip-pkg-prefix
                    (concatenate 'string str0 str1 (symbol-name fn) str2)
                    (concatenate 'string
                      str0
                      str1
                      (symbol-package-name fn)
                      "::"
                      (symbol-name fn)
                      str2)))))))
        (case-match reason
          ((:non-executable . erp) (let ((reason-string (reason-string erp nil wrld state)))
              (fcons-term* 'hide
                (if reason-string
                  (comment-fn+ reason-string term)
                  term))))
          ((:scons-term . erp) (let ((reason-string (reason-string erp t wrld state)))
              (fcons-term* 'hide
                (if reason-string
                  (comment-fn+ reason-string term)
                  term))))
          ((:expand rune . skip-pkg-prefix) (fcons-term* 'hide
              (comment-fn+ (let ((name (if skip-pkg-prefix
                       (symbol-name (base-symbol rune))
                       (concatenate 'string
                         (symbol-package-name (base-symbol rune))
                         "::"
                         (symbol-name (base-symbol rune))))))
                  (concatenate 'string
                    "Unable to expand using the rule "
                    name))
                term)))
          ((:missing-warrant . fn?) (fcons-term* 'hide
              (comment-fn+ (let* ((disabledp (consp fn?)) (fn (if disabledp
                        (car fn?)
                        fn?))
                    (skip-pkg-prefix (symbol-in-current-package-p fn state))
                    (fn-str (if skip-pkg-prefix
                        (symbol-name fn)
                        (concatenate 'string
                          (symbol-package-name fn)
                          "::"
                          (symbol-name fn)))))
                  (concatenate 'string
                    "Call failed because "
                    (if disabledp
                      (concatenate 'string "the rule " fn-str " is disabled")
                      (concatenate 'string
                        "the warrant for "
                        fn-str
                        " is not known to be true"))))
                term)))
          (& (er hard
              'hide-with-comment
              "Unexpected reason supplied to ~x0!"
              'hide-with-comment)))))))

(defun scons-term
  (fn args ens wrld state ttree)
  (cond ((and (all-quoteps args)
       (or (flambdap fn)
         (and (enabled-xfnp fn ens wrld)
           (not (getpropc fn 'constrainedp nil wrld))))) (cond ((flambdap fn) (mv nil (cons-term fn args) ttree))
        ((eq fn 'if) (mv t
            (if (cadr (car args))
              (cadr args)
              (caddr args))
            ttree))
        ((programp fn wrld) (mv nil (cons-term fn args) ttree))
        (t (mv-let (erp val bad-fn)
            (pstk (ev-fncall+ fn (strip-cadrs args) t state))
            (cond (erp (cond (bad-fn (mv nil (cons-term fn args) ttree))
                  (t (mv t
                      (hide-with-comment (cons :scons-term erp)
                        (cons-term fn args)
                        wrld
                        state)
                      (push-lemma (fn-rune-nume 'hide nil nil wrld) ttree)))))
              (t (mv t
                  (kwote val)
                  (push-lemma (fn-rune-nume fn nil t wrld) ttree))))))))
    ((and (eq fn 'equal) (equal (car args) (cadr args))) (mv t *t* (puffert ttree)))
    (t (mv nil (cons-term fn args) ttree))))

(defun subst-equiv-expr
  (equiv new old geneqv term ens wrld state ttree)
  (cond ((and (nvariablep old) (fquotep old)) (mv (subst-expr-error old) term ttree))
    (t (subst-equiv-expr1 equiv
        new
        old
        geneqv
        term
        ens
        wrld
        state
        ttree))))

(defun next-pequiv
  (pequiv rewritten-args-rev rest-args alist)
  (let ((pattern (access pequiv pequiv :pattern)))
    (mv-let (flg unify-subst)
      (one-way-unify1-term-alist-lst (access pequiv-pattern pattern :pre-rev)
        rewritten-args-rev
        nil
        (access pequiv pequiv :unify-subst))
      (cond ((null flg) nil)
        (t (mv-let (flg unify-subst)
            (one-way-unify1-term-alist-lst (access pequiv-pattern pattern :post)
              rest-args
              alist
              unify-subst)
            (cond ((null flg) nil)
              ((equal (access pequiv pequiv :unify-subst) unify-subst) (change pequiv
                  pequiv
                  :pattern (access pequiv-pattern pattern :next)))
              (t (change pequiv
                  pequiv
                  :pattern (access pequiv-pattern pattern :next)
                  :unify-subst unify-subst)))))))))

(defun next-pequivs
  (deep-pequiv-lst rewritten-args-rev
    rest-args
    alist
    bkptr
    parent-fn
    child-fn
    ens
    next-deep-pequiv-lst
    next-shallow-pequiv-lst)
  (cond ((endp deep-pequiv-lst) (mv next-deep-pequiv-lst next-shallow-pequiv-lst))
    (t (let* ((deep-pequiv (car deep-pequiv-lst)) (pat (access pequiv deep-pequiv :pattern))
          (next (access pequiv-pattern pat :next))
          (next-pequiv (assert$ (not (variablep next))
              (and (eq parent-fn (access pequiv-pattern pat :fn))
                (eql bkptr (access pequiv-pattern pat :posn))
                (if child-fn
                  (eq child-fn (access pequiv-pattern next :fn))
                  (enabled-numep (access congruence-rule
                      (access pequiv deep-pequiv :congruence-rule)
                      :nume)
                    ens))
                (next-pequiv deep-pequiv rewritten-args-rev rest-args alist)))))
        (cond ((not next-pequiv) (next-pequivs (cdr deep-pequiv-lst)
              rewritten-args-rev
              rest-args
              alist
              bkptr
              parent-fn
              child-fn
              ens
              next-deep-pequiv-lst
              next-shallow-pequiv-lst))
          ((variablep (access pequiv-pattern next :next)) (next-pequivs (cdr deep-pequiv-lst)
              rewritten-args-rev
              rest-args
              alist
              bkptr
              parent-fn
              child-fn
              ens
              next-deep-pequiv-lst
              (cons next-pequiv next-shallow-pequiv-lst)))
          (t (next-pequivs (cdr deep-pequiv-lst)
              rewritten-args-rev
              rest-args
              alist
              bkptr
              parent-fn
              child-fn
              ens
              (cons next-pequiv next-deep-pequiv-lst)
              next-shallow-pequiv-lst)))))))

(defun next-pequivs-alist
  (deep-pequiv-alist rewritten-args-rev
    rest-args
    alist
    bkptr
    parent-fn
    parent-geneqv
    wrld
    ens
    next-deep-pequiv-lst
    next-shallow-pequiv-lst)
  (cond ((endp deep-pequiv-alist) (mv next-deep-pequiv-lst next-shallow-pequiv-lst))
    ((geneqv-refinementp (caar deep-pequiv-alist)
       parent-geneqv
       wrld) (mv-let (next-deep-pequiv-lst next-shallow-pequiv-lst)
        (next-pequivs (cdar deep-pequiv-alist)
          rewritten-args-rev
          rest-args
          alist
          bkptr
          parent-fn
          nil
          ens
          next-deep-pequiv-lst
          next-shallow-pequiv-lst)
        (next-pequivs-alist (cdr deep-pequiv-alist)
          rewritten-args-rev
          rest-args
          alist
          bkptr
          parent-fn
          parent-geneqv
          wrld
          ens
          next-deep-pequiv-lst
          next-shallow-pequiv-lst)))
    (t (next-pequivs-alist (cdr deep-pequiv-alist)
        rewritten-args-rev
        rest-args
        alist
        bkptr
        parent-fn
        parent-geneqv
        wrld
        ens
        next-deep-pequiv-lst
        next-shallow-pequiv-lst))))

(defun extend-pequiv-lst
  (pequiv-lst ens acc)
  (cond ((endp pequiv-lst) acc)
    (t (extend-pequiv-lst (cdr pequiv-lst)
        ens
        (cond ((enabled-numep (access congruence-rule
               (access pequiv (car pequiv-lst) :congruence-rule)
               :nume)
             ens) (cons (car pequiv-lst) acc))
          (t acc))))))

(defun accumulate-shallow-pequiv-alist
  (alist geneqv wrld ens acc)
  (cond ((endp alist) acc)
    (t (accumulate-shallow-pequiv-alist (cdr alist)
        geneqv
        wrld
        ens
        (cond ((geneqv-refinementp (caar alist) geneqv wrld) (extend-pequiv-lst (cdar alist) ens acc))
          (t acc))))))

(defun pequivs-for-rewrite-args
  (fn geneqv pequiv-info wrld ens)
  (cond ((flambdap fn) (mv nil nil))
    (t (let* ((prop (getpropc fn 'pequivs nil wrld)) (shallow-pequiv-alist (pequivs-property-field prop :shallow)))
        (cond ((not pequiv-info) (mv (and (pequivs-property-field prop :deep-pequiv-p) :none)
              (accumulate-shallow-pequiv-alist shallow-pequiv-alist
                geneqv
                wrld
                ens
                nil)))
          (t (let ((deep-pequiv-lst (access pequiv-info pequiv-info :deep-pequiv-lst)) (rewritten-args-rev (access pequiv-info pequiv-info :rewritten-args-rev))
                (rest-args (access pequiv-info pequiv-info :rest-args))
                (alist (access pequiv-info pequiv-info :alist))
                (bkptr (access pequiv-info pequiv-info :bkptr))
                (parent-fn (access pequiv-info pequiv-info :fn)))
              (mv-let (next-deep-pequiv-lst next-shallow-pequiv-lst)
                (next-pequivs deep-pequiv-lst
                  rewritten-args-rev
                  rest-args
                  alist
                  bkptr
                  parent-fn
                  fn
                  nil
                  nil
                  nil)
                (mv-let (next-deep-pequiv-lst next-shallow-pequiv-lst)
                  (next-pequivs-alist (pequivs-property-field prop :deep)
                    rewritten-args-rev
                    rest-args
                    alist
                    bkptr
                    parent-fn
                    (access pequiv-info pequiv-info :geneqv)
                    wrld
                    ens
                    next-deep-pequiv-lst
                    next-shallow-pequiv-lst)
                  (mv (or next-deep-pequiv-lst
                      (and (pequivs-property-field prop :deep-pequiv-p) :none))
                    (accumulate-shallow-pequiv-alist shallow-pequiv-alist
                      geneqv
                      wrld
                      ens
                      next-shallow-pequiv-lst)))))))))))

(defun pequiv-info-for-rewrite
  (fn bkptr
    rewritten-args-rev
    args
    alist
    geneqv
    deep-pequiv-lst)
  (cond ((or (null deep-pequiv-lst)
       (flambdap fn)
       (variablep (car args))
       (fquotep (car args))) nil)
    (t (make pequiv-info
        :rewritten-args-rev rewritten-args-rev
        :rest-args (cdr args)
        :alist alist
        :bkptr bkptr
        :fn fn
        :geneqv geneqv
        :deep-pequiv-lst (and (consp deep-pequiv-lst) deep-pequiv-lst)))))

(defun reduce-geneqv-for-equiv
  (equiv wrld geneqv)
  (cond ((endp geneqv) (mv nil nil))
    (t (mv-let (changedp rest)
        (reduce-geneqv-for-equiv equiv wrld (cdr geneqv))
        (cond ((refinementp (access congruence-rule (car geneqv) :equiv)
             equiv
             wrld) (mv t rest))
          (changedp (mv t (cons (car geneqv) rest)))
          (t (mv nil geneqv)))))))

(defun geneqv-for-rewrite
  (shallow-pequiv-lst fn
    bkptr
    rewritten-args-rev
    rest-args
    alist
    wrld
    geneqv)
  (cond ((null shallow-pequiv-lst) geneqv)
    (t (let* ((pequiv (car shallow-pequiv-lst)) (pat (access pequiv pequiv :pattern))
          (congruence-rule (access pequiv pequiv :congruence-rule))
          (equiv (access congruence-rule congruence-rule :equiv)))
        (geneqv-for-rewrite (cdr shallow-pequiv-lst)
          fn
          bkptr
          rewritten-args-rev
          rest-args
          alist
          wrld
          (cond ((or (not (eq fn (access pequiv-pattern pat :fn)))
               (not (eql bkptr (access pequiv-pattern pat :posn)))
               (geneqv-refinementp equiv geneqv wrld)) geneqv)
            (t (mv-let (flg unify-subst)
                (one-way-unify1-term-alist-lst (access pequiv-pattern pat :pre-rev)
                  rewritten-args-rev
                  nil
                  (access pequiv pequiv :unify-subst))
                (cond ((null flg) geneqv)
                  (t (mv-let (flg unify-subst)
                      (one-way-unify1-term-alist-lst (access pequiv-pattern pat :post)
                        rest-args
                        alist
                        unify-subst)
                      (declare (ignore unify-subst))
                      (cond ((null flg) geneqv)
                        (t (mv-let (changedp geneqv)
                            (reduce-geneqv-for-equiv equiv wrld geneqv)
                            (declare (ignore changedp))
                            (cons congruence-rule geneqv)))))))))))))))

(defun geneqv-and-pequiv-info-for-rewrite
  (fn bkptr
    rewritten-args-rev
    args
    alist
    parent-geneqv
    child-geneqv
    deep-pequiv-lst
    shallow-pequiv-lst
    wrld)
  (mv (geneqv-for-rewrite shallow-pequiv-lst
      fn
      bkptr
      rewritten-args-rev
      (cdr args)
      alist
      wrld
      child-geneqv)
    (pequiv-info-for-rewrite fn
      bkptr
      rewritten-args-rev
      args
      alist
      parent-geneqv
      deep-pequiv-lst)))

(defun comm-equal
  (fn lhs rhs term)
  (and (nvariablep term)
    (not (fquotep term))
    (eq fn (ffn-symb term))
    (if (equal rhs (fargn term 2))
      (equal lhs (fargn term 1))
      (and (equal rhs (fargn term 1)) (equal lhs (fargn term 2))))))

(defun member-term2
  (fn lhs rhs cl)
  (cond ((null cl) nil)
    ((comm-equal fn lhs rhs (car cl)) cl)
    (t (member-term2 fn lhs rhs (cdr cl)))))

(defun member-complement-term2
  (fn lhs rhs cl)
  (cond ((null cl) nil)
    ((and (ffn-symb-p (car cl) 'not)
       (comm-equal fn lhs rhs (fargn (car cl) 1))) cl)
    (t (member-complement-term2 fn lhs rhs (cdr cl)))))

(defun member-complement-term1
  (lit cl)
  (cond ((null cl) nil)
    ((and (ffn-symb-p (car cl) 'not)
       (equal lit (fargn (car cl) 1))) cl)
    (t (member-complement-term1 lit (cdr cl)))))

(defun instr-listp
  (l)
  (cond ((atom l) (equal l nil))
    (t (and (or (integerp (car l))
          (let ((carl (car l)))
            (case-match carl
              (('push . x) (pseudo-termp x))
              (('push-local . n) (integerp n))
              (('push-frame-ptr) t)
              (('go . x) (integerp x))
              (('test . x) (integerp x))
              (('call . term) (pseudo-termp term))
              (('ret . lst) (pseudo-term-listp lst)))))
        (instr-listp (cdr l))))))

(defun spliced-instr-listp
  (l)
  (cond ((atom l) (equal l nil))
    (t (and (let ((carl (car l)))
          (case-match carl
            (('push . x) (pseudo-termp x))
            (('push-local . n) (integerp n))
            (('push-frame-ptr) t)
            (('test . x) (spliced-instr-listp x))
            (('call . term) (pseudo-termp term))
            (('ret . lst) (pseudo-term-listp lst))))
        (spliced-instr-listp (cdr l))))))

(defun next-tag
  (l)
  (declare (xargs :guard (instr-listp l)))
  (cond ((null l) 1)
    ((and (consp (car l)) (eq (caar l) 'test)) (+ 2 (cdr (car l))))
    (t (next-tag (cdr l)))))

(defun if-compile-formal
  (var rformals i)
  (declare (xargs :guard (and (symbolp var)
        (true-listp rformals)
        (member-eq var rformals))))
  (cond ((eq var (car rformals)) i)
    (t (if-compile-formal var (cdr rformals) (1+ i)))))

(defun if-interp-assume-true
  (not-flg term assumptions)
  (cond ((variablep term) (if not-flg
        (cons :not (cons term assumptions))
        (cons term assumptions)))
    ((eq (ffn-symb term) 'not) (if-interp-assume-true (not not-flg)
        (fargn term 1)
        assumptions))
    (t (if not-flg
        (cons :not (cons term assumptions))
        (cons term assumptions)))))

(defun if-interp-switch
  (assumptions)
  (cond ((eq (car assumptions) :not) (cdr assumptions))
    (t (cons :not assumptions))))

(defun if-interp-assumed-value0
  (var assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (cond ((eq var (cadr assumptions)) 'f)
        (t (if-interp-assumed-value0 var (cddr assumptions)))))
    ((eq (car assumptions) var) 't)
    (t (if-interp-assumed-value0 var (cdr assumptions)))))

(defun if-interp-assumed-value1
  (term assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (cond ((equal term (cadr assumptions)) 'f)
        (t (if-interp-assumed-value1 term (cddr assumptions)))))
    ((equal (car assumptions) term) 't)
    (t (if-interp-assumed-value1 term (cdr assumptions)))))

(defun if-interp-assumed-value2-equal-constant
  (arg const1 assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (let ((term (cadr assumptions)))
        (cond ((variablep term) (if-interp-assumed-value2-equal-constant arg
              const1
              (cddr assumptions)))
          ((and (eq 'equal (ffn-symb term))
             (or (and (equal arg (fargn term 1))
                 (equal const1 (fargn term 2)))
               (and (equal arg (fargn term 2))
                 (equal const1 (fargn term 1))))) 'f)
          (t (if-interp-assumed-value2-equal-constant arg
              const1
              (cddr assumptions))))))
    (t (let ((term (car assumptions)))
        (cond ((variablep term) (if-interp-assumed-value2-equal-constant arg
              const1
              (cdr assumptions)))
          (t (let ((term-fn (ffn-symb term)))
              (cond ((eq term-fn 'equal) (cond ((or (and (equal arg (fargn term 1))
                         (equal const1 (fargn term 2)))
                       (and (equal arg (fargn term 2))
                         (equal const1 (fargn term 1)))) 't)
                    ((or (and (equal arg (fargn term 1))
                         (quotep (fargn term 2))
                         (not (equal const1 (fargn term 2))))
                       (and (equal arg (fargn term 2))
                         (quotep (fargn term 1))
                         (not (equal const1 (fargn term 1))))) 'f)
                    (t (if-interp-assumed-value2-equal-constant arg
                        const1
                        (cdr assumptions)))))
                (t (if-interp-assumed-value2-equal-constant arg
                    const1
                    (cdr assumptions)))))))))))

(defun if-interp-assumed-value2
  (fn arg1 arg2 assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (let ((term (cadr assumptions)))
        (cond ((variablep term) (if-interp-assumed-value2 fn arg1 arg2 (cddr assumptions)))
          ((and (eq fn (ffn-symb term))
             (or (and (equal arg1 (fargn term 1))
                 (equal arg2 (fargn term 2)))
               (and (equal arg1 (fargn term 2))
                 (equal arg2 (fargn term 1))))) 'f)
          (t (if-interp-assumed-value2 fn arg1 arg2 (cddr assumptions))))))
    ((let* ((term (car assumptions)) (term-fn (and (nvariablep term) (ffn-symb term))))
       (and (eq fn term-fn)
         (or (and (equal arg1 (fargn term 1))
             (equal arg2 (fargn term 2)))
           (and (equal arg1 (fargn term 2))
             (equal arg2 (fargn term 1)))))) 't)
    (t (if-interp-assumed-value2 fn arg1 arg2 (cdr assumptions)))))

(defun if-interp-assumed-value3
  (term assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (cond ((equal term (cadr assumptions)) 'f)
        (t (if-interp-assumed-value3 term (cddr assumptions)))))
    ((equal (car assumptions) term) 't)
    ((and (ffn-symb-p (car assumptions) 'integerp)
       (equal (fargn term 1) (fargn (car assumptions) 1))) 't)
    (t (if-interp-assumed-value3 term (cdr assumptions)))))

(defun if-interp-assumed-value4
  (term assumptions)
  (cond ((null assumptions) nil)
    ((eq (car assumptions) :not) (cond ((equal term (cadr assumptions)) 'f)
        ((and (ffn-symb-p (cadr assumptions) 'rationalp)
           (equal (fargn term 1) (fargn (cadr assumptions) 1))) 'f)
        (t (if-interp-assumed-value4 term (cddr assumptions)))))
    ((equal (car assumptions) term) 't)
    (t (if-interp-assumed-value4 term (cdr assumptions)))))

(defun if-interp-assumed-value-x
  (term assumptions)
  (cond ((variablep term) (if-interp-assumed-value0 term assumptions))
    ((eq (ffn-symb term) 'equal) (cond ((quotep (fargn term 1)) (if-interp-assumed-value2-equal-constant (fargn term 2)
            (fargn term 1)
            assumptions))
        ((quotep (fargn term 2)) (if-interp-assumed-value2-equal-constant (fargn term 1)
            (fargn term 2)
            assumptions))
        (t (if-interp-assumed-value2 (ffn-symb term)
            (fargn term 1)
            (fargn term 2)
            assumptions))))
    ((eq (ffn-symb term) 'iff) (if-interp-assumed-value2 (ffn-symb term)
        (fargn term 1)
        (fargn term 2)
        assumptions))
    ((eq (ffn-symb term) 'rationalp) (if-interp-assumed-value3 term assumptions))
    ((eq (ffn-symb term) 'integerp) (if-interp-assumed-value4 term assumptions))
    (t (if-interp-assumed-value1 term assumptions))))

(defun if-interp-assumed-value
  (term assumptions)
  (cond ((variablep term) (if-interp-assumed-value0 term assumptions))
    ((eq (ffn-symb term) 'not) (let ((temp (if-interp-assumed-value-x (fargn term 1) assumptions)))
        (cond ((eq temp t) 'f) ((eq temp 'f) t) (t nil))))
    (t (if-interp-assumed-value-x term assumptions))))

(defun convert-assumptions-to-clause-segment
  (assumptions ans known-constants)
  (cond ((or (null assumptions)
       (eq (car assumptions) :ignore-when-converting-to-clause)) ans)
    ((eq (car assumptions) :not) (let ((test (cadr assumptions)))
        (cond ((and (ffn-symb-p test 'equal)
             (or (quotep (fargn test 1)) (quotep (fargn test 2)))) (cond ((quotep (fargn test 1)) (let* ((x (fargn test 2)) (const2 (fargn test 1))
                    (temp (assoc-equal x known-constants)))
                  (cond ((and temp (not (equal const2 (cdr temp)))) (convert-assumptions-to-clause-segment (cddr assumptions)
                        ans
                        known-constants))
                    (t (convert-assumptions-to-clause-segment (cddr assumptions)
                        (cons test ans)
                        known-constants)))))
              ((quotep (fargn test 2)) (let* ((x (fargn test 1)) (const2 (fargn test 2))
                    (temp (assoc-equal x known-constants)))
                  (cond ((and temp (not (equal const2 (cdr temp)))) (convert-assumptions-to-clause-segment (cddr assumptions)
                        ans
                        known-constants))
                    (t (convert-assumptions-to-clause-segment (cddr assumptions)
                        (cons test ans)
                        known-constants)))))
              (t (convert-assumptions-to-clause-segment (cddr assumptions)
                  (cons test ans)
                  known-constants))))
          (t (convert-assumptions-to-clause-segment (cddr assumptions)
              (cons test ans)
              known-constants)))))
    (t (let ((test (car assumptions)))
        (cond ((and (ffn-symb-p test 'equal)
             (or (quotep (fargn test 1)) (quotep (fargn test 2)))) (cond ((quotep (fargn test 1)) (convert-assumptions-to-clause-segment (cdr assumptions)
                  (cons (list 'not test) ans)
                  (cons (cons (fargn test 2) (fargn test 1)) known-constants)))
              ((quotep (fargn test 2)) (convert-assumptions-to-clause-segment (cdr assumptions)
                  (cons (list 'not test) ans)
                  (cons (cons (fargn test 1) (fargn test 2)) known-constants)))
              (t (convert-assumptions-to-clause-segment (cdr assumptions)
                  (cons (list 'not test) ans)
                  known-constants))))
          (t (convert-assumptions-to-clause-segment (cdr assumptions)
              (cons (list 'not test) ans)
              known-constants)))))))

(defun convert-clause-to-assumptions
  (clause ans)
  (cond ((null clause) (cons :ignore-when-converting-to-clause ans))
    (t (convert-clause-to-assumptions (cdr clause)
        (if-interp-assume-true t (car clause) ans)))))

(defun simplifiable-mv-nth1
  (n cons-term alist)
  (cond ((variablep cons-term) (let ((temp (assoc-eq cons-term alist)))
        (cond (temp (mv-let (term1 rewritep)
              (simplifiable-mv-nth1 n (cdr temp) nil)
              (declare (ignore rewritep))
              (mv term1 nil)))
          (t (mv nil nil)))))
    ((fquotep cons-term) (cond ((and (true-listp (cadr cons-term))
           (> (length (cadr cons-term)) n)) (mv (kwote (nth n (cadr cons-term))) t))
        (t (mv nil nil))))
    ((eq (ffn-symb cons-term) 'cons) (if (= n 0)
        (mv (fargn cons-term 1) t)
        (simplifiable-mv-nth1 (1- n) (fargn cons-term 2) alist)))
    (t (mv nil nil))))

(defun simplifiable-mv-nth
  (term alist)
  (cond ((simplifiable-mv-nth-p) (let ((arg1 (cond ((variablep (fargn term 1)) (let ((temp (assoc-eq (fargn term 1) alist)))
                 (cond (temp (cdr temp)) (t (fargn term 1)))))
             (t (fargn term 1)))))
        (cond ((and (quotep arg1)
             (integerp (cadr arg1))
             (>= (cadr arg1) 0)) (simplifiable-mv-nth1 (cadr arg1) (fargn term 2) alist))
          (t (mv nil nil)))))
    (t (mv nil nil))))

(defun call-stack
  (fn lst stack assumptions ac)
  (declare (xargs :guard (and (true-listp lst)
        (true-listp stack)
        (>= (length stack) (length lst)))))
  (cond ((null lst) (cons (cond ((eq fn 'not) (let ((x (car ac)))
              (cond ((quotep x) (if (eq (cadr x) nil)
                    *t*
                    *nil*))
                (t (let ((temp (if-interp-assumed-value x assumptions)))
                    (cond ((eq temp t) *nil*)
                      ((eq temp 'f) *t*)
                      (t (list 'not x))))))))
          ((eq fn 'equal) (cond ((equal (car ac) (cadr ac)) *t*)
              ((and (quotep (car ac)) (quotep (cadr ac))) *nil*)
              ((and (equal (car ac) *t*) (ffn-symb-p (cadr ac) 'equal)) (cadr ac))
              ((and (equal (cadr ac) *t*) (ffn-symb-p (car ac) 'equal)) (car ac))
              (t (fcons-term fn ac))))
          ((eq fn '<) (cond ((equal (car ac) (cadr ac)) *nil*)
              ((and (quotep (car ac))
                 (quotep (cadr ac))
                 (rationalp (cadr (car ac)))
                 (rationalp (cadr (cadr ac)))) (if (< (cadr (car ac)) (cadr (cadr ac)))
                  *t*
                  *nil*))
              (t (cons-term fn ac))))
          ((eq fn 'iff) (let ((arg1 (car ac)) (arg2 (cadr ac)))
              (cond ((equal arg1 arg2) *t*)
                (t (let ((temp1 (if (quotep arg1)
                         (if (eq (cadr arg1) nil)
                           'f
                           t)
                         (if-interp-assumed-value arg1 assumptions))) (temp2 (if (quotep arg2)
                          (if (eq (cadr arg2) nil)
                            'f
                            t)
                          (if-interp-assumed-value arg2 assumptions))))
                    (cond ((and temp1 temp2) (if (eq temp1 temp2)
                          *t*
                          *nil*))
                      (t (fcons-term fn ac))))))))
          ((eq fn 'mv-nth) (let ((term (fcons-term fn ac)))
              (mv-let (term1 rewritep)
                (simplifiable-mv-nth term nil)
                (declare (ignore rewritep))
                (or term1 term))))
          (t (cons-term fn ac)))
        stack))
    (t (call-stack fn
        (cdr lst)
        (cdr stack)
        assumptions
        (cons (car stack) ac)))))

(defun ret-stack
  (lst stack)
  (cond ((null lst) stack)
    (t (ret-stack (cdr lst) (cdr stack)))))

(defun extra-info-lit-p
  (lit)
  (and (ffn-symb-p lit 'not)
    (let ((atm (fargn lit 1)))
      (and (nvariablep atm) (eq (ffn-symb atm) *extra-info-fn*)))))

(defun subsetp-equal-mod-extra-info-lits
  (x y)
  (declare (xargs :guard (and (true-listp y) (true-listp x))))
  (cond ((endp x) t)
    ((or (extra-info-lit-p (car x)) (member-equal (car x) y)) (subsetp-equal-mod-extra-info-lits (cdr x) y))
    (t nil)))

(defun quick-and-dirty-subsumption-replacement-step1
  (cl1 cl2)
  (cond ((null cl1) 'subsumed2)
    ((extra-info-lit-p (car cl1)) (quick-and-dirty-subsumption-replacement-step1 (cdr cl1)
        cl2))
    ((null cl2) 'subsumed1)
    ((extra-info-lit-p (car cl2)) (quick-and-dirty-subsumption-replacement-step1 cl1
        (cdr cl2)))
    ((equal (car cl1) (car cl2)) (let ((ans (quick-and-dirty-subsumption-replacement-step1 (cdr cl1)
             (cdr cl2))))
        (cond ((symbolp ans) ans) (t (cons (car cl1) ans)))))
    ((and (complementaryp (car cl1) (car cl2))
       (subsetp-equal-mod-extra-info-lits (cdr cl1) (cdr cl2))) (cdr cl2))
    (t nil)))

(defun quick-and-dirty-subsumption-replacement-step
  (cl1 lst)
  (cond ((null lst) nil)
    ((time-limit5-reached-p "Out of time in subsumption ~
      (quick-and-dirty-subsumption-replacement-step).") nil)
    (t (let ((cl3 (quick-and-dirty-subsumption-replacement-step1 cl1
             (car lst))))
        (cond ((eq cl3 'subsumed1) 'subsumed1)
          (t (let ((ans (quick-and-dirty-subsumption-replacement-step cl1 (cdr lst))))
              (cond ((eq cl3 'subsumed2) ans)
                ((eq ans 'subsumed1) ans)
                ((null cl3) (cons (car lst) ans))
                (t (cons cl3 ans))))))))))

(defun quick-and-dirty-srs-builtin
  (cl1 ac)
  (declare (ignore cl1 ac)
    (xargs :mode :logic :guard t))
  t)

(defun if-interp-add-clause
  (assumptions cl ac pflg)
  (cond (pflg t)
    (t (let ((cl1 (convert-assumptions-to-clause-segment assumptions cl nil)))
        (cond ((quick-and-dirty-srs cl1 ac) (let ((ans (quick-and-dirty-subsumption-replacement-step cl1 ac)))
              (cond ((eq ans 'subsumed1) ac) (t (cons cl1 ans)))))
          (t (cons cl1 ac)))))))

(defun if-interp
  (instrs stack frame-ptr-stack assumptions ac pflg)
  (declare (type (or null (unsigned-byte 60)) pflg))
  (cond ((null instrs) (let ((v (car stack)))
        (or (cond ((quotep v) (cond ((equal v *nil*) (if-interp-add-clause assumptions nil ac pflg))
                (t ac)))
            (t (let ((assumed-val (if-interp-assumed-value v assumptions)))
                (cond ((eq assumed-val t) ac)
                  ((eq assumed-val 'f) (if-interp-add-clause assumptions nil ac pflg))
                  (t (if-interp-add-clause assumptions (list v) ac pflg))))))
          pflg)))
    ((and pflg (zpf pflg)) 0)
    (t (let ((caarinstrs (caar instrs)) (pflg (and pflg (1-f pflg))))
        (declare (type (or null (unsigned-byte 60)) pflg))
        (case caarinstrs
          (push (if-interp (cdr instrs)
              (cons (cdr (car instrs)) stack)
              frame-ptr-stack
              assumptions
              ac
              pflg))
          (push-local (if-interp (cdr instrs)
              (cons (nth (cdr (car instrs)) (car frame-ptr-stack)) stack)
              frame-ptr-stack
              assumptions
              ac
              pflg))
          (push-frame-ptr (if-interp (cdr instrs)
              stack
              (cons stack frame-ptr-stack)
              assumptions
              ac
              pflg))
          (ret (if-interp (cdr instrs)
              (cons (car stack)
                (ret-stack (cdr (car instrs)) (cdr stack)))
              (cdr frame-ptr-stack)
              assumptions
              ac
              pflg))
          (call (if-interp (cdr instrs)
              (call-stack (cadr (car instrs))
                (cddr (car instrs))
                stack
                assumptions
                nil)
              frame-ptr-stack
              assumptions
              ac
              pflg))
          (test (let* ((v (car stack)) (stack (cdr stack)))
              (cond ((quotep v) (cond ((equal v *nil*) (if-interp (cdr (car instrs))
                        stack
                        frame-ptr-stack
                        assumptions
                        ac
                        pflg))
                    (t (if-interp (cdr instrs)
                        stack
                        frame-ptr-stack
                        assumptions
                        ac
                        pflg))))
                (t (let ((temp (if-interp-assumed-value v assumptions)))
                    (cond ((eq temp 'f) (if-interp (cdr (car instrs))
                          stack
                          frame-ptr-stack
                          assumptions
                          ac
                          pflg))
                      ((eq temp t) (if-interp (cdr instrs)
                          stack
                          frame-ptr-stack
                          assumptions
                          ac
                          pflg))
                      (pflg (let ((assumptions (if-interp-assume-true nil v assumptions)))
                          (let ((pflg (if-interp (cdr instrs)
                                 stack
                                 frame-ptr-stack
                                 assumptions
                                 ac
                                 pflg)))
                            (cond ((eq pflg t) t)
                              (t (if-interp (cdr (car instrs))
                                  stack
                                  frame-ptr-stack
                                  (if-interp-switch assumptions)
                                  ac
                                  pflg))))))
                      (t (let ((assumptions (if-interp-assume-true nil v assumptions)))
                          (if-interp (cdr instrs)
                            stack
                            frame-ptr-stack
                            assumptions
                            (if-interp (cdr (car instrs))
                              stack
                              frame-ptr-stack
                              (if-interp-switch assumptions)
                              ac
                              pflg)
                            pflg))))))))))))))

(defun splice-instrs1
  (instrs ans alist)
  (declare (xargs :guard (instr-listp instrs)))
  (cond ((null instrs) ans)
    ((atom (car instrs)) (splice-instrs1 (cdr instrs)
        ans
        (cons (cons (car instrs) ans) alist)))
    (t (let ((caarinstrs (caar instrs)))
        (case caarinstrs
          ((push push-local push-frame-ptr call ret) (splice-instrs1 (cdr instrs) (cons (car instrs) ans) alist))
          (test (splice-instrs1 (cdr instrs)
              (cons (cons 'test (cdr (assoc (cdr (car instrs)) alist)))
                ans)
              alist))
          (go (splice-instrs1 (cdr instrs)
              (cdr (assoc (cdr (car instrs)) alist))
              alist)))))))

(defun splice-instrs
  (instrs)
  (declare (xargs :guard (instr-listp instrs)))
  (splice-instrs1 instrs nil nil))

(defun strip-branches
  (term assumptions lambda-exp)
  (declare (xargs :guard (pseudo-termp term)))
  (cond ((and (ffn-symb-p term 'if) (equal (fargn term 3) *nil*)) (union-equal (strip-branches (fargn term 1) assumptions lambda-exp)
        (strip-branches (fargn term 2) assumptions lambda-exp)))
    (t (if-interp (splice-instrs (if-compile term lambda-exp nil nil))
        nil
        nil
        assumptions
        nil
        nil))))

(defun merge-length
  (l1 l2)
  (declare (xargs :guard (and (true-list-listp l1) (true-list-listp l2))))
  (cond ((null l1) l2)
    ((null l2) l1)
    ((<= (length (car l1)) (length (car l2))) (cons (car l1) (merge-length (cdr l1) l2)))
    (t (cons (car l2) (merge-length l1 (cdr l2))))))

(defun merge-sort-length
  (l)
  (declare (xargs :guard (true-list-listp l)))
  (cond ((null (cdr l)) l)
    (t (merge-length (merge-sort-length (evens l))
        (merge-sort-length (odds l))))))

(defun member-equal-+-
  (lit clause)
  (cond ((null clause) nil)
    ((equal lit (car clause)) '+)
    ((complementaryp lit (car clause)) '-)
    (t (member-equal-+- lit (cdr clause)))))

(defun arg1-almost-subsumes-arg2
  (arg1 arg2)
  (declare (xargs :guard (and (pseudo-term-listp arg1) (pseudo-term-listp arg2))))
  (cond ((null arg1) 'subsumed)
    ((extra-info-lit-p (car arg1)) (arg1-almost-subsumes-arg2 (cdr arg1) arg2))
    (t (let ((sign (member-equal-+- (car arg1) arg2)))
        (cond ((null sign) nil)
          ((eq sign '+) (arg1-almost-subsumes-arg2 (cdr arg1) arg2))
          ((subsetp-equal-mod-extra-info-lits (cdr arg1) arg2) arg1)
          (t nil))))))

(defun find-subsumer-replacement-rec
  (cl l len-cl)
  (declare (xargs :guard (and (pseudo-term-listp cl)
        (pseudo-term-list-listp l)
        (equal len-cl (length cl)))))
  (cond ((null l) (mv nil nil))
    ((> (len (car l)) len-cl) (find-subsumer-replacement-rec cl (cdr l) len-cl))
    (t (let ((here (arg1-almost-subsumes-arg2 (car l) cl)))
        (cond ((eq here 'subsumed) (mv here (car l)))
          (t (mv-let (rst cl0)
              (find-subsumer-replacement-rec cl (cdr l) len-cl)
              (cond ((eq rst 'subsumed) (mv rst cl0))
                (t (mv (or here rst) nil))))))))))

(defun find-subsumer-replacement
  (cl l)
  (declare (xargs :guard (and (pseudo-term-listp cl) (pseudo-term-list-listp l))))
  (find-subsumer-replacement-rec cl l (length cl)))

(defun remove-one-complement
  (lit cl)
  (declare (xargs :guard (and (pseudo-termp lit) (pseudo-term-listp cl))))
  (cond ((null cl) nil)
    ((complementaryp lit (car cl)) (cdr cl))
    (t (cons (car cl) (remove-one-complement lit (cdr cl))))))

(defun weak-disc-tree
  (x)
  (and (or (consp x) (equal x nil))
    (cond ((equal (car x) 'node) (and (true-listp x)
          (equal (length x) 4)
          (pseudo-termp (cadr x))
          (weak-disc-tree (caddr x))
          (weak-disc-tree (cadddr x))))
      (t (pseudo-term-list-listp (cdr x))))))

(defun sweep-clauses1
  (tree ac)
  (declare (xargs :guard (weak-disc-tree tree)))
  (cond ((eq (car tree) 'node) (sweep-clauses1 (caddr tree)
        (sweep-clauses1 (cadddr tree) ac)))
    (t (append (cdr tree) ac))))

(defun sweep-clauses
  (tree)
  (declare (xargs :guard (weak-disc-tree tree)))
  (sweep-clauses1 tree nil))

(defun filter-with-and-without
  (x l with-lst without-lst)
  (cond ((null l) (mv with-lst without-lst))
    ((or (extra-info-lit-p x) (member-equal-+- x (car l))) (filter-with-and-without x
        (cdr l)
        (cons (car l) with-lst)
        without-lst))
    (t (filter-with-and-without x
        (cdr l)
        with-lst
        (cons (car l) without-lst)))))

(defun disc-tree
  (x)
  (and (or (consp x) (equal x nil))
    (cond ((equal (car x) 'node) (and (true-listp x)
          (equal (length x) 4)
          (pseudo-termp (cadr x))
          (disc-tree (caddr x))
          (disc-tree (cadddr x))
          (mv-let (with-lst without-lst)
            (filter-with-and-without (cadr x)
              (sweep-clauses (caddr x))
              nil
              nil)
            (declare (ignore with-lst))
            (null without-lst))
          (mv-let (with-lst without-lst)
            (filter-with-and-without (cadr x)
              (sweep-clauses (cadddr x))
              nil
              nil)
            (declare (ignore without-lst))
            (null with-lst))))
      (t (pseudo-term-list-listp (cdr x))))))

(defun find-clauses1
  (clause tree ac)
  (declare (xargs :guard (and (disc-tree tree)
        (pseudo-term-listp clause)
        (pseudo-term-list-listp ac))))
  (cond ((eq (car tree) 'node) (cond ((or (extra-info-lit-p (cadr tree))
           (member-equal-+- (cadr tree) clause)) (find-clauses1 clause
            (caddr tree)
            (find-clauses1 clause (cadddr tree) ac)))
        (t (find-clauses1 clause (cadddr tree) ac))))
    (t (append (cdr tree) ac))))

(defun find-clauses
  (clause tree)
  (find-clauses1 clause tree nil))

(defun remove-one-+-
  (x l)
  (cond ((null l) nil)
    ((equal x (car l)) (cdr l))
    ((complementaryp x (car l)) (cdr l))
    (t (cons (car l) (remove-one-+- x (cdr l))))))

(defun store-clause1
  (clause undisc-lits tree)
  (declare (xargs :guard (and (pseudo-term-listp clause)
        (pseudo-term-listp undisc-lits)
        (disc-tree tree))))
  (cond ((eq (car tree) 'node) (cond ((extra-info-lit-p (cadr tree)) (list 'node
            (cadr tree)
            (store-clause1 clause undisc-lits (caddr tree))
            (cadddr tree)))
        ((member-equal-+- (cadr tree) clause) (list 'node
            (cadr tree)
            (store-clause1 clause
              (remove-one-+- (cadr tree) undisc-lits)
              (caddr tree))
            (cadddr tree)))
        (t (list 'node
            (cadr tree)
            (caddr tree)
            (store-clause1 clause undisc-lits (cadddr tree))))))
    ((null undisc-lits) (cons 'tip (cons clause (cdr tree))))
    ((extra-info-lit-p (car undisc-lits)) (store-clause1 clause (cdr undisc-lits) tree))
    (t (mv-let (with-lst without-lst)
        (filter-with-and-without (car undisc-lits)
          (cdr tree)
          nil
          nil)
        (store-clause1 clause
          undisc-lits
          (list 'node
            (car undisc-lits)
            (cons 'tip with-lst)
            (cons 'tip without-lst)))))))

(defun store-clause (cl tree) (store-clause1 cl cl tree))

(defun substitute1-ac
  (new old seq acc)
  (declare (xargs :guard (and (true-listp acc)
        (true-listp seq)
        (member-equal old seq))))
  (cond ((endp seq) (er hard
        'substitute
        "Attempted to substitute ~x0 for ~x1 into a sequence in which the ~
         latter was not an element."
        new
        old))
    ((equal old (car seq)) (revappend acc (cons new (cdr seq))))
    (t (substitute1-ac new old (cdr seq) (cons (car seq) acc)))))

(defun substitute1
  (new old seq)
  (declare (xargs :guard (and (true-listp seq) (member-equal old seq))))
  (substitute1-ac new old seq nil))

(defun replace-clause1
  (clause undisc-lits new-clause tree)
  (declare (xargs :guard (and (pseudo-term-listp clause)
        (pseudo-term-listp undisc-lits)
        (disc-tree tree))))
  (cond ((eq (car tree) 'node) (cond ((member-equal-+- (cadr tree) clause) (list 'node
            (cadr tree)
            (replace-clause1 clause
              (remove-one-+- (cadr tree) undisc-lits)
              new-clause
              (caddr tree))
            (cadddr tree)))
        (t (list 'node
            (cadr tree)
            (caddr tree)
            (replace-clause1 clause
              undisc-lits
              new-clause
              (cadddr tree))))))
    ((member-equal clause (cdr tree)) (cons (car tree) (substitute1 new-clause clause (cdr tree))))
    (t tree)))

(defun replace-clause
  (clause new-clause tree)
  (declare (xargs :guard (and (pseudo-term-listp clause) (disc-tree tree))))
  (replace-clause1 clause clause new-clause tree))

(defun extra-info-lits
  (cl acc)
  (cond ((endp cl) acc)
    ((extra-info-lit-p (car cl)) (extra-info-lits (cdr cl) (cons (car cl) acc)))
    (t (extra-info-lits (cdr cl) acc))))

(defun merge-extra-info-lits
  (cl cl0 tree)
  (let ((lits (extra-info-lits cl nil)))
    (cond (lits (replace-clause cl0 (rev-union-equal lits cl0) tree))
      (t tree))))

(defun subsumption-replacement-loop
  (todo done-tree again-flg)
  (declare (xargs :guard (and (pseudo-term-list-listp todo) (disc-tree done-tree))))
  (cond ((null todo) (cond (again-flg (cond ((time-limit5-reached-p "Out of time in subsumption (subsumption-replacement-loop).") nil)
            (t (subsumption-replacement-loop (merge-sort-length (sweep-clauses done-tree))
                nil
                nil))))
        (t (sweep-clauses done-tree))))
    (t (mv-let (x cl0)
        (find-subsumer-replacement (car todo)
          (find-clauses (car todo) done-tree))
        (cond ((null x) (subsumption-replacement-loop (cdr todo)
              (store-clause (car todo) done-tree)
              again-flg))
          ((eq x 'subsumed) (subsumption-replacement-loop (cdr todo)
              (merge-extra-info-lits (car todo) cl0 done-tree)
              again-flg))
          (t (subsumption-replacement-loop (cdr todo)
              (store-clause (remove-one-complement (car x) (car todo))
                done-tree)
              t)))))))

(defun clausify
  (term assumptions lambda-exp sr-limit)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((clauses (pstk (strip-branches term assumptions lambda-exp))))
    (cond ((or (null sr-limit) (<= (length clauses) sr-limit)) (pstk (subsumption-replacement-loop (merge-sort-length clauses)
            nil
            nil)))
      (t clauses))))

(defun find-rewriting-equivalence
  (lhs type-alist geneqv wrld ttree)
  (cond ((null type-alist) (mv nil nil ttree))
    (t (let ((entry (car type-alist)))
        (cond ((not (variablep (car entry))) (let ((rw-equivp (cond ((and (eq (ffn-symb (car entry)) 'hide)
                      (not (variablep (fargn (car entry) 1)))
                      (eq (ffn-symb (fargn (car entry) 1)) 'rewrite-equiv)) (car entry)))))
              (cond ((if rw-equivp
                   (ts-disjointp (cadr entry) *ts-nil*)
                   (ts= (cadr entry) *ts-t*)) (let* ((equiv-term (cond (rw-equivp (fargn (fargn (car entry) 1) 1))
                         (t (car entry)))) (rune (and (not (flambdap (ffn-symb equiv-term)))
                          (geneqv-refinementp (ffn-symb equiv-term) geneqv wrld))))
                    (cond ((and rune (equal (fargn equiv-term 1) lhs)) (mv rw-equivp
                          equiv-term
                          (cons-tag-trees (cddr entry) (push-lemma rune ttree))))
                      (t (find-rewriting-equivalence lhs
                          (cdr type-alist)
                          geneqv
                          wrld
                          ttree)))))
                (t (find-rewriting-equivalence lhs
                    (cdr type-alist)
                    geneqv
                    wrld
                    ttree)))))
          (t (find-rewriting-equivalence lhs
              (cdr type-alist)
              geneqv
              wrld
              ttree)))))))

(defun obj-table
  (term ts ts-ttree obj geneqv wrld ttree)
  (declare (ignore obj))
  (cond ((ts= ts *ts-t*) (mv *t* (cons-tag-trees ts-ttree ttree)))
    ((ts= ts *ts-nil*) (mv *nil* (cons-tag-trees ts-ttree ttree)))
    ((ts= ts *ts-zero*) (mv *0* (cons-tag-trees ts-ttree ttree)))
    (t (let ((rune (geneqv-refinementp 'iff geneqv wrld)))
        (cond (rune (cond ((ts-subsetp *ts-nil* ts) (mv term ttree))
              (t (mv *t* (push-lemma rune (cons-tag-trees ts-ttree ttree))))))
          (t (mv term ttree)))))))

(defun rewrite-solidify-rec
  (bound term type-alist obj geneqv ens wrld ttree pot-lst pt)
  (declare (type (unsigned-byte 60) bound))
  (cond ((quotep term) (cond ((equal term *nil*) (mv *nil* ttree))
        (t (let ((rune (geneqv-refinementp 'iff geneqv wrld)))
            (cond (rune (mv *t* (push-lemma rune ttree)))
              (t (mv term ttree)))))))
    ((ffn-symb-p term 'if) (mv term ttree))
    ((and (ffn-symb-p term 'hide)
       (let ((e (fargn term 1)))
         (case-match e
           (('rewrite-equiv (equiv x x)) (prog2$ x (equivalence-relationp equiv wrld)))
           (& nil)))) (mv *t*
        (push-lemma (fn-rune-nume 'hide nil nil wrld)
          (push-lemma (fn-rune-nume 'rewrite-equiv nil nil wrld)
            ttree))))
    (t (mv-let (rw-equivp eterm ttree)
        (find-rewriting-equivalence term
          type-alist
          geneqv
          wrld
          ttree)
        (cond (eterm (let ((new-bound (cond ((not rw-equivp) bound)
                   ((zpf bound) (prog2$ (er hard
                         'rewrite-solidify
                         "You appear to have hit the unusual case ~
                                    of a loop in the replacement of terms by ~
                                    equivalent terms using rewrite-equiv.  ~
                                    The term ~x0 is involved in the loop."
                         rw-equivp)
                       0))
                   (t (1-f bound)))))
              (declare (type (unsigned-byte 60) new-bound))
              (rewrite-solidify-rec new-bound
                (fargn eterm 2)
                type-alist
                obj
                geneqv
                ens
                wrld
                ttree
                pot-lst
                pt)))
          (t (mv-let (ts ts-ttree)
              (cond ((not (eq obj '?)) (type-set term nil t type-alist ens wrld nil pot-lst pt))
                (t (assoc-type-alist term type-alist wrld)))
              (if (null ts)
                (mv term ttree)
                (obj-table term ts ts-ttree obj geneqv wrld ttree)))))))))

(defun rewrite-solidify
  (term type-alist obj geneqv ens wrld ttree pot-lst pt)
  (rewrite-solidify-rec *rewrite-equiv-solidify-iteration-bound*
    term
    type-alist
    obj
    geneqv
    ens
    wrld
    ttree
    pot-lst
    pt))

(defun rewrite-if11
  (term type-alist geneqv wrld ttree)
  (mv-let (ts ts-ttree)
    (look-in-type-alist term type-alist wrld)
    (cond ((ts= ts *ts-nil*) (mv *nil* (cons-tag-trees ts-ttree ttree)))
      ((and (equal geneqv *geneqv-iff*) (ts-disjointp ts *ts-nil*)) (mv *t* (cons-tag-trees ts-ttree ttree)))
      (t (mv term ttree)))))

(defun rewrite-if1
  (test left
    right
    swapped-p
    type-alist
    geneqv
    ens
    ok-to-force
    wrld
    ttree)
  (flet ((if-call (test left right swapped-p)
       (cond ((and swapped-p (rewrite-if-avoid-swap)) (mcons-term* 'if (dumb-negate-lit test) right left))
         (t (mcons-term* 'if test left right)))))
    (cond ((equal left right) (mv left ttree))
      ((equal right *nil*) (cond ((equal test left) (mv test ttree))
          ((equal left *t*) (mv-let (ts ts-ttree)
              (type-set test
                ok-to-force
                nil
                type-alist
                ens
                wrld
                ttree
                nil
                nil)
              (cond ((ts-subsetp ts *ts-boolean*) (mv test ts-ttree))
                (t (rewrite-if11 (if-call test left right swapped-p)
                    type-alist
                    geneqv
                    wrld
                    ttree)))))
          (t (rewrite-if11 (if-call test left right swapped-p)
              type-alist
              geneqv
              wrld
              ttree))))
      ((and swapped-p
         (equal left *nil*)
         (equal right *t*)
         (rewrite-if-avoid-swap)) (mv (fcons-term* 'not test) ttree))
      (t (rewrite-if11 (if-call test left right swapped-p)
          type-alist
          geneqv
          wrld
          ttree)))))

(defun member-equal-mod-alist
  (term1 alist1 term2-lst)
  (cond ((endp term2-lst) nil)
    ((equal-mod-alist term1 alist1 (car term2-lst)) t)
    (t (member-equal-mod-alist term1 alist1 (cdr term2-lst)))))

(defun not-to-be-rewrittenp1
  (fn lst)
  (cond ((null lst) nil)
    ((equal fn (ffn-symb (car lst))) t)
    (t (not-to-be-rewrittenp1 fn (cdr lst)))))

(defun not-to-be-rewrittenp
  (term alist terms-to-be-ignored-by-rewrite)
  (cond ((not-to-be-rewrittenp1 (ffn-symb term)
       terms-to-be-ignored-by-rewrite) (member-equal-mod-alist term
        alist
        terms-to-be-ignored-by-rewrite))
    (t nil)))

(defun rewrite-recognizer
  (recog-tuple arg
    type-alist
    ens
    force-flg
    wrld
    ttree
    pot-lst
    pt)
  (mv-let (ts ttree+)
    (type-set arg
      force-flg
      nil
      type-alist
      ens
      wrld
      ttree
      pot-lst
      pt)
    (cond ((ts-intersectp ts
         (access recognizer-tuple recog-tuple :true-ts)) (cond ((ts-intersectp ts
             (access recognizer-tuple recog-tuple :false-ts)) (mv (mcons-term* (access recognizer-tuple recog-tuple :fn) arg)
              ttree))
          (t (mv *t*
              (push-lemma (access recognizer-tuple recog-tuple :rune)
                ttree+)))))
      (t (mv *nil*
          (push-lemma (access recognizer-tuple recog-tuple :rune)
            ttree+))))))

(defun remove-invisible-fncalls
  (term invisible-fns)
  (cond ((or (variablep term)
       (fquotep term)
       (flambda-applicationp term)) term)
    ((member-eq (ffn-symb term) invisible-fns) (remove-invisible-fncalls (fargn term 1) invisible-fns))
    (t term)))

(defun term-order+
  (x1 x2 invisible-fns)
  (let ((x1-guts (remove-invisible-fncalls x1 invisible-fns)) (x2-guts (remove-invisible-fncalls x2 invisible-fns)))
    (cond ((equal x1-guts x2-guts) (term-order x1 x2))
      (t (term-order x1-guts x2-guts)))))

(defun invisible-fns
  (fns alist acc)
  (declare (xargs :guard (and (symbol-listp fns) (or (true-listp acc) (eq acc t)))))
  (cond ((null fns) (if (eq acc t)
        nil
        acc))
    ((eq acc t) (invisible-fns (cdr fns)
        alist
        (cdr (assoc-eq (car fns) alist))))
    ((null acc) nil)
    (t (invisible-fns (cdr fns)
        alist
        (intersection-eq (cdr (assoc-eq (car fns) alist)) acc)))))

(defun loop-stopperp-rec
  (loop-stopper sbst wrld)
  (cond ((null loop-stopper) nil)
    (t (let ((pre (cdr (assoc-eq (car (car loop-stopper)) sbst))) (post (cdr (assoc-eq (cadr (car loop-stopper)) sbst))))
        (cond ((equal pre post) (loop-stopperp-rec (cdr loop-stopper) sbst wrld))
          (t (term-order+ post
              pre
              (invisible-fns (cddr (car loop-stopper))
                (invisible-fns-table wrld)
                t))))))))

(defun loop-stopperp
  (loop-stopper sbst wrld)
  (or (null loop-stopper)
    (loop-stopperp-rec loop-stopper sbst wrld)))

(defun relevant-ground-lemmas
  (hyp wrld)
  (mv-let (not-flg hyp)
    (strip-not hyp)
    (declare (ignore not-flg))
    (cond ((variablep hyp) nil)
      ((fquotep hyp) nil)
      ((flambda-applicationp hyp) nil)
      (t (getpropc (ffn-symb hyp) 'lemmas nil wrld)))))

(defun search-ground-units1
  (hyp unify-subst lemmas type-alist ens force-flg wrld ttree)
  (cond ((null lemmas) (mv nil unify-subst ttree nil))
    ((and (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
       (not (eq (access rewrite-rule (car lemmas) :subclass) 'meta))
       (null (access rewrite-rule (car lemmas) :hyps))
       (not (access rewrite-rule (car lemmas) :var-info))
       (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
         *geneqv-iff*
         wrld)) (mv-let (knownp nilp nilp-ttree)
        (known-whether-nil (access rewrite-rule (car lemmas) :rhs)
          type-alist
          ens
          force-flg
          nil
          wrld
          ttree)
        (cond ((and knownp (not nilp)) (mv-let (ans unify-subst)
              (one-way-unify1 hyp
                (access rewrite-rule (car lemmas) :lhs)
                unify-subst)
              (cond (ans (let ((rune (access rewrite-rule (car lemmas) :rune)))
                    (with-accumulated-persistence rune
                      (flg final-unify-subst final-ttree final-lemmas)
                      t
                      (mv t
                        unify-subst
                        (push-lemma (geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
                            *geneqv-iff*
                            wrld)
                          (push-lemma rune nilp-ttree))
                        (cdr lemmas)))))
                (t (search-ground-units1 hyp
                    unify-subst
                    (cdr lemmas)
                    type-alist
                    ens
                    force-flg
                    wrld
                    ttree)))))
          (t (search-ground-units1 hyp
              unify-subst
              (cdr lemmas)
              type-alist
              ens
              force-flg
              wrld
              ttree)))))
    (t (search-ground-units1 hyp
        unify-subst
        (cdr lemmas)
        type-alist
        ens
        force-flg
        wrld
        ttree))))

(defun search-ground-units
  (hyp unify-subst type-alist ens force-flg wrld ttree)
  (let ((lemmas (relevant-ground-lemmas hyp wrld)))
    (mv-let (winp unify-subst ttree rest-lemmas)
      (search-ground-units1 hyp
        unify-subst
        lemmas
        type-alist
        ens
        force-flg
        wrld
        ttree)
      (declare (ignore rest-lemmas))
      (mv winp unify-subst ttree))))

(defun if-tautologyp
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (posp (if-interp (splice-instrs (if-compile term t nil nil))
      nil
      nil
      nil
      nil
      100000)))

(defun tautologyp
  (term wrld)
  (cond ((and (ffn-symb-p term 'implies)
       (equal (fargn term 1) (fargn term 2))) t)
    (t (if-tautologyp (expand-some-non-rec-fns '(iff implies
            eq
            atom
            eql
            =
            /=
            null
            zerop
            synp
            return-last
            plusp
            minusp
            listp
            mv-list
            cons-with-hint
            wormhole-eval
            force
            case-split
            double-rewrite)
          term
          wrld)))))

(defun being-openedp-rec
  (fn fnstack)
  (cond ((null fnstack) nil)
    ((consp (car fnstack)) (or (eq fn (caar fnstack))
        (being-openedp-rec fn (cdr fnstack))))
    (t (or (eq fn (car fnstack))
        (being-openedp-rec fn (cdr fnstack))))))

(defun recursive-fn-on-fnstackp
  (fnstack)
  (cond ((null fnstack) nil)
    ((and (consp (car fnstack)) (not (eq (caar fnstack) :term))) t)
    (t (recursive-fn-on-fnstackp (cdr fnstack)))))

(defun fnstack-term-member
  (term fnstack)
  (cond ((null fnstack) nil)
    ((and (consp (car fnstack))
       (eq (caar fnstack) :term)
       (equal (cdar fnstack) term)) t)
    (t (fnstack-term-member term (cdr fnstack)))))

(defun var-counts
  (lhs-args rhs)
  (declare (xargs :guard (and (true-listp lhs-args) (pseudo-termp rhs))))
  (cond ((endp lhs-args) nil)
    (t (cons (var-counts1 (car lhs-args) rhs 0)
        (var-counts (cdr lhs-args) rhs)))))

(defun too-many-ifs0
  (args counts diff ctx)
  (declare (type (signed-byte 61) diff)
    (xargs :guard (and (pseudo-term-listp args)
        (integer-listp counts)
        (equal (len args) (len counts)))))
  (cond ((endp args) (> diff 0))
    ((eql (car counts) 1) (too-many-ifs0 (cdr args) (cdr counts) diff ctx))
    (t (let ((count1 (the-fixnum! (count-ifs (car args)) ctx)))
        (declare (type (unsigned-byte 60) count1))
        (too-many-ifs0 (cdr args)
          (cdr counts)
          (the-fixnum! (+ (the-fixnum! (* count1 (1- (car counts))) ctx) diff)
            ctx)
          ctx)))))

(defun too-many-ifs-pre-rewrite-builtin
  (args counts)
  (declare (xargs :guard (and (pseudo-term-listp args)
        (integer-listp counts)
        (equal (len args) (len counts)))))
  (too-many-ifs0 args counts 0 'too-many-ifs-pre-rewrite))

(defun too-many-ifs1
  (args val lhs rhs ctx)
  (declare (type (signed-byte 61) lhs rhs)
    (xargs :guard (and (pseudo-term-listp args)
        (pseudo-termp val)
        (<= 0 lhs)
        (<= lhs rhs)
        (<= (count-ifs-lst args) rhs))))
  (cond ((endp args) nil)
    (t (let ((x (the-fixnum! (count-ifs (car args)) ctx)))
        (declare (type (signed-byte 61) x))
        (cond ((eql x 0) (too-many-ifs1 (cdr args) val lhs rhs ctx))
          (t (let ((lhs (occur-cnt-bounded (car args)
                   val
                   lhs
                   x
                   (the-fixnum (- rhs x)))))
              (declare (type (signed-byte 61) lhs))
              (if (eql lhs -1)
                -1
                (too-many-ifs1 (cdr args) val lhs rhs ctx)))))))))

(defun too-many-ifs-post-rewrite-builtin
  (args val)
  (declare (xargs :guard (and (pseudo-term-listp args) (pseudo-termp val))))
  (let* ((ctx 'too-many-ifs-post-rewrite-builtin) (rhs (the-fixnum! (count-ifs-lst args) ctx)))
    (cond ((int= rhs 0) nil)
      (t (too-many-ifs1 args val 0 rhs ctx)))))

(defun all-args-occur-in-top-clausep
  (args top-clause)
  (cond ((null args) t)
    (t (and (dumb-occur-lst (car args) top-clause)
        (all-args-occur-in-top-clausep (cdr args) top-clause)))))

(defun controller-complexity1
  (flg args controller-pocket)
  (cond ((null args) 0)
    ((eq (car controller-pocket) flg) (+ (max-form-count (car args))
        (controller-complexity1 flg
          (cdr args)
          (cdr controller-pocket))))
    (t (controller-complexity1 flg
        (cdr args)
        (cdr controller-pocket)))))

(defun controller-complexity
  (flg term controller-alist)
  (controller-complexity1 flg
    (fargs term)
    (cdr (assoc-eq (ffn-symb term) controller-alist))))

(defun controller-pocket-simplerp
  (call result controller-alist)
  (< (controller-complexity t result controller-alist)
    (controller-complexity t call controller-alist)))

(defun constant-controller-pocketp1
  (args controller-pocket)
  (cond ((null args) t)
    ((car controller-pocket) (and (quotep (car args))
        (constant-controller-pocketp1 (cdr args)
          (cdr controller-pocket))))
    (t (constant-controller-pocketp1 (cdr args)
        (cdr controller-pocket)))))

(defun constant-controller-pocketp
  (term controller-alist)
  (constant-controller-pocketp1 (fargs term)
    (cdr (assoc-eq (ffn-symb term) controller-alist))))

(defun some-controller-pocket-constant-and-non-controller-simplerp
  (call result controller-alist)
  (and (constant-controller-pocketp result controller-alist)
    (< (controller-complexity nil result controller-alist)
      (controller-complexity nil call controller-alist))))

(defun ok-to-force
  (rcnst)
  (let ((force-info (access rewrite-constant rcnst :force-info)))
    (cond ((eq force-info t) (and (enabled-numep *force-xnume*
            (access rewrite-constant rcnst :current-enabled-structure))
          t))
      ((eq force-info 'weak) nil)
      (t (er hard
          'ok-to-force
          "OK-TO-FORCE called on apparently uninitialized rewrite constant, ~
           ~x0."
          rcnst)))))

(defun plist-to-alist
  (lst)
  (cond ((null lst) nil)
    (t (cons (cons (car lst) (cadr lst))
        (plist-to-alist (cddr lst))))))

(defun add-rewrite-args
  (extra-formals keyword-extra-formals alist)
  (cond ((null extra-formals) nil)
    (t (cons (let ((pair (assoc-eq (car keyword-extra-formals) alist)))
          (cond (pair (cdr pair)) (t (car extra-formals))))
        (add-rewrite-args (cdr extra-formals)
          (cdr keyword-extra-formals)
          alist)))))

(defun step-limit-start
  (state)
  (let ((rec (f-get-global 'step-limit-record state)))
    (cond (rec (access step-limit-record rec :start))
      (t (step-limit-from-table (w state))))))

(defun step-limit-strictp
  (state)
  (let ((rec (f-get-global 'step-limit-record state)))
    (cond (rec (access step-limit-record rec :strictp)) (t nil))))

(defun initial-step-limit
  (wrld state)
  (declare (xargs :guard (and (plist-worldp wrld)
        (alistp (table-alist 'acl2-defaults-table wrld))
        (let ((val (cdr (assoc-eq :step-limit (table-alist 'acl2-defaults-table wrld)))))
          (or (null val)
            (and (natp val) (<= val *default-step-limit*))))
        (state-p state)
        (boundp-global 'step-limit-record state)
        (boundp-global 'last-step-limit state))))
  (let ((rec (f-get-global 'step-limit-record state)))
    (cond (rec (or (access step-limit-record rec :sub-limit)
          (f-get-global 'last-step-limit state)))
      (t (step-limit-from-table wrld)))))

(defun step-limit-error1
  (ctx str start where state)
  (declare (ignorable state))
  (the (signed-byte 61)
    (prog2$ (er hard? ctx str start where) -1)))

(defun tilde-@-bkptr-phrase
  (calling-sys-fn called-sys-fn bkptr)
  (case called-sys-fn
    (rewrite (cond ((integerp bkptr) (cond ((member-eq calling-sys-fn
               '(rewrite-with-lemma rewrite-quoted-constant-with-lemma
                 add-linear-lemma)) (msg " the atom of the ~n0 hypothesis" (list bkptr)))
            ((eq calling-sys-fn 'simplify-clause) (msg " the atom of the ~n0 literal" (list bkptr)))
            (t (msg " the ~n0 argument" (list bkptr)))))
        ((consp bkptr) (msg " the rhs of the ~n0 hypothesis" (list (cdr bkptr))))
        ((symbolp bkptr) (case bkptr
            (body " the body")
            (lambda-body " the lambda body")
            (lambda-object-body " the body of the lambda object")
            (rewritten-body " the rewritten body")
            (expansion " the expansion")
            (equal-consp-hack-car " the equality of the cars")
            (equal-consp-hack-cdr " the equality of the cdrs")
            (rhs " the rhs of the conclusion")
            (meta " the result of the metafunction")
            (nth-update " the result of the nth/update rewriter")
            (multiply-alists2 " the product of two polys")
            (forced-assumption " a forced assumption")
            (proof-builder " proof-builder top level")
            (otherwise (er hard
                'tilde-@-bkptr-phrase
                "When ~x0 calls ~x1 we get an unrecognized ~
                                      bkptr, ~x2."
                calling-sys-fn
                called-sys-fn
                bkptr))))
        (t (er hard
            'tilde-@-bkptr-phrase
            "When ~x0 calls ~x1 we get an unrecognized bkptr, ~x2."
            calling-sys-fn
            called-sys-fn
            bkptr))))
    ((rewrite-with-lemma setup-simplify-clause-pot-lst
       simplify-clause
       add-terms-and-lemmas
       add-linear-lemma
       non-linear-arithmetic
       synp) "")
    (t (er hard
        'tilde-@-bkptr-phrase
        "When ~x0 calls ~x1 we get an unrecognized bkptr, ~x2."
        calling-sys-fn
        called-sys-fn
        bkptr))))

(defun show-geneqv
  (x with-runes-p)
  (cond ((endp x) nil)
    (t (cons (cond ((eq with-runes-p t) (list (access congruence-rule (car x) :equiv)
              (access congruence-rule (car x) :rune)))
          ((eq with-runes-p 'non-prims) (cond ((or (eq (car (access congruence-rule (car x) :rune))
                   :fake-rune-for-anonymous-enabled-rule)
                 (equal (access congruence-rule (car x) :rune)
                   '(:equivalence iff-is-an-equivalence))) (access congruence-rule (car x) :equiv))
              ((eq (car (access congruence-rule (car x) :rune))
                 :congruence) (list (access congruence-rule (car x) :equiv)
                  (cadr (access congruence-rule (car x) :rune))))
              (t (list (access congruence-rule (car x) :equiv)
                  (access congruence-rule (car x) :rune)))))
          (t (access congruence-rule (car x) :equiv)))
        (show-geneqv (cdr x) with-runes-p)))))

(defun cw-gframe
  (i calling-sys-fn frame evisc-tuple)
  (case (access gframe frame :sys-fn)
    (simplify-clause (cw "~x0. Simplifying the clause~%     ~Y12"
        i
        (access gframe frame :args)
        evisc-tuple))
    (setup-simplify-clause-pot-lst (cw "~x0. Setting up the linear pot list for the clause~%     ~Y12"
        i
        (access gframe frame :args)
        evisc-tuple))
    (rewrite (let ((term (car (access gframe frame :args))) (alist (cadr (access gframe frame :args)))
          (obj (caddr (access gframe frame :args)))
          (geneqv (cdddr (access gframe frame :args))))
        (cw "~x0. Rewriting (to ~@6)~@1,~%     ~Y23,~#4~[~/   under the ~
                substitution~%~*5~]~#7~[~/~|   Geneqv: ~y8~]"
          i
          (tilde-@-bkptr-phrase calling-sys-fn
            'rewrite
            (access gframe frame :bkptr))
          term
          evisc-tuple
          (if alist
            1
            0)
          (tilde-*-alist-phrase alist evisc-tuple 5)
          (cond ((eq obj nil) "falsify")
            ((eq obj t) "establish")
            (t "simplify"))
          (if geneqv
            1
            0)
          (show-geneqv geneqv 'non-prims))))
    ((rewrite-with-lemma rewrite-quoted-constant-with-lemma) (let ((term (car (access gframe frame :args))) (lemma (cadr (access gframe frame :args)))
          (geneqv (cddr (access gframe frame :args))))
        (cw "~x0. Attempting to apply ~F1 to~%     ~Y23~|~#4~[~/   Preserving: ~x5~]~|~#6~[~/   Geneqv: ~y7~]"
          i
          (get-rule-field lemma :rune)
          term
          evisc-tuple
          (if (eq (access rewrite-rule lemma :equiv) 'equal)
            0
            1)
          (access rewrite-rule lemma :equiv)
          (if geneqv
            1
            0)
          (show-geneqv geneqv 'non-prims))))
    (add-linear-lemma (let ((term (car (access gframe frame :args))) (lemma (cdr (access gframe frame :args))))
        (cw "~x0. Attempting to apply ~F1 to~%     ~Y23"
          i
          (get-rule-field lemma :rune)
          term
          evisc-tuple)))
    (add-terms-and-lemmas (cw "~x0. Attempting to apply linear arithmetic to ~@1~%     ~Y23"
        i
        (let ((obj (cdr (access gframe frame :args))))
          (cond ((eq obj nil) (msg "falsify the term list"))
            ((eq obj t) "establish the term list")
            (t "the clause")))
        (car (access gframe frame :args))
        evisc-tuple))
    (non-linear-arithmetic (cw "~x0. Attempting to apply non-linear arithmetic to the list of ~
              ~x1 var~#2~[~/s~]:~%     ~Y23"
        i
        (length (access gframe frame :args))
        (access gframe frame :args)
        evisc-tuple))
    (synp (let ((synp-fn (access gframe frame :args)))
        (cw "~x0. Entering ~x1 for hypothesis ~x2~%"
          i
          synp-fn
          (access gframe frame :bkptr))))
    (otherwise (er hard
        'cw-gframe
        "Unrecognized sys-fn, ~x0"
        (access gframe frame :sys-fn)))))

(defun cw-gstack1
  (i calling-sys-fn lst evisc-tuple)
  (cond ((null lst) nil)
    (t (prog2$ (cw-gframe i calling-sys-fn (car lst) evisc-tuple)
        (cw-gstack1 (1+ i)
          (access gframe (car lst) :sys-fn)
          (cdr lst)
          evisc-tuple)))))

(defun cw-gstack-fn
  (evisc-tuple frames)
  (let ((gstack nil) (ctx 'cw-gstack))
    (cond ((null gstack) (cw "There is no gstack to print.  If you have enabled stack monitoring ~
           with ``:BRR t'' this is likely due to the loop you wish to ~
           investigate occurring in so-called preprocessing, where monitoring ~
           is not done, rather than in the rewriter proper.  You may obtain ~
           better results by replaying the problematic event with a hint ~
           of:~%(("Goal" :DO-NOT '(preprocess)).~%See :DOC hints, in ~
           particular the discussion of :DO-NOT.~%"))
      ((and evisc-tuple (not (standard-evisc-tuplep evisc-tuple))) (er hard
          ctx
          "Illegal :evisc-tuple argument to ~x0: ~x1.  See :DOC cw-gstack."
          'cw-gstack
          evisc-tuple))
      ((not (or (null frames)
           (and (integerp frames) (< 0 frames))
           (and (true-listp frames)
             (eql (length frames) 2)
             (natp (car frames))
             (natp (cadr frames))
             (<= (car frames) (cadr frames))))) (er hard
          ctx
          "Illegal :frames argument to ~x0: ~x1.  See :DOC cw-gstack."
          'cw-gstack
          frames))
      (t (let ((start (cond ((or (null frames) (integerp frames)) 1)
               ((<= (car frames) (length gstack)) (car frames))
               (t (length gstack)))))
          (cw-gstack1 start
            nil
            (cond ((null frames) (reverse gstack))
              (t (let* ((rev-gstack (reverse gstack)) (len (length gstack))
                    (n (min (if (integerp frames)
                          frames
                          (cadr frames))
                        len)))
                  (nthcdr (1- start) (take n rev-gstack)))))
            evisc-tuple))))))

(defun make-initial-brr-status
  (monitored-runes)
  (make brr-status
    :entry-code :enter :brr-monitored-runes monitored-runes
    :brr-gstack nil
    :brr-local-alist nil
    :brr-previous-status nil))

(defun dive-to-deepest-brr-status
  (whs)
  (let ((prev-whs (access brr-status whs :brr-previous-status)))
    (if (null prev-whs)
      whs
      (dive-to-deepest-brr-status prev-whs))))

(defun top-level-brr-status
  (whs)
  (make-initial-brr-status (access brr-status
      (dive-to-deepest-brr-status whs)
      :brr-monitored-runes)))

(defun brr-depth1
  (whs)
  (let ((prev-whs (access brr-status whs :brr-previous-status)))
    (cond ((null prev-whs) 0) (t (+ 1 (brr-depth1 prev-whs))))))

(defun brr-depth
  (state)
  (brr-depth1 (f-get-global 'wormhole-status state)))

(defun get-brr-local
  (var state)
  (let ((whs (f-get-global 'wormhole-status state)))
    (cdr (assoc-eq var (access brr-status whs :brr-local-alist)))))

(defun put-brr-local
  (var val state)
  (if (eq (f-get-global 'wormhole-name state) 'brr)
    (let* ((whs (f-get-global 'wormhole-status state)) (alist (access brr-status whs :brr-local-alist))
        (new-whs (change brr-status
            whs
            :brr-local-alist (put-assoc-eq var val alist))))
      (set-persistent-whs-and-ephemeral-whs 'brr new-whs state))
    (prog2$ (illegal 'put-brr-local
        "It is illegal to call put-brr-local unless you are under ~
                 break-rewrite and you are not.  The arguments to ~
                 put-brr-local were ~x0 and ~x1"
        (list (cons #\0 var) (cons #\1 val)))
      state)))

(defun put-brr-locals
  (alist state)
  (if (eq (f-get-global 'wormhole-name state) 'brr)
    (let* ((whs (f-get-global 'wormhole-status state)) (alist1 (access brr-status whs :brr-local-alist))
        (new-whs (change brr-status
            whs
            :brr-local-alist (put-assoc-eq-alist alist1 alist))))
      (set-persistent-whs-and-ephemeral-whs 'brr new-whs state))
    (prog2$ (illegal 'put-brr-locals
        "It is illegal to call put-brr-locals unless you are under ~
                 break-rewrite and you are not.  The alist argument to ~
                 put-brr-locals was ~x0."
        (list (cons #\0 alist)))
      state)))

(defun push-brr-status
  (state)
  (let* ((input (f-get-global 'wormhole-input state)) (gstack (cdr (assoc-eq 'brr-gstack input)))
      (alist (cdr (assoc-eq 'brr-local-alist input)))
      (whs (f-get-global 'wormhole-status state))
      (new-whs (change brr-status
          whs
          :brr-gstack gstack
          :brr-local-alist alist
          :brr-previous-status whs)))
    (set-persistent-whs-and-ephemeral-whs 'brr new-whs state)))

(defun pop-brr-status
  (state)
  (let* ((whs (f-get-global 'wormhole-status state)) (prev-whs (access brr-status whs :brr-previous-status)))
    (if (null prev-whs)
      state
      (set-persistent-whs-and-ephemeral-whs 'brr prev-whs state))))

(defun decode-type-alist
  (type-alist)
  (cond ((null type-alist) nil)
    (t (cons (cons (caar type-alist)
          (decode-type-set (cadar type-alist)))
        (decode-type-alist (cdr type-alist))))))

(defun translate-break-condition
  (xterm ctx state)
  (er-let* ((term (translate xterm '(nil) nil t ctx (w state) state)))
    (let* ((used-vars (all-vars term)) (bad-vars (set-difference-eq used-vars '(state))))
      (cond (bad-vars (er soft
            ctx
            "The only variable allowed in a break condition ~
                    is STATE.  Your form, ~x0, contains the ~
                    variable~#1~[~/s~] ~&2."
            xterm
            (if (cdr bad-vars)
              1
              0)
            (reverse bad-vars)))
        (t (value term))))))

(defun eval-break-condition
  (rune term ctx state)
  (cond ((equal term *t*) (value t))
    ((not (termp term (w state))) (er soft
        ctx
        "The monitored rune ~x0 has a non-trivial break :condition, ~X12, ~
         which is no longer a term.  This is presumably because an undo ~
         erased some critical definition after the monitor was installed.  We ~
         are aborting this proof attempt and suggest you inspect ~
         :monitored-runes."
        rune
        term
        nil))
    (t (mv-let (erp okp latches)
        (ev term
          (list (cons 'state (coerce-state-to-object state)))
          state
          nil
          nil
          t)
        (declare (ignore latches))
        (cond (erp (pprogn (error-fms nil ctx nil (car okp) (cdr okp) state)
              (er soft
                ctx
                "The break condition installed on ~x0 could not be ~
                    evaluated.  We are aborting this proof attempt."
                rune)))
          (t (value okp)))))))

(defun free-vars-display-limit
  (state)
  (if (f-boundp-global 'free-vars-display-limit state)
    (let ((val (f-get-global 'free-vars-display-limit state)))
      (if (or (natp val) (null val))
        val
        *default-free-vars-display-limit*))
    *default-free-vars-display-limit*))

(defun ancestor-backchain-rune
  (ancestor)
  (and (access ancestor ancestor :bkptr)
    (let ((tokens (access ancestor ancestor :tokens)))
      (assert$ (and tokens (null (cdr tokens))) (car tokens)))))

(defun scan-to-defpkg
  (name wrld)
  (cond ((null wrld) nil)
    ((and (eq (caar wrld) 'event-landmark)
       (eq (cadar wrld) 'global-value)
       (eq (access-event-tuple-type (cddar wrld)) 'defpkg)
       (equal name (access-event-tuple-namex (cddar wrld)))) wrld)
    (t (scan-to-defpkg name (cdr wrld)))))

(defun multiple-assoc-terminal-substringp1
  (x i alist)
  (cond ((null alist) nil)
    ((terminal-substringp x
       (caar alist)
       i
       (1- (length (caar alist)))) (cons (car alist)
        (multiple-assoc-terminal-substringp1 x i (cdr alist))))
    (t (multiple-assoc-terminal-substringp1 x i (cdr alist)))))

(defun multiple-assoc-terminal-substringp
  (x alist)
  (multiple-assoc-terminal-substringp1 x
    (1- (length x))
    alist))

(defun possibly-add-lisp-extension
  (str)
  (let ((len (length str)))
    (cond ((and (> len 5)
         (eql (char str (- len 5)) #\.)
         (eql (char str (- len 4)) #\l)
         (eql (char str (- len 3)) #\i)
         (eql (char str (- len 2)) #\s)
         (eql (char str (- len 1)) #\p)) str)
      (t (string-append str ".lisp")))))

(defun stuff-standard-oi
  (cmds state)
  (declare (xargs :guard (true-listp cmds)))
  (cond ((null cmds) state)
    (t (pprogn (f-put-global 'ld-pre-eval-print t state)
        (f-put-global 'standard-oi
          (append cmds
            (cond ((symbolp (f-get-global 'standard-oi state)) (cons '(set-ld-pre-eval-print nil state)
                  (f-get-global 'standard-oi state)))
              (t (f-get-global 'standard-oi state))))
          state)))))

(defun defun-mode-prompt-string
  (state)
  (if (raw-mode-p state)
    "P"
    (case (default-defun-mode (w state))
      (:logic (if (gc-off state)
          (if (ld-skip-proofsp state)
            "s"
            "")
          (if (ld-skip-proofsp state)
            "!s"
            "!")))
      (otherwise (if (gc-off state)
          (if (ld-skip-proofsp state)
            "ps"
            "p")
          (if (ld-skip-proofsp state)
            "p!s"
            "p!"))))))

(defun brr-prompt
  (channel state)
  (the2s (unsigned-byte 60)
    (fmt1 "~F0 ~s1~sr ~@2>"
      (list (cons #\0 (brr-depth state))
        (cons #\1 (f-get-global 'current-package state))
        (cons #\2 (defun-mode-prompt-string state))
        (cons #\r ""))
      0
      channel
      state
      nil)))

(defun ts<
  (x y)
  (cond ((ts= x y) nil)
    ((ts= x *ts-t*) t)
    ((ts= y *ts-t*) nil)
    ((ts= x *ts-non-nil*) t)
    ((ts= y *ts-non-nil*) nil)
    ((ts= x *ts-nil*) t)
    ((ts= y *ts-nil*) nil)
    ((ts-subsetp x y) t)
    (t nil)))

(defun add-to-type-alist-segments
  (ts term segs)
  (cond ((or (endp segs) (ts< ts (caar segs))) (cons (cons ts (list term)) segs))
    ((ts= ts (caar segs)) (cons (cons ts (cons term (cdar segs))) (cdr segs)))
    (t (cons (car segs)
        (add-to-type-alist-segments ts term (cdr segs))))))

(defun merge-term-order
  (l1 l2)
  (declare (xargs :guard (and (pseudo-term-listp l1) (pseudo-term-listp l2))))
  (cond ((endp l1) l2)
    ((endp l2) l1)
    ((term-order (car l1) (car l2)) (cons (car l1) (merge-term-order (cdr l1) l2)))
    (t (cons (car l2) (merge-term-order l1 (cdr l2))))))

(defun merge-sort-term-order
  (l)
  (declare (xargs :guard (pseudo-term-listp l)))
  (cond ((endp (cdr l)) l)
    (t (merge-term-order (merge-sort-term-order (evens l))
        (merge-sort-term-order (odds l))))))

(defun sort-type-alist-segments
  (segs)
  (if (endp segs)
    nil
    (cons (cons (caar segs) (merge-sort-term-order (cdar segs)))
      (sort-type-alist-segments (cdr segs)))))

(defun type-alist-segments
  (type-alist acc)
  (if (endp type-alist)
    (sort-type-alist-segments acc)
    (type-alist-segments (cdr type-alist)
      (add-to-type-alist-segments (cadar type-alist)
        (caar type-alist)
        acc))))

(defun print-terms
  (terms iff-flg wrld evisc-tuple)
  (if (endp terms)
    terms
    (prog2$ (cw "~Y01"
        (untranslate (car terms) iff-flg wrld)
        evisc-tuple)
      (print-terms (cdr terms) iff-flg wrld evisc-tuple))))

(defun print-type-alist-segments
  (segs wrld evisc-tuple)
  (if (endp segs)
    segs
    (prog2$ (cw "-----~%Terms with type ~x0:~%"
        (decode-type-set (caar segs)))
      (prog2$ (print-terms (cdar segs)
          (member (caar segs)
            (list *ts-t* *ts-non-nil* *ts-nil* *ts-boolean*))
          wrld
          evisc-tuple)
        (print-type-alist-segments (cdr segs) wrld evisc-tuple)))))

(defun print-type-alist
  (type-alist wrld evisc-tuple)
  (print-type-alist-segments (type-alist-segments type-alist nil)
    wrld
    evisc-tuple))

(defun print-pot-lst
  (pot-lst evisc-tuple)
  (cond ((null pot-lst) (cw "~%"))
    (t (prog2$ (cw "-----~|For maximal term ~X02~|the list of polynomials is:~|~X12~|"
          (access linear-pot (car pot-lst) :var)
          (append (show-poly-lst (access linear-pot (car pot-lst) :negatives)
              nil)
            (show-poly-lst (access linear-pot (car pot-lst) :positives)
              nil))
          evisc-tuple)
        (print-pot-lst (cdr pot-lst) evisc-tuple)))))

(defun decode-logical-name
  (name wrld)
  (cond ((symbolp name) (cond ((eq name :here) (scan-to-event wrld))
        (t (let ((n (getpropc name 'absolute-event-number nil wrld)))
            (cond ((null n) nil) (t (lookup-world-index 'event n wrld)))))))
    ((and (stringp name)
       (find-non-hidden-package-entry name
         (global-val 'known-package-alist wrld))) (cond ((find-package-entry name *initial-known-package-alist*) (lookup-world-index 'event 0 wrld))
        (t (scan-to-defpkg name wrld))))
    (t nil)))

(defun access-x-rule-rune
  (x rule)
  (case x
    (recognizer-tuple (access recognizer-tuple rule :rune))
    (type-prescription (access type-prescription rule :rune))
    (congruence-rule (access congruence-rule rule :rune))
    (pequiv (access congruence-rule
        (access pequiv rule :congruence-rule)
        :rune))
    (rewrite-rule (access rewrite-rule rule :rune))
    (well-founded-relation-rule (cddr rule))
    (linear-lemma (access linear-lemma rule :rune))
    (forward-chaining-rule (access forward-chaining-rule rule :rune))
    (built-in-clause (access built-in-clause rule :rune))
    (elim-rule (access elim-rule rule :rune))
    (generalize-rule (access generalize-rule rule :rune))
    (induction-rule (access induction-rule rule :rune))
    (type-set-inverter-rule (access type-set-inverter-rule rule :rune))
    (otherwise (er hard
        'access-x-rule-rune
        "Unrecognized rule class, ~x0."
        x))))

(defun collect-x-rules-of-rune
  (x rune lst ans)
  (cond ((null lst) ans)
    ((equal rune (access-x-rule-rune x (car lst))) (collect-x-rules-of-rune x
        rune
        (cdr lst)
        (add-to-set-equal (car lst) ans)))
    (t (collect-x-rules-of-rune x rune (cdr lst) ans))))

(defun collect-congruence-rules-of-rune-in-geneqv-lst
  (geneqv-lst rune ans)
  (cond ((null geneqv-lst) ans)
    (t (collect-congruence-rules-of-rune-in-geneqv-lst (cdr geneqv-lst)
        rune
        (collect-x-rules-of-rune 'congruence-rule
          rune
          (car geneqv-lst)
          ans)))))

(defun collect-congruence-rules-of-rune
  (congruences rune ans)
  (cond ((null congruences) ans)
    (t (collect-congruence-rules-of-rune (cdr congruences)
        rune
        (collect-congruence-rules-of-rune-in-geneqv-lst (cdr (car congruences))
          rune
          ans)))))

(defun collect-pequivs-of-rune
  (alist rune ans)
  (cond ((null alist) ans)
    (t (collect-pequivs-of-rune (cdr alist)
        rune
        (collect-x-rules-of-rune 'pequiv rune (cdr (car alist)) ans)))))

(defun find-rules-of-rune2
  (rune sym key val ans)
  (let ((token (car rune)))
    (cond ((eq key 'global-value) (case sym
          (well-founded-relation-alist (if (eq token :well-founded-relation)
              (collect-x-rules-of-rune 'well-founded-relation-rule
                rune
                val
                ans)
              ans))
          (built-in-clauses (if (eq token :built-in-clause)
              (collect-x-rules-of-rune 'built-in-clause rune val ans)
              ans))
          (type-set-inverter-rules (if (eq token :type-set-inverter)
              (collect-x-rules-of-rune 'type-set-inverter-rule
                rune
                val
                ans)
              ans))
          (generalize-rules (if (eq token :generalize)
              (collect-x-rules-of-rune 'generalize-rule rune val ans)
              ans))
          (otherwise ans)))
      (t (case key
          (lemmas (if (member-eq token '(:rewrite :meta :definition))
              (collect-x-rules-of-rune 'rewrite-rule rune val ans)
              ans))
          (linear-lemmas (if (eq token :linear)
              (collect-x-rules-of-rune 'linear-lemma rune val ans)
              ans))
          (eliminate-destructors-rules (if (eq token :elim)
              (collect-x-rules-of-rune 'elim-rule rune val ans)
              ans))
          (congruences (if (member-eq token '(:congruence :equivalence))
              (collect-congruence-rules-of-rune val rune ans)
              ans))
          (pequivs (if (eq token :congruence)
              (collect-pequivs-of-rune (access pequivs-property val :deep)
                rune
                (collect-pequivs-of-rune (access pequivs-property val :shallow)
                  rune
                  ans))
              ans))
          (coarsenings ans)
          (forward-chaining-rules (if (eq token :forward-chaining)
              (collect-x-rules-of-rune 'forward-chaining-rule
                rune
                val
                ans)
              ans))
          (type-prescriptions (if (eq token :type-prescription)
              (collect-x-rules-of-rune 'type-prescription rune val ans)
              ans))
          (induction-rules (if (eq token :induction)
              (collect-x-rules-of-rune 'induction-rule rune val ans)
              ans))
          (recognizer-alist (if (eq token :compound-recognizer)
              (collect-x-rules-of-rune 'recognizer-tuple rune val ans)
              ans))
          (otherwise ans))))))

(defun find-rules-of-rune1
  (rune props ans)
  (cond ((null props) ans)
    ((eq (cddar props) *acl2-property-unbound*) (find-rules-of-rune1 rune (cdr props) ans))
    (t (find-rules-of-rune1 rune
        (cdr props)
        (find-rules-of-rune2 rune
          (caar props)
          (cadar props)
          (cddar props)
          ans)))))

(defun world-to-next-event
  (wrld)
  (cond ((null wrld) nil)
    ((and (eq (caar wrld) 'event-landmark)
       (eq (cadar wrld) 'global-value)) nil)
    (t (cons (car wrld) (world-to-next-event (cdr wrld))))))

(defun world-to-next-non-deeper-event
  (n wrld)
  (cond ((null wrld) nil)
    ((and (eq (caar wrld) 'event-landmark)
       (eq (cadar wrld) 'global-value)
       (<= (access-event-tuple-depth (cddr (car wrld))) n)) nil)
    (t (cons (car wrld)
        (world-to-next-non-deeper-event n (cdr wrld))))))

(defun actual-props
  (props seen acc)
  (cond ((null props) (prog2$ (fast-alist-free seen) (reverse acc)))
    ((member-eq (cadar props) (cdr (hons-get (caar props) seen))) (actual-props (cdr props) seen acc))
    ((eq (cddr (car props)) *acl2-property-unbound*) (actual-props (cdr props)
        (hons-acons (caar props)
          (cons (cadar props) (cdr (hons-get (caar props) seen)))
          seen)
        acc))
    (t (actual-props (cdr props)
        (hons-acons (caar props)
          (cons (cadar props) (cdr (hons-get (caar props) seen)))
          seen)
        (cons (car props) acc)))))

(defun find-rules-of-rune
  (rune wrld)
  (declare (xargs :guard (and (plist-worldp wrld) (runep rune wrld))))
  (let* ((wrld-tail (decode-logical-name (base-symbol rune) wrld)) (depth (access-event-tuple-depth (cddr (car wrld-tail)))))
    (find-rules-of-rune1 rune
      (actual-props (world-to-next-non-deeper-event depth (cdr wrld-tail))
        'find-rules-of-rune1
        nil)
      nil)))

(defun backchain-limit-enforcers
  (position ancestors wrld)
  (cond ((endp ancestors) nil)
    (t (let* ((rune (ancestor-backchain-rune (car ancestors))) (rule (and rune (car (find-rules-of-rune rune wrld)))))
        (cond (rule (let* ((linearp (eq (car rune) :linear)) (backchain-limit-lst (if linearp
                    (access linear-lemma rule :backchain-limit-lst)
                    (access rewrite-rule rule :backchain-limit-lst)))
                (bkptr (access ancestor (car ancestors) :bkptr))
                (hyp-backchain-limit (and backchain-limit-lst
                    (if (and (not linearp)
                        (eq (access rewrite-rule rule :subclass) 'meta))
                      backchain-limit-lst
                      (nth (1- bkptr) backchain-limit-lst)))))
              (cond ((and hyp-backchain-limit
                   (>= (1+ position) hyp-backchain-limit)) (cons (cons position hyp-backchain-limit)
                    (backchain-limit-enforcers (1+ position)
                      (cdr ancestors)
                      wrld)))
                (t (backchain-limit-enforcers (1+ position)
                    (cdr ancestors)
                    wrld))))))))))

(defun tilde-*-ancestors-stack-msg1
  (i ancestors wrld evisc-tuple)
  (cond ((endp ancestors) nil)
    ((ancestor-binding-hyp-p (car ancestors)) (cons (msg "~c0. Binding Hyp: ~Q12~|~
                     ~ ~ ~ ~ ~ Unify-subst:  ~Q32~%"
          (cons i 2)
          (untranslate (dumb-negate-lit (ancestor-binding-hyp/hyp (car ancestors)))
            t
            wrld)
          evisc-tuple
          (ancestor-binding-hyp/unify-subst (car ancestors)))
        (tilde-*-ancestors-stack-msg1 (+ 1 i)
          (cdr ancestors)
          wrld
          evisc-tuple)))
    (t (cons (let ((tokens (access ancestor (car ancestors) :tokens)))
          (msg "~c0. Hyp: ~Q12~|~
                         ~ ~ ~ ~ ~ Rune~#3~[:  ~x4~/s:  ~x3~]~%"
            (cons i 2)
            (untranslate (dumb-negate-lit (access ancestor (car ancestors) :lit))
              t
              wrld)
            evisc-tuple
            tokens
            (car tokens)))
        (tilde-*-ancestors-stack-msg1 (+ 1 i)
          (cdr ancestors)
          wrld
          evisc-tuple)))))

(defun tilde-*-ancestors-stack-msg
  (ancestors wrld evisc-tuple)
  (list ""
    "~@*"
    "~@*"
    "~@*"
    (tilde-*-ancestors-stack-msg1 0 ancestors wrld evisc-tuple)))

(defun semi-initialize-brr-wormhole
  (state)
  (cond ((eq (f-get-global 'wormhole-name state) 'brr) nil)
    (t (wormhole-eval 'brr
        '(lambda (whs)
          (change brr-status
            whs
            :brr-monitored-runes (access brr-status
              (top-level-brr-status whs)
              :brr-monitored-runes)
            :brr-gstack nil
            :brr-local-alist nil
            :brr-previous-status nil))
        nil))))

(defun show-ancestors-stack-msg
  (state evisc-tuple)
  (msg "Ancestors stack (most recent entry on top):~%~*0~%Use ~x1 to see ~
        actual ancestors stack.~%"
    (tilde-*-ancestors-stack-msg (get-brr-local 'ancestors state)
      (w state)
      evisc-tuple)
    '(get-brr-local 'ancestors state)))

(defun tilde-@-failure-reason-phrase1-backchain-limit
  (hyp-number ancestors state evisc-tuple)
  (msg "a backchain limit was reached while processing :HYP ~x0.  ~@1"
    hyp-number
    (let ((pairs (backchain-limit-enforcers 0 ancestors (w state))))
      (cond ((null pairs) (let ((str "  Note that the brr command, :ANCESTORS, will show you the ~
                   ancestors stack."))
            (cond ((backchain-limit (w state) :rewrite) (msg "This appears to be due to the global backchain-limit of ~
                      ~x0.~@1"
                  (backchain-limit (w state) :rewrite)
                  str))
              (t (msg "Note that the limit is 0 for that :HYP.")))))
        (t (msg "The ancestors stack is below.  The ~#0~[entry~/entries~] at ~
             index ~&0 ~#0~[shows~/each show~] a rune whose ~#0~[~/respective ~
             ~]backchain limit of ~v1 has been reached, for backchaining ~
             through its indicated hypothesis.~|~%~@2"
            (strip-cars pairs)
            (strip-cdrs pairs)
            (show-ancestors-stack-msg state evisc-tuple)))))))

(defun get-evg
  (q ctx)
  (if (quotep q)
    (cadr q)
    (er hard
      ctx
      "We expected a quotep in this context, variables, but ~x0 is not a ~
         quotep!"
      q)))

(defun get-brr-one-way-unify-info
  (lemma rcnst)
  (declare (xargs :guard (and (or (weak-rewrite-rule-p lemma) (weak-linear-lemma-p lemma))
        (weak-rewrite-constant-p rcnst))))
  (if (eq (record-type lemma) 'rewrite-rule)
    (mv (access rewrite-rule lemma :rune)
      :lhs (if (and (eq (access rewrite-rule lemma :subclass)
            'rewrite-quoted-constant)
          (let ((heuristic-info (access rewrite-rule lemma :heuristic-info)))
            (and (consp heuristic-info) (eql (car heuristic-info) 2))))
        (access rewrite-rule lemma :rhs)
        (access rewrite-rule lemma :lhs))
      (let ((restrictions-alist (access rewrite-constant rcnst :restrictions-alist)))
        (if (alistp restrictions-alist)
          (cdr (assoc-equal (access rewrite-rule lemma :rune)
              restrictions-alist))
          nil)))
    (mv (access linear-lemma lemma :rune)
      :max-term (access linear-lemma lemma :max-term)
      nil)))

(defun abstract-pat
  (k-flg pat)
  (declare (xargs :guard (and (or (eq k-flg t) (natp k-flg)) (pseudo-termp pat))))
  (mv-let (new-pat vars)
    (abstract-pat1 k-flg pat (all-vars pat))
    (declare (ignore vars))
    new-pat))

(defun alistp-listp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (eq x nil))
    (t (and (alistp (car x)) (alistp-listp (cdr x))))))

(defun one-way-unify-restrictions1
  (pat term restrictions)
  (declare (xargs :guard (and (pseudo-termp pat)
        (pseudo-termp term)
        (alistp-listp restrictions))))
  (cond ((endp restrictions) (mv nil nil))
    (t (mv-let (unify-ans unify-subst)
        (one-way-unify1 pat term (car restrictions))
        (cond (unify-ans (mv unify-ans unify-subst))
          (t (one-way-unify-restrictions1 pat term (cdr restrictions))))))))

(defun one-way-unify-restrictions
  (pat term restrictions)
  (declare (xargs :guard (and (pseudo-termp pat)
        (pseudo-termp term)
        (alistp-listp restrictions))))
  (cond ((null restrictions) (one-way-unify pat term))
    (t (one-way-unify-restrictions1 pat term restrictions))))

(defun symbol-alist-to-keyword-value-list
  (alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((endp alist) nil)
    (t (cons (car (car alist))
        (cons (cdr (car alist))
          (symbol-alist-to-keyword-value-list (cdr alist)))))))

(defun brr-criteria-alistp
  (alist)
  (declare (xargs :guard t))
  (cond ((atom alist) (equal alist nil))
    ((not (consp (car alist))) nil)
    ((eq (car (car alist)) :depth) (and (natp (cdr (car alist)))
        (brr-criteria-alistp (cdr alist))))
    ((eq (car (car alist)) :abstraction) (and (pseudo-termp (cdr (car alist)))
        (brr-criteria-alistp (cdr alist))))
    ((eq (car (car alist)) :lambda) (and (booleanp (cdr (car alist)))
        (brr-criteria-alistp (cdr alist))))
    (t (brr-criteria-alistp (cdr alist)))))

(defun make-built-in-brr-near-miss-msg
  (brr-cmd-name pat
    alist
    depth-criterion-satisfiedp
    abstraction-criterion-satisfiedp
    lambda-criterion-satisfiedp)
  (declare (xargs :guard (and (pseudo-termp pat)
        (brr-criteria-alistp alist)
        (implies depth-criterion-satisfiedp
          (natp (cdr (assoc-eq :depth alist)))))))
  (let* ((depth-msg (if depth-criterion-satisfiedp
         (list (msg "* The abstraction of ~x0 to depth ~x1, namely the ~
                          pattern ~X23, matches :TARGET."
             brr-cmd-name
             (cdr (assoc-eq :depth alist))
             (abstract-pat (cdr (assoc-eq :depth alist)) pat)
             nil))
         nil)) (abstraction-msg (if abstraction-criterion-satisfiedp
          (list (msg "* The :ABSTRACTION pattern provided in your ~
                          monitor, ~x0, matches :TARGET."
              (cdr (assoc-eq :abstraction alist))))
          nil))
      (lambda-msg (if lambda-criterion-satisfiedp
          (list (msg "* ~x0 matches :TARGET except at one or more quoted ~
                          LAMBDA constants."
              brr-cmd-name))
          nil))
      (reasons (append depth-msg abstraction-msg lambda-msg)))
    (msg "However, this is considered a NEAR MISS under the break criteria, ~
          ~X01, specified when this rule was monitored.  The following ~
          ~#2~[criterion is~/criteria are~] satisfied.~%~%~*3"
      (symbol-alist-to-keyword-value-list alist)
      nil
      (if (cdr reasons)
        1
        0)
      (list "" "~@*~%~%" "~@*~%~%" "~@*~%~%" reasons))))

(defun built-in-brr-near-missp
  (msgp lemma target rcnst criteria-alist)
  (declare (xargs :guard (and (or (weak-rewrite-rule-p lemma) (weak-linear-lemma-p lemma))
        (pseudo-termp target)
        (weak-rewrite-constant-p rcnst)
        (brr-criteria-alistp criteria-alist))))
  (mv-let (rune brr-cmd-name pattern restrictions)
    (get-brr-one-way-unify-info lemma rcnst)
    (declare (ignore rune))
    (cond ((and (pseudo-termp pattern) (alistp-listp restrictions)) (let* ((depth-arg (assoc-eq :depth criteria-alist)) (depth-criterion-satisfiedp (if (cdr depth-arg)
                (mv-let (flg unify-subst)
                  (one-way-unify-restrictions (abstract-pat (cdr depth-arg) pattern)
                    target
                    restrictions)
                  (declare (ignore unify-subst))
                  flg)
                nil))
            (abstraction-arg (if (and (not msgp) depth-criterion-satisfiedp)
                nil
                (assoc-eq :abstraction criteria-alist)))
            (abstraction-criterion-satisfiedp (if (cdr abstraction-arg)
                (mv-let (flg unify-subst)
                  (one-way-unify-restrictions (cdr abstraction-arg)
                    target
                    restrictions)
                  (declare (ignore unify-subst))
                  flg)
                nil))
            (lambda-arg (if (and (not msgp)
                  (or depth-criterion-satisfiedp
                    abstraction-criterion-satisfiedp))
                nil
                (assoc-eq :lambda criteria-alist)))
            (lambda-criterion-satisfiedp (if (cdr lambda-arg)
                (mv-let (flg unify-subst)
                  (one-way-unify-restrictions (abstract-pat (cdr lambda-arg) pattern)
                    target
                    restrictions)
                  (declare (ignore unify-subst))
                  flg)
                nil)))
          (if (or depth-criterion-satisfiedp
              abstraction-criterion-satisfiedp
              lambda-criterion-satisfiedp)
            (if msgp
              (make-built-in-brr-near-miss-msg brr-cmd-name
                pattern
                criteria-alist
                depth-criterion-satisfiedp
                abstraction-criterion-satisfiedp
                lambda-criterion-satisfiedp)
              t)
            nil)))
      (t nil))))

(defun tilde-@-failure-reason-phrase
  (failure-reason level
    unify-subst
    evisc-tuple
    free-vars-display-limit
    state)
  (tilde-@-failure-reason-phrase1 (fix-free-failure-reason failure-reason)
    level
    unify-subst
    evisc-tuple
    free-vars-display-limit
    state))

(defun brr-result
  (state)
  (let ((result (get-brr-local 'brr-result state)))
    (cond ((eq (record-type (get-brr-local 'lemma state))
         'linear-lemma) (show-poly-lst result))
      (t result))))

(defun brkpt1-brr-data-entry-builtin
  (ancestors gstack rcnst state)
  (declare (xargs :stobjs state)
    (ignore gstack rcnst state))
  (null ancestors))

(defun brkpt2-brr-data-entry-builtin
  (ancestors gstack rcnst state)
  (declare (xargs :stobjs state)
    (ignore gstack rcnst state))
  (null ancestors))

(defun update-brr-data-1-builtin
  (lemma target
    unify-subst
    type-alist
    geneqv
    ancestors
    initial-ttree
    gstack
    rcnst
    pot-lst
    whs-data)
  (declare (xargs :guard t))
  (let ((ctx 'update-brr-data-1-builtin))
    (cond ((listp whs-data) (let* ((pending (car whs-data)) (completed (cdr whs-data)))
          (cons (cons (make brr-data
                :pre (make brr-data-1
                  :lemma lemma
                  :target target
                  :unify-subst unify-subst
                  :type-alist type-alist
                  :geneqv geneqv
                  :ancestors ancestors
                  :initial-ttree initial-ttree
                  :gstack gstack
                  :rcnst rcnst
                  :pot-list pot-lst)
                :post nil
                :completed nil)
              pending)
            completed)))
      (t (er hard?
          ctx
          "Implementation error: Found whs-data not a listp:~|~y0"
          whs-data)))))

(defun update-brr-data-2-builtin
  (wonp failure-reason
    unify-subst
    gstack
    brr-result
    final-ttree
    rcnst
    ancestors
    whs-data)
  (declare (xargs :guard t)
    (ignore ancestors))
  (let ((ctx 'update-brr-data-2-builtin))
    (cond ((listp whs-data) (let* ((pending (car whs-data)) (completed (cdr whs-data)))
          (cond ((not (consp pending)) (er hard?
                ctx
                "Implementation error: Found bad whs-data ((car pending) not a ~
               cons):~|~y0"
                whs-data))
            ((null wonp) (cons (cdr pending) completed))
            ((not (weak-brr-data-p (car pending))) (er hard?
                ctx
                "Implementation error: Found bad whs-data ((car pending) not a ~
               brr-data record)):~|~y0"
                whs-data))
            (t (let ((x (make brr-data-2
                     :failure-reason failure-reason
                     :unify-subst unify-subst
                     :gstack gstack
                     :brr-result brr-result
                     :final-ttree final-ttree
                     :rcnst rcnst)))
                (cond ((consp (cdr pending)) (cond ((not (weak-brr-data-p (cadr pending))) (er hard?
                          ctx
                          "Implementation error: Found whs-data (bad (cadr ~
                     pending)):~|~y0"
                          whs-data))
                      (t (cons (cons (change brr-data
                              (cadr pending)
                              :completed (cons (change brr-data (car pending) :post x)
                                (access brr-data (cadr pending) :completed)))
                            (cddr pending))
                          completed))))
                  (t (cons nil
                      (cons (change brr-data (car pending) :post x) completed)))))))))
      (t (er hard?
          ctx
          "Implementation error: Found whs-data not a listp:~|~y0"
          whs-data)))))

(defun set-wormhole-data-fast
  (whs data)
  (declare (xargs :guard t))
  (if (consp whs)
    (cons (car whs) data)
    (cons :enter data)))

(defun brr-data-mirror
  (lst acc)
  (declare (xargs :guard (and (brr-data-listp t lst) (true-listp acc))))
  (cond ((endp lst) acc)
    (t (let* ((x1 (car lst)) (c (access brr-data x1 :completed))
          (x2 (if (null c)
              x1
              (change brr-data x1 :completed (brr-data-mirror c nil)))))
        (brr-data-mirror (cdr lst) (cons x2 acc))))))

(defun brr-data-lst
  (state)
  (declare (xargs :stobjs state))
  (er-let* ((status (get-persistent-whs 'brr-data state)))
    (value (let ((data (wormhole-data status)))
        (cond ((consp data) (ec-call (brr-data-mirror (cdr data) nil)))
          (t nil))))))

(defun clear-brr-data-lst
  nil
  (declare (xargs :guard t))
  (wormhole-eval 'brr-data
    '(lambda (whs) (set-wormhole-data-fast whs nil))
    nil))

(defun addr^p
  (addr)
  (declare (xargs :guard t))
  (cond ((atom addr) (eq addr nil))
    ((eq (car addr) '^) nil)
    ((posp (car addr)) (if (and (consp (cdr addr)) (eq (cadr addr) '^))
        (eq (cddr addr) nil)
        (addr^p (cdr addr))))
    (t nil)))

(defun safe-nth
  (n x)
  (declare (xargs :guard t))
  (if (natp n)
    (if (consp x)
      (if (= n 0)
        (car x)
        (safe-nth (- n 1) (cdr x)))
      nil)
    (if (consp x)
      (car x)
      nil)))

(defun safe-nthcdr
  (n x)
  (declare (xargs :guard t))
  (if (natp n)
    (if (consp x)
      (if (= n 0)
        x
        (safe-nthcdr (- n 1) (cdr x)))
      (if (= n 0)
        x
        nil))
    x))

(defun terminal-marker
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (terminal-marker (cdr x))
    x))

(defun get-addr^
  (addr x)
  (declare (xargs :guard (addr^p addr) :measure (acl2-count addr)))
  (cond ((endp addr) x)
    (t (let* ((n (- (car addr) 1)) (k (len x))
          (up-flg (and (cdr addr) (eq (cadr addr) '^)))
          (addr1 (if up-flg
              nil
              (cdr addr))))
        (cond ((< n k) (get-addr^ addr1
              (if up-flg
                (safe-nthcdr n x)
                (safe-nth n x))))
          ((= n k) (get-addr^ addr1
              (if up-flg
                (list '. (terminal-marker x))
                '.)))
          ((= n (+ 1 k)) (get-addr^ addr1
              (if up-flg
                (list (terminal-marker x))
                (terminal-marker x))))
          (t nil))))))

(defun update-nthcdr
  (n val x)
  (declare (xargs :guard (and (natp n) (<= n (len x)))))
  (cond ((zp n) val)
    (t (cons (car x) (update-nthcdr (- n 1) val (cdr x))))))

(defun put-addr^
  (addr val x)
  (cond ((endp addr) val)
    ((and (consp (cdr addr)) (eq (cadr addr) '^)) (cond ((= (car addr) 1) val)
        (t (let* ((n (- (car addr) 1)) (k (len x)))
            (cond ((< n k) (update-nthcdr n val x))
              ((or (= n k) (= n (+ 1 k))) (update-nthcdr k
                  (if (and (consp val)
                      (eq (car val) '.)
                      (consp (cdr val))
                      (null (cddr val)))
                    (cadr val)
                    val)
                  x))
              (t x))))))
    (t (let* ((n (- (car addr) 1)) (k (len x)))
        (cond ((< n k) (update-nth n (put-addr^ (cdr addr) val (nth n x)) x))
          ((and (or (= n k) (= n (+ k 1))) (null (cdr addr))) (update-nthcdr k
              (if (and (consp val)
                  (eq (car val) '.)
                  (consp (cdr val))
                  (null (cddr val)))
                (cadr val)
                val)
              x))
          (t x))))))