simplify

(defun negate-lit
  (term type-alist ens force-flg wrld)
  (mv-let (knownp nilp ttree)
    (known-whether-nil term
      type-alist
      ens
      force-flg
      nil
      wrld
      nil)
    (cond (knownp (cond (nilp (mv *t* ttree)) (t (mv *nil* ttree))))
      (t (mv (dumb-negate-lit term) nil)))))

(defun pegate-lit
  (term type-alist ens force-flg wrld)
  (mv-let (knownp nilp ttree)
    (known-whether-nil term
      type-alist
      ens
      force-flg
      nil
      wrld
      nil)
    (cond (knownp (cond (nilp (mv *nil* ttree)) (t (mv *t* ttree))))
      (t (mv term nil)))))

(defun add-literal
  (lit cl at-end-flg)
  (cond ((quotep lit) (cond ((equal lit *nil*) cl) (t *true-clause*)))
    ((equal cl *true-clause*) *true-clause*)
    ((member-complement-term lit cl) *true-clause*)
    ((variablep lit) (cond ((member-term lit cl) cl)
        (at-end-flg (append cl (list lit)))
        (t (cons lit cl))))
    ((eq (ffn-symb lit) 'hard-error) cl)
    ((and (eq (ffn-symb lit) 'rationalp)
       (member-complement-term1 (fcons-term 'integerp (fargs lit))
         cl)) *true-clause*)
    ((and (eq (ffn-symb lit) 'not)
       (ffn-symb-p (fargn lit 1) 'integerp)
       (member-equal (fcons-term 'rationalp (fargs (fargn lit 1)))
         cl)) *true-clause*)
    ((member-term lit cl) cl)
    (at-end-flg (append cl (list lit)))
    (t (cons lit cl))))

(defun add-each-literal
  (cl)
  (cond ((null cl) nil)
    (t (add-literal (car cl) (add-each-literal (cdr cl)) nil))))

(defun subsumes
  (init-subsumes-count cl1 cl2 alist)
  (cond ((time-limit5-reached-p "Out of time in subsumption (subsumes).") nil)
    ((null init-subsumes-count) (subsumes!-rec cl1 cl2 alist))
    (t (let ((temp (subsumes-rec init-subsumes-count cl1 cl2 alist)))
        (cond ((eql temp 0) '?) (t (< 0 temp)))))))

(defun some-member-subsumes
  (init-subsumes-count cl-set cl acc)
  (cond ((null cl-set) acc)
    (t (let ((temp (subsumes init-subsumes-count (car cl-set) cl nil)))
        (cond ((eq temp t))
          (t (some-member-subsumes init-subsumes-count
              (cdr cl-set)
              cl
              (or temp acc))))))))

(defun equal-mod-commuting-lst
  (cl1 cl2)
  (cond ((endp cl1) (endp cl2))
    ((endp cl2) nil)
    (t (and (equal-mod-commuting (car cl1) (car cl2) nil)
        (equal-mod-commuting-lst (cdr cl1) (cdr cl2))))))

(defun member-equal-mod-commuting-lst
  (cl cl-set)
  (cond ((endp cl-set) nil)
    ((equal-mod-commuting-lst cl (car cl-set)) t)
    (t (member-equal-mod-commuting-lst cl (cdr cl-set)))))

(defun conjoin-clause-to-clause-set
  (cl cl-set)
  (cond ((member-equal *t* cl) cl-set)
    ((member-equal-mod-commuting-lst cl cl-set) cl-set)
    (t (cons cl cl-set))))

(defun add-each-literal-lst
  (cl-set)
  (cond ((null cl-set) nil)
    (t (conjoin-clause-to-clause-set (add-each-literal (car cl-set))
        (add-each-literal-lst (cdr cl-set))))))

(defun conjoin-clause-sets-bound-builtin
  nil
  (declare (xargs :guard t :mode :logic))
  50)

(defun conjoin-clause-sets-rec
  (cl-set1 cl-set2)
  (cond ((null cl-set1) cl-set2)
    (t (conjoin-clause-to-clause-set (car cl-set1)
        (conjoin-clause-sets-rec (cdr cl-set1) cl-set2)))))

(defun conjoin-clause-to-clause-set-trivial
  (cl cl-set)
  (cond ((member-equal *t* cl) cl-set) (t (cons cl cl-set))))

(defun conjoin-clause-sets-trivial
  (cl-set1 cl-set2)
  (cond ((null cl-set1) cl-set2)
    (t (conjoin-clause-to-clause-set-trivial (car cl-set1)
        (conjoin-clause-sets-trivial (cdr cl-set1) cl-set2)))))

(defun conjoin-clause-sets
  (cl-set1 cl-set2)
  (cond ((nthcdr (conjoin-clause-sets-bound) cl-set1) (conjoin-clause-sets-trivial cl-set1 cl-set2))
    (t (conjoin-clause-sets-rec cl-set1 cl-set2))))

(defun some-element-member-complement-term
  (lst1 lst2)
  (cond ((null lst1) nil)
    ((member-complement-term (car lst1) lst2) t)
    (t (some-element-member-complement-term (cdr lst1) lst2))))

(defun disjoin-clauses1
  (cl1 cl2)
  (cond ((endp cl2) cl1)
    (t (disjoin-clauses1 (add-literal (car cl2) cl1 t) (cdr cl2)))))

(defun disjoin-clauses
  (cl1 cl2)
  (cond ((or (equal cl1 *true-clause*) (equal cl2 *true-clause*)) *true-clause*)
    ((null cl1) cl2)
    ((null cl2) cl1)
    (t (disjoin-clauses1 cl1 cl2))))

(defun disjoin-clause-segment-to-clause-set
  (segment cl-set)
  (cond ((null cl-set) nil)
    (t (conjoin-clause-to-clause-set (disjoin-clauses segment (car cl-set))
        (disjoin-clause-segment-to-clause-set segment (cdr cl-set))))))

(defun split-on-assumptions
  (assumptions cl ans)
  (cond ((null assumptions) ans)
    (t (split-on-assumptions (cdr assumptions)
        cl
        (conjoin-clause-to-clause-set (add-literal (car assumptions) cl nil)
          ans)))))

(defun rewrite-clause-action
  (lit branches)
  (cond ((consp branches) (cond ((null (cdr branches)) (cond ((null (car branches)) 'shown-false)
            ((and (null (cdr (car branches)))
               (equal lit (car (car branches)))) 'no-change)
            (t 'change)))
        (t 'change)))
    (t 'shown-true)))

(defun suspend-fc-activation
  (act inst-hyp hyps unify-subst ttree)
  (cond ((equal unify-subst (access fc-activation act :unify-subst)) (cond ((and (equal hyps (access fc-activation act :hyps))
           (equal ttree (access fc-activation act :ttree))) (cond ((equal inst-hyp (access fc-activation act :inst-hyp)) act)
            (t (change fc-activation act :inst-hyp inst-hyp))))
        (t (change fc-activation
            act
            :inst-hyp inst-hyp
            :hyps hyps
            :ttree ttree))))
    (t (change fc-activation
        act
        :inst-hyp inst-hyp
        :hyps hyps
        :unify-subst unify-subst
        :ttree ttree))))

(defun prettyify-fc-activation
  (act level)
  (let* ((rune (access forward-chaining-rule
         (access fc-activation act :rule)
         :rune)) (name (if (null (cddr rune))
          (cadr rune)
          (cdr rune)))
      (inst-trigger (access fc-activation act :inst-trigger))
      (inst-hyp (access fc-activation act :inst-hyp))
      (hyps (access fc-activation act :hyps))
      (unify-subst (access fc-activation act :unify-subst))
      (pretty-subst (pairlis$ (strip-cars unify-subst)
          (pairlis-x2 (strip-cdrs unify-subst) nil)))
      (k (+ 1
          (- (len (access forward-chaining-rule
                (access fc-activation act :rule)
                :hyps))
            (if (and (consp inst-hyp) (eq (car inst-hyp) :fc-free-vars))
              (len hyps)
              (+ 1 (len hyps)))))))
    (case level
      (1 `(,NAME (:trigger ,INST-TRIGGER)
          (:blocked-hyp ,K)
          ,(IF (AND (CONSP INST-HYP) (EQ (CAR INST-HYP) :FC-FREE-VARS))
     `(:REASON :FREE
       ,(SUBLIS-VAR
         (BIND-FREE-VARS-TO-UNBOUND-FREE-VARS (ALL-VARS (CAR HYPS))
                                              UNIFY-SUBST)
         (CAR HYPS))
       ,(LEN (CDDR INST-HYP)))
     `(:REASON ,INST-HYP))))
      (otherwise `(,RUNE (:trigger ,INST-TRIGGER)
          (:blocked-hyp ,K)
          ,(IF (AND (CONSP INST-HYP) (EQ (CAR INST-HYP) :FC-FREE-VARS))
     `(:REASON :FREE
       ,(SUBLIS-VAR
         (BIND-FREE-VARS-TO-UNBOUND-FREE-VARS (ALL-VARS (CAR HYPS))
                                              UNIFY-SUBST)
         (CAR HYPS))
       ,(CDDR INST-HYP))
     `(:REASON ,INST-HYP))
          (:unify-subst ,PRETTY-SUBST))))))

(defun prettyify-fc-activations
  (acts level)
  (cond ((endp acts) nil)
    (t (cons (prettyify-fc-activation (car acts) level)
        (prettyify-fc-activations (cdr acts) level)))))

(defun make-fc-activation
  (term rule ttree ens)
  (cond ((not (enabled-numep (access forward-chaining-rule rule :nume)
         ens)) nil)
    (t (mv-let (unify-ans unify-subst)
        (one-way-unify (access forward-chaining-rule rule :trigger)
          term)
        (cond ((null unify-ans) nil)
          (t (let ((rule-hyps (access forward-chaining-rule rule :hyps)))
              (make fc-activation
                :inst-hyp *t*
                :hyps rule-hyps
                :ttree ttree
                :unify-subst unify-subst
                :inst-trigger term
                :rule rule))))))))

(defun make-fc-activations
  (term rules ttree ens activations)
  (cond ((endp rules) activations)
    (t (let ((act (make-fc-activation term (car rules) ttree ens)))
        (make-fc-activations term
          (cdr rules)
          ttree
          ens
          (if act
            (cons act activations)
            activations))))))

(defun collect-terms-and-activations-from-fcd-lst
  (fcd-lst wrld ens trigger-terms activations)
  (cond ((endp fcd-lst) (mv trigger-terms activations))
    (t (mv-let (trigger-terms activations)
        (collect-terms-and-activations (access fc-derivation (car fcd-lst) :concl)
          (add-to-tag-tree! 'fc-derivation (car fcd-lst) nil)
          wrld
          ens
          trigger-terms
          activations)
        (collect-terms-and-activations-from-fcd-lst (cdr fcd-lst)
          wrld
          ens
          trigger-terms
          activations)))))

(defun mult-search-type-alist
  (rest-hyps concls
    term
    typ
    type-alist
    unify-subst
    ttree
    oncep
    keys-seen
    compound-rec-rune?)
  (cond ((null type-alist) (mv nil nil nil))
    ((and (ts-subsetp (cadr (car type-alist)) typ)
       (not (member-equal (car (car type-alist)) keys-seen))) (mv-let (ans new-unify-subst)
        (one-way-unify1 term (car (car type-alist)) unify-subst)
        (cond (ans (let ((diff-alist (alist-difference-eq new-unify-subst unify-subst)))
              (cond ((or oncep
                   (not (or (sublis-var-lstp diff-alist rest-hyps)
                       (sublis-var-lstp diff-alist concls)))) (mv (list new-unify-subst)
                    (list (cons-tag-trees (cddr (car type-alist))
                        (push-lemma? compound-rec-rune? ttree)))
                    (list (car (car type-alist)))))
                (t (mv-let (other-unifies other-ttrees other-instances)
                    (mult-search-type-alist rest-hyps
                      concls
                      term
                      typ
                      (cdr type-alist)
                      unify-subst
                      ttree
                      oncep
                      keys-seen
                      compound-rec-rune?)
                    (mv (cons new-unify-subst other-unifies)
                      (cons (cons-tag-trees (cddr (car type-alist))
                          (push-lemma? compound-rec-rune? ttree))
                        other-ttrees)
                      (cons (car (car type-alist)) other-instances)))))))
          (t (mult-search-type-alist rest-hyps
              concls
              term
              typ
              (cdr type-alist)
              new-unify-subst
              ttree
              oncep
              keys-seen
              compound-rec-rune?)))))
    (t (mult-search-type-alist rest-hyps
        concls
        term
        typ
        (cdr type-alist)
        unify-subst
        ttree
        oncep
        keys-seen
        compound-rec-rune?))))

(defun mult-lookup-hyp
  (hyp rest-hyps
    concls
    type-alist
    wrld
    unify-subst
    ttree
    oncep
    last-keys-seen
    ens)
  (mv-let (term typ rune)
    (term-and-typ-to-lookup hyp wrld ens)
    (mult-search-type-alist rest-hyps
      concls
      term
      typ
      type-alist
      unify-subst
      ttree
      oncep
      last-keys-seen
      rune)))

(defun add-fc-derivations
  (rune concls
    unify-subst
    inst-trigger
    fc-round
    ens
    wrld
    state
    ttree
    fcd-lst)
  (cond ((null concls) fcd-lst)
    (t (mv-let (flg concl new-ttree)
        (eval-ground-subexpressions (car concls)
          ens
          wrld
          state
          ttree)
        (declare (ignore flg))
        (mv-let (fn-cnt p-fn-cnt)
          (fn-count concl)
          (add-fc-derivations rune
            (cdr concls)
            unify-subst
            inst-trigger
            fc-round
            ens
            wrld
            state
            ttree
            (cons (make fc-derivation
                :fc-round fc-round
                :rune rune
                :concl concl
                :fn-cnt fn-cnt
                :p-fn-cnt p-fn-cnt
                :inst-trigger inst-trigger
                :unify-subst unify-subst
                :ttree new-ttree)
              fcd-lst)))))))

(defun current-fc-call-number
  (data)
  (car (car (cdr (assoc-eq :forward-chain-calls data)))))

(defun current-fc-call-alist
  (data)
  (cdr (car (cdr (assoc-eq :forward-chain-calls data)))))

(defun put-current-fc-call-alist
  (call-alist data)
  (let* ((calls-alist (cdr (assoc-eq :forward-chain-calls data))) (temp (car calls-alist))
      (k (car temp)))
    (put-assoc-eq :forward-chain-calls (cons (cons k call-alist) (cdr calls-alist))
      data)))

(defun initialize-fc-wormhole-sites
  nil
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((data (wormhole-data whs)))
        (set-wormhole-data whs
          `((:criteria ,@(CDR (ASSOC-EQ :CRITERIA DATA))) (:report-on-the-flyp . ,(CDR (ASSOC-EQ :REPORT-ON-THE-FLYP DATA)))
            (:forward-chain-calls)))))
    nil))

(defun show-fc-criteria
  nil
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (prog2$ (cw "Forward Chaining Tracking Criteria:~%~x0~%"
          (cdr (assoc-eq :criteria (wormhole-data whs))))
        whs))
    nil))

(defun reset-fc-reporting
  nil
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (set-wormhole-data whs
        '((:criteria) (:report-on-the-flyp) (:forward-chain-calls))))
    nil))

(defun translate-fc-criterion
  (x state)
  (cond ((and (true-listp x) (equal (length x) 3)) (let ((rune (car x)) (inst-trigger (cadr x)) (concl (caddr x)))
        (cond ((not (or (eq rune t)
               (and (runep rune (w state))
                 (eq (car rune) :forward-chaining)))) (er soft
              'set-fc-criteria
              "~x0 is not a :FORWARD-CHAINING rune."
              rune))
          (t (er-let* ((inst-trigger (cond ((eq inst-trigger t) (value t))
                   (t (translate inst-trigger
                       t
                       t
                       t
                       'add-fc-criterion
                       (w state)
                       state)))) (concl (cond ((eq concl t) (value t))
                    (t (translate concl t t t 'add-fc-criterion (w state) state)))))
              (value (list rune inst-trigger concl)))))))
    (t (er soft
        'set-fc-criteria
        "Each element of a criteria must be a triple, (rune inst-trigger ~
           inst-concl), where rune is a :FORWARD-CHAINING rune or t, ~
           inst-trigger is a term or t, and inst-concl is a term or t.  ~
           But ~x0 is not of this form."
        x))))

(defun translate-fc-criteria
  (lst state)
  (cond ((atom lst) (cond ((equal lst nil) (value nil))
        (t (er soft
            'set-fc-criteria
            "The criteria must be a true-list."))))
    (t (er-let* ((triple (translate-fc-criterion (car lst) state)) (rest (translate-fc-criteria (cdr lst) state)))
        (value (cons triple rest))))))

(defun set-fc-criteria-fn
  (x state)
  (er-let* ((criteria (cond ((equal x '(nil)) (value nil))
         ((equal x '(t)) (value '((t t t))))
         (t (translate-fc-criteria x state)))))
    (prog2$ (wormhole-eval 'fc-wormhole
        '(lambda (whs)
          (set-wormhole-data whs
            (put-assoc-eq :criteria criteria (wormhole-data whs))))
        nil)
      (value nil))))

(defun set-fc-report-on-the-fly
  (flg)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((data (wormhole-data whs)))
        (prog2$ (cond (flg (cond ((cdr (assoc-eq :criteria data)) (cw "On-the-fly reporting of forward-chaining activity is ~
                  enabled.  The criteria being tracked are: ~x0.~%"
                    (cdr (assoc-eq :criteria data))))
                (t (cw "On-the-fly reporting of forward-chaining activity is enabled ~
                  but no data will be collected because there are no criteria.~%"))))
            ((cdr (assoc-eq :criteria data)) (cw "On-the-fly reporting of forward-chaining activity is disabled.  ~
                The criteria being tracked are: ~x0.~%"
                (cdr (assoc-eq :criteria data))))
            (t (cw "On-the-fly reporting of forward-chaining activity is disabled ~
                but no data will be collected because there are no criteria.~%")))
          (set-wormhole-data whs
            (put-assoc-eq :report-on-the-flyp flg data)))))
    nil))

(defun new-fc-call
  (caller cl
    pts
    force-flg
    do-not-reconsiderp
    wrld
    ens
    oncep-override)
  (declare (ignore wrld ens))
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data))))
        (cond ((cdr (assoc-eq :criteria data)) (set-wormhole-data whs
              (put-assoc-eq :forward-chain-calls (cons (cons (+ 1 (or (car (car calls-alist)) 0))
                    `((:blocked-false-satisfying-activations) (:all-satisfying-fc-derivations)
                      (:approved-satisfying-fc-derivations)
                      (:leftover-activations)
                      (:input . ,(LIST CALLER CL PTS FORCE-FLG DO-NOT-RECONSIDERP 'WRLD 'ENS ONCEP-OVERRIDE
       'STATE))
                      (:rounds)
                      (:output)))
                  calls-alist)
                data)))
          (t whs))))
    :no-wormhole-lock))

(defun member-one-way-unify1
  (term pat-lst unify-subst)
  (cond ((endp pat-lst) nil)
    (t (mv-let (flg alist)
        (one-way-unify1 (car pat-lst) term unify-subst)
        (declare (ignore alist))
        (cond (flg t)
          (t (member-one-way-unify1 term (cdr pat-lst) unify-subst)))))))

(defun satisfying-fc-activation1p
  (criterion act)
  (let ((rune (car criterion)) (trig (cadr criterion))
      (concl (caddr criterion))
      (rule (access fc-activation act :rule)))
    (and (or (eq rune t)
        (equal rune (access forward-chaining-rule rule :rune)))
      (or (eq trig t)
        (equal trig (access fc-activation act :inst-trigger)))
      (or (eq concl t)
        (member-one-way-unify1 concl
          (access forward-chaining-rule rule :concls)
          (access fc-activation act :unify-subst))))))

(defun satisfying-fc-activationp
  (criteria act)
  (cond ((endp criteria) nil)
    (t (or (satisfying-fc-activation1p (car criteria) act)
        (satisfying-fc-activationp (cdr criteria) act)))))

(defun collect-satisfying-fc-activations
  (criteria acts ans)
  (cond ((endp acts) ans)
    ((satisfying-fc-activationp criteria (car acts)) (collect-satisfying-fc-activations criteria
        (cdr acts)
        (cons (car acts) ans)))
    (t (collect-satisfying-fc-activations criteria (cdr acts) ans))))

(defun satisfying-virtual-fc-activation1p
  (criterion act0 unify-subst)
  (let ((rune (car criterion)) (trig (cadr criterion))
      (concl (caddr criterion))
      (rule (access fc-activation act0 :rule)))
    (and (or (eq rune t)
        (equal rune (access forward-chaining-rule rule :rune)))
      (or (eq trig t)
        (equal trig (access fc-activation act0 :inst-trigger)))
      (or (eq concl t)
        (member-one-way-unify1 concl
          (access forward-chaining-rule rule :concls)
          unify-subst)))))

(defun satisfying-virtual-fc-activationp
  (criteria act0 unify-subst)
  (cond ((endp criteria) nil)
    (t (or (satisfying-virtual-fc-activation1p (car criteria)
          act0
          unify-subst)
        (satisfying-virtual-fc-activationp (cdr criteria)
          act0
          unify-subst)))))

(defun satisfying-fc-derivation1p
  (criterion fcd)
  (let ((rune (car criterion)) (trig (cadr criterion))
      (concl (caddr criterion)))
    (and (or (eq rune t)
        (equal rune (access fc-derivation fcd :rune)))
      (or (eq trig t)
        (equal trig (access fc-derivation fcd :inst-trigger)))
      (or (eq concl t)
        (equal concl (access fc-derivation fcd :concl))))))

(defun satisfying-fc-derivationp
  (criteria fcd)
  (cond ((endp criteria) nil)
    (t (or (satisfying-fc-derivation1p (car criteria) fcd)
        (satisfying-fc-derivationp (cdr criteria) fcd)))))

(defun collect-satisfying-fc-derivations
  (criteria fcd-lst ans)
  (cond ((endp fcd-lst) ans)
    ((satisfying-fc-derivationp criteria (car fcd-lst)) (collect-satisfying-fc-derivations criteria
        (cdr fcd-lst)
        (cons (car fcd-lst) ans)))
    (t (collect-satisfying-fc-derivations criteria
        (cdr fcd-lst)
        ans))))

(defun filter-satisfying-virtual-fc-activation
  (act0 inst-hyp hyps unify-subst ttree)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
        (cond ((null criteria) whs)
          ((satisfying-virtual-fc-activationp criteria
             act0
             unify-subst) (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
                (k (car (car calls-alist)))
                (call-alist (cdr (car calls-alist)))
                (act (suspend-fc-activation act0 inst-hyp hyps unify-subst ttree)))
              (set-wormhole-data whs
                (put-assoc-eq :forward-chain-calls (cons (cons k
                      (put-assoc-eq :blocked-false-satisfying-activations (cons act
                          (cdr (assoc-eq :blocked-false-satisfying-activations call-alist)))
                        call-alist))
                    (cdr calls-alist))
                  data))))
          (t whs))))
    :no-wormhole-lock))

(defun filter-all-satisfying-fc-derivations
  (fcd-lst)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
        (cond ((null criteria) whs)
          (t (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
                (k (car (car calls-alist)))
                (call-alist (cdr (car calls-alist))))
              (set-wormhole-data whs
                (put-assoc-eq :forward-chain-calls (cons (cons k
                      (put-assoc-eq :all-satisfying-fc-derivations (collect-satisfying-fc-derivations criteria
                          fcd-lst
                          (cdr (assoc-eq :all-satisfying-fc-derivations call-alist)))
                        call-alist))
                    (cdr calls-alist))
                  data)))))))
    :no-wormhole-lock))

(defun filter-satisfying-fc-activations
  (acts)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
        (cond ((null criteria) whs)
          (t (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
                (k (car (car calls-alist)))
                (call-alist (cdr (car calls-alist))))
              (set-wormhole-data whs
                (put-assoc-eq :forward-chain-calls (cons (cons k
                      (put-assoc-eq :leftover-activations (collect-satisfying-fc-activations criteria
                          acts
                          (cdr (assoc-eq :leftover-activations call-alist)))
                        call-alist))
                    (cdr calls-alist))
                  data)))))))
    :no-wormhole-lock))

(defun filter-redundant-approved-fc-derivation
  (fcd)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
        (cond ((null criteria) whs)
          ((satisfying-fc-derivationp criteria fcd) (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
                (k (car (car calls-alist)))
                (call-alist (cdr (car calls-alist))))
              (set-wormhole-data whs
                (put-assoc-eq :forward-chain-calls (cons (cons k
                      (put-assoc-eq :redundant-approved-fc-derivations (cons fcd
                          (cdr (assoc-eq :redundant-approved-fc-derivations call-alist)))
                        call-alist))
                    (cdr calls-alist))
                  data))))
          (t whs))))
    :no-wormhole-lock))

(defun collect-rune-trigger-pairs-from-fc-activations
  (acts ans)
  (cond ((endp acts) ans)
    (t (collect-rune-trigger-pairs-from-fc-activations (cdr acts)
        (add-to-set-equal (cons (access forward-chaining-rule
              (access fc-activation (car acts) :rule)
              :rune)
            (access fc-activation (car acts) :inst-trigger))
          ans)))))

(defun collect-rune-trigger-pairs-from-fc-derivations
  (fcds ans)
  (cond ((endp fcds) ans)
    (t (collect-rune-trigger-pairs-from-fc-derivations (cdr fcds)
        (add-to-set-equal (cons (access fc-derivation (car fcds) :rune)
            (access fc-derivation (car fcds) :inst-trigger))
          ans)))))

(defun prettyify-subst
  (alist)
  (cond ((endp alist) nil)
    (t (cons (list (car (car alist)) (cdr (car alist)))
        (prettyify-subst (cdr alist))))))

(defun collect-fc-status-site-1
  (rune inst-trigger acts)
  (cond ((endp acts) nil)
    ((and (equal rune
         (access forward-chaining-rule
           (access fc-activation (car acts) :rule)
           :rune))
       (equal inst-trigger
         (access fc-activation (car acts) :inst-trigger))) (cons `((:unify-subst ,(PRETTYIFY-SUBST (ACCESS FC-ACTIVATION (CAR ACTS) :UNIFY-SUBST))) (:disposition blocked
            false
            ,(ACCESS FC-ACTIVATION (CAR ACTS) :INST-HYP)))
        (collect-fc-status-site-1 rune inst-trigger (cdr acts))))
    (t (collect-fc-status-site-1 rune inst-trigger (cdr acts)))))

(defun collect-fc-status-sites-2-3-5
  (rune inst-trigger
    all-fcds
    approved-fcds
    redundant-approved-fc-derivations)
  (cond ((endp all-fcds) nil)
    ((and (equal rune (access fc-derivation (car all-fcds) :rune))
       (equal inst-trigger
         (access fc-derivation (car all-fcds) :inst-trigger))) (cons `((:unify-subst ,(PRETTYIFY-SUBST (ACCESS FC-DERIVATION (CAR ALL-FCDS) :UNIFY-SUBST))) (:disposition success
            ,(IF (MEMBER-EQUAL (CAR ALL-FCDS) APPROVED-FCDS)
     (IF (MEMBER-EQUAL (CAR ALL-FCDS) REDUNDANT-APPROVED-FC-DERIVATIONS)
         'REDUNDANT
         'APPROVED)
     'REJECTED)
            ,(ACCESS FC-DERIVATION (CAR ALL-FCDS) :CONCL)))
        (collect-fc-status-sites-2-3-5 rune
          inst-trigger
          (cdr all-fcds)
          approved-fcds
          redundant-approved-fc-derivations)))
    (t (collect-fc-status-sites-2-3-5 rune
        inst-trigger
        (cdr all-fcds)
        approved-fcds
        redundant-approved-fc-derivations))))

(defun prettyify-blocked-fc-inst-hyp
  (inst-hyp hyps unify-subst)
  (cond ((and (consp inst-hyp) (eq (car inst-hyp) :fc-free-vars)) (let ((hyp (sublis-var (bind-free-vars-to-unbound-free-vars (all-vars (car hyps))
               unify-subst)
             (car hyps))))
        (if (cadr inst-hyp)
          `(,(CADR INST-HYP) ,HYP)
          hyp)))
    (t inst-hyp)))

(defun collect-fc-status-site-4
  (rune inst-trigger acts)
  (cond ((endp acts) nil)
    ((and (equal rune
         (access forward-chaining-rule
           (access fc-activation (car acts) :rule)
           :rune))
       (equal inst-trigger
         (access fc-activation (car acts) :inst-trigger))) (let ((inst-hyp (access fc-activation (car acts) :inst-hyp)))
        (cons `((:unify-subst ,(PRETTYIFY-SUBST (ACCESS FC-ACTIVATION (CAR ACTS) :UNIFY-SUBST))) (:disposition blocked
              ,(IF (AND (CONSP INST-HYP) (EQ (CAR INST-HYP) :FC-FREE-VARS))
     'UNRELIEVED-HYP-FREE
     'UNRELIEVED-HYP)
              ,(PRETTYIFY-BLOCKED-FC-INST-HYP INST-HYP
                                (ACCESS FC-ACTIVATION (CAR ACTS) :HYPS)
                                (ACCESS FC-ACTIVATION (CAR ACTS) :UNIFY-SUBST))))
          (collect-fc-status-site-4 rune inst-trigger (cdr acts)))))
    (t (collect-fc-status-site-4 rune inst-trigger (cdr acts)))))

(defun collect-fc-status
  (rune inst-trigger site1 site2 site3 site4 site5)
  `(,RUNE (:trigger ,INST-TRIGGER)
    ,@(COLLECT-FC-STATUS-SITE-1 RUNE INST-TRIGGER SITE1)
    ,@(COLLECT-FC-STATUS-SITES-2-3-5 RUNE INST-TRIGGER SITE2 SITE3 SITE5)
    ,@(COLLECT-FC-STATUS-SITE-4 RUNE INST-TRIGGER SITE4)))

(defun make-fc-activity-report1
  (rune-trigger-pairs site1 site2 site3 site4 site5)
  (cond ((endp rune-trigger-pairs) nil)
    (t (cons (collect-fc-status (car (car rune-trigger-pairs))
          (cdr (car rune-trigger-pairs))
          site1
          site2
          site3
          site4
          site5)
        (make-fc-activity-report1 (cdr rune-trigger-pairs)
          site1
          site2
          site3
          site4
          site5)))))

(defun make-fc-activity-report
  (call-alist)
  (let* ((site1 (cdr (assoc-eq :blocked-false-satisfying-activations call-alist))) (site2 (cdr (assoc-eq :all-satisfying-fc-derivations call-alist)))
      (site3 (cdr (assoc-eq :approved-satisfying-fc-derivations call-alist)))
      (site4 (cdr (assoc-eq :leftover-activations call-alist)))
      (site5 (cdr (assoc-eq :redundant-approved-fc-derivations call-alist)))
      (rune-trigger-pairs (collect-rune-trigger-pairs-from-fc-activations site1
          (collect-rune-trigger-pairs-from-fc-derivations site2
            (collect-rune-trigger-pairs-from-fc-activations site4 nil)))))
    (merge-sort-lexorder (make-fc-activity-report1 rune-trigger-pairs
        site1
        site2
        site3
        site4
        site5))))

(defun fc-report1
  (whs k)
  (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
      (temp (assoc-equal k calls-alist)))
    (cond ((and temp (cdr (assoc-eq :output (cdr temp)))) (let* ((call-alist (cdr temp)) (input (cdr (assoc-eq :input call-alist)))
            (caller (car input))
            (clause (cadr input))
            (output (cdr (assoc-eq :output call-alist)))
            (flg (car output))
            (rounds (cdr (assoc-eq :rounds call-alist)))
            (activity (make-fc-activity-report call-alist)))
          (cw "~%~
       -----------------------------------------------------------------~%~
       Forward Chaining Report ~x0:~%~
       Caller: ~x1~%~
       Clause: ~x2~%~
       Number of Rounds: ~x3~%~
       Contradictionp: ~x4~%~
       Activations:~%~
       ~x5~%~
       -----------------------------------------------------------------~%"
            k
            caller
            clause
            rounds
            flg
            activity)))
      (t (cw "~%There is no Forward Chaining Report for ~x0.~%" k)))))

(defun fc-report
  (k)
  (wormhole-eval 'fc-wormhole
    '(lambda (whs)
      (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
        (cond ((null criteria) whs)
          (t (prog2$ (fc-report1 whs k) whs)))))
    nil))

(defun fc-exit
  (flg type-alist
    ttree-or-fc-pairs
    caller
    rounds
    all-approved-fcds
    all-leftover-activations)
  (prog2$ (wormhole-eval 'fc-wormhole
      '(lambda (whs)
        (let ((criteria (cdr (assoc-eq :criteria (wormhole-data whs)))))
          (cond ((null criteria) whs)
            (t (let* ((data (wormhole-data whs)) (calls-alist (cdr (assoc-eq :forward-chain-calls data)))
                  (k (car (car calls-alist)))
                  (call-alist (cdr (car calls-alist)))
                  (new-data (put-assoc-eq :forward-chain-calls (cons (cons k
                          (put-assoc-eq :approved-satisfying-fc-derivations (collect-satisfying-fc-derivations criteria
                              all-approved-fcds
                              nil)
                            (put-assoc-eq :leftover-activations (collect-satisfying-fc-activations criteria
                                all-leftover-activations
                                nil)
                              (put-assoc-eq :rounds rounds
                                (put-assoc-eq :output (list flg type-alist ttree-or-fc-pairs)
                                  call-alist)))))
                        (cdr calls-alist))
                      data))
                  (new-whs (set-wormhole-data whs new-data)))
                (cond ((cdr (assoc-eq :report-on-the-flyp new-data)) (prog2$ (fc-report1 new-whs k) new-whs))
                  (t (prog2$ (cw "~%(Forward Chaining on behalf of ~x0:  (FC-Report ~x1))~%"
                        caller
                        k)
                      new-whs))))))))
      :no-wormhole-lock)
    (mv flg type-alist ttree-or-fc-pairs)))

(defun advance-fc-activation
  (act fc-round
    type-alist
    ens
    force-flg
    wrld
    state
    oncep-override
    suspensions
    fcd-lst)
  (with-accumulated-persistence (access forward-chaining-rule
      (access fc-activation act :rule)
      :rune)
    (suspensions1 fcd-lst1)
    t
    (advance-fc-activation1 act
      (access fc-activation act :inst-hyp)
      (access fc-activation act :hyps)
      (access fc-activation act :unify-subst)
      (access fc-activation act :ttree)
      fc-round
      type-alist
      ens
      force-flg
      wrld
      state
      oncep-override
      suspensions
      fcd-lst)))

(defun advance-fc-activations
  (lst fc-round
    type-alist
    ens
    force-flg
    wrld
    state
    oncep-override
    suspensions
    fcd-lst)
  (cond ((null lst) (mv suspensions fcd-lst))
    (t (mv-let (suspensions1 fcd-lst1)
        (advance-fc-activation (car lst)
          fc-round
          type-alist
          ens
          force-flg
          wrld
          state
          oncep-override
          suspensions
          fcd-lst)
        (advance-fc-activations (cdr lst)
          fc-round
          type-alist
          ens
          force-flg
          wrld
          state
          oncep-override
          suspensions1
          fcd-lst1)))))

(defun fc-pair-lst
  (fcd-lst)
  (cond ((null fcd-lst) nil)
    (t (cons (cons (access fc-derivation (car fcd-lst) :concl)
          (push-lemma (access fc-derivation (car fcd-lst) :rune)
            (expunge-fc-derivations (access fc-derivation (car fcd-lst) :ttree))))
        (fc-pair-lst (cdr fcd-lst))))))

(defun fc-pair-lst-type-alist
  (fc-pair-lst fcd-lst type-alist force-flg ens wrld)
  (cond ((null fc-pair-lst) (mv nil type-alist nil))
    (t (mv-let (mbt mbf tta fta ttree)
        (assume-true-false (car (car fc-pair-lst))
          (cdr (car fc-pair-lst))
          force-flg
          nil
          type-alist
          ens
          wrld
          nil
          nil
          :fta)
        (declare (ignore fta))
        (cond (mbf (mv t nil ttree))
          (mbt (prog2$ (filter-redundant-approved-fc-derivation (car fcd-lst))
              (fc-pair-lst-type-alist (cdr fc-pair-lst)
                (cdr fcd-lst)
                type-alist
                force-flg
                ens
                wrld)))
          (t (fc-pair-lst-type-alist (cdr fc-pair-lst)
              (cdr fcd-lst)
              tta
              force-flg
              ens
              wrld)))))))

(defun fcd-runep-lst
  (rune lst)
  (cond ((endp lst) nil)
    (t (or (equal rune (access fc-derivation (car lst) :rune))
        (fcd-runep rune (access fc-derivation (car lst) :ttree))
        (fcd-runep-lst rune (cdr lst))))))

(defun fcd-worse-than-or-equal-lst
  (concl fn-cnt p-fn-cnt lst)
  (cond ((endp lst) nil)
    (t (or (and (let ((fc-fn-cnt (access fc-derivation (car lst) :fn-cnt)))
            (or (> fn-cnt fc-fn-cnt)
              (and (eql fn-cnt fc-fn-cnt)
                (>= p-fn-cnt (access fc-derivation (car lst) :p-fn-cnt)))))
          (worse-than-or-equal concl
            (access fc-derivation (car lst) :concl)))
        (fcd-worse-than-or-equal concl
          fn-cnt
          p-fn-cnt
          (access fc-derivation (car lst) :ttree))
        (fcd-worse-than-or-equal-lst concl
          fn-cnt
          p-fn-cnt
          (cdr lst))))))

(defun exists-fcd-worse-than-or-equal
  (fcd-lst concl fn-cnt p-fn-cnt)
  (cond ((null fcd-lst) nil)
    (t (or (and (let ((fcd-fn-cnt (access fc-derivation (car fcd-lst) :fn-cnt)))
            (or (> fcd-fn-cnt fn-cnt)
              (and (eql fcd-fn-cnt fn-cnt)
                (>= (access fc-derivation (car fcd-lst) :p-fn-cnt) p-fn-cnt))))
          (worse-than-or-equal (access fc-derivation (car fcd-lst) :concl)
            concl))
        (exists-fcd-worse-than-or-equal (cdr fcd-lst)
          concl
          fn-cnt
          p-fn-cnt)))))

(defun all-dumb-occur-lst
  (args cl)
  (cond ((endp args) t)
    (t (and (dumb-occur-lst (car args) cl)
        (all-dumb-occur-lst (cdr args) cl)))))

(defun all-args-occur-after-strip-not
  (term cl)
  (cond ((variablep term) t)
    ((fquotep term) nil)
    ((eq (ffn-symb term) 'not) (all-args-occur-after-strip-not (fargn term 1) cl))
    (t (all-dumb-occur-lst (fargs term) cl))))

(defun approved-fc-derivationp
  (fcd cl)
  (let ((ttree (access fc-derivation fcd :ttree)))
    (or (not (fcd-runep (access fc-derivation fcd :rune) ttree))
      (not (fcd-worse-than-or-equal (access fc-derivation fcd :concl)
          (access fc-derivation fcd :fn-cnt)
          (access fc-derivation fcd :p-fn-cnt)
          ttree))
      (all-args-occur-after-strip-not (access fc-derivation fcd :concl)
        cl))))

(defun approve-fc-derivations
  (new-fcd-lst cl approved-this-round all-approved)
  (cond ((null new-fcd-lst) (mv approved-this-round all-approved))
    ((approved-fc-derivationp (car new-fcd-lst) cl) (approve-fc-derivations (cdr new-fcd-lst)
        cl
        (cons (car new-fcd-lst) approved-this-round)
        (cons (car new-fcd-lst) all-approved)))
    (t (approve-fc-derivations (cdr new-fcd-lst)
        cl
        approved-this-round
        all-approved))))

(defun sort-fcds1-rating
  (term wrld)
  (mv-let (fc vc)
    (sort-fcds1-rating1 term wrld 0 0)
    (- (+ (* 10 fc) vc))))

(defun sort-fcds1
  (approved wrld)
  (cond ((null approved) nil)
    (t (cons (cons (sort-fcds1-rating (access fc-derivation (car approved) :concl)
            wrld)
          (car approved))
        (sort-fcds1 (cdr approved) wrld)))))

(defun sort-fcds
  (fcd-lst wrld)
  (strip-cdrs (merge-sort-car-> (sort-fcds1 fcd-lst wrld))))

(defun strip-fcd-concls
  (fcd-lst)
  (cond ((null fcd-lst) nil)
    (t (cons (access fc-derivation (car fcd-lst) :concl)
        (strip-fcd-concls (cdr fcd-lst))))))

(defun type-alist-fcd-lst
  (fcd-lst type-alist do-not-reconsiderp force-flg ens wrld)
  (cond ((endp fcd-lst) (if do-not-reconsiderp
        (mv nil type-alist)
        (mv-let (contradictionp xtype-alist ttree)
          (reconsider-type-alist type-alist
            type-alist
            nil
            ens
            wrld
            nil
            nil)
          (cond (contradictionp (mv t ttree))
            (t (mv nil xtype-alist))))))
    (t (mv-let (mbt mbf tta fta ttree)
        (assume-true-false (access fc-derivation (car fcd-lst) :concl)
          (add-to-tag-tree! 'fc-derivation (car fcd-lst) nil)
          force-flg
          nil
          type-alist
          ens
          wrld
          nil
          nil
          :fta)
        (declare (ignore fta))
        (cond (mbf (mv t ttree))
          (mbt (type-alist-fcd-lst (cdr fcd-lst)
              type-alist
              do-not-reconsiderp
              force-flg
              ens
              wrld))
          (t (type-alist-fcd-lst (cdr fcd-lst)
              tta
              do-not-reconsiderp
              force-flg
              ens
              wrld)))))))

(defun every-concl-member-equalp
  (fcd-lst trigger-terms)
  (cond ((endp fcd-lst) t)
    ((member-equal (access fc-derivation (car fcd-lst) :concl)
       trigger-terms) (every-concl-member-equalp (cdr fcd-lst) trigger-terms))
    (t nil)))

(defun collect-disjuncts
  (term top-level)
  (case-match term
    (('if p p q) (cons p (collect-disjuncts q nil)))
    (('if p *t* q) (cons p (collect-disjuncts q nil)))
    (('if p q *t*) (cons (dumb-negate-lit p) (collect-disjuncts q nil)))
    (& (and (not top-level) (list term)))))

(defun collect-disjunction-triples
  (fcd-lst triples)
  (cond ((endp fcd-lst) triples)
    (t (let* ((fcd (car fcd-lst)) (concl (access fc-derivation (car fcd-lst) :concl))
          (disjuncts (collect-disjuncts concl t)))
        (cond (disjuncts (collect-disjunction-triples (cdr fcd-lst)
              (cons (list* disjuncts (access fc-derivation fcd :ttree) fcd)
                triples)))
          (t (collect-disjunction-triples (cdr fcd-lst) triples)))))))

(defun exploit-disjunction-triple
  (clause ttree
    fcd
    type-alist
    ens
    wrld
    last-lit-kept
    kept-cnt
    lit-deletedp)
  (cond ((endp clause) (cond ((eql kept-cnt 0) (mv :contradiction ttree nil type-alist nil))
        ((eql kept-cnt 1) (mv-let (mbt mbf tta fta ttree1)
            (assume-true-false last-lit-kept
              ttree
              nil
              nil
              type-alist
              ens
              wrld
              nil
              nil
              :fta)
            (declare (ignore fta))
            (cond (mbf (mv :contradiction ttree1
                  nil
                  type-alist
                  (change fc-derivation fcd :concl last-lit-kept :ttree ttree)))
              (mbt (mv :delete nil nil type-alist nil))
              (t (mv :delete nil
                  nil
                  tta
                  (change fc-derivation fcd :concl last-lit-kept :ttree ttree))))))
        (lit-deletedp (mv :new ttree nil type-alist nil))
        (t (mv :unchanged nil nil type-alist nil))))
    (t (let ((lit (car clause)))
        (mv-let (ts ttree1)
          (type-set lit nil nil type-alist ens wrld ttree nil nil)
          (cond ((ts= ts *ts-nil*) (exploit-disjunction-triple (cdr clause)
                ttree1
                fcd
                type-alist
                ens
                wrld
                last-lit-kept
                kept-cnt
                t))
            ((ts-disjointp ts *ts-nil*) (mv :delete nil nil type-alist nil))
            (t (mv-let (signal new-ttree new-clause new-type-alist new-fcd)
                (exploit-disjunction-triple (cdr clause)
                  ttree
                  fcd
                  type-alist
                  ens
                  wrld
                  lit
                  (+ 1 kept-cnt)
                  lit-deletedp)
                (cond ((eq signal :new) (mv :new new-ttree (cons lit new-clause) new-type-alist nil))
                  (t (mv signal new-ttree new-clause new-type-alist new-fcd)))))))))))

(defun exploit-disjunction-triples1
  (disjunction-triples type-alist
    ens
    wrld
    new-approved-fcds
    all-approved-fcds)
  (cond ((endp disjunction-triples) (mv nil
        nil
        nil
        type-alist
        new-approved-fcds
        all-approved-fcds))
    (t (let ((clause (caar disjunction-triples)) (ttree (cadar disjunction-triples))
          (fcd (cddar disjunction-triples)))
        (mv-let (signal new-ttree new-clause new-type-alist new-fcd)
          (exploit-disjunction-triple clause
            ttree
            fcd
            type-alist
            ens
            wrld
            nil
            0
            nil)
          (let ((new-approved-fcds (if new-fcd
                 (cons new-fcd new-approved-fcds)
                 new-approved-fcds)) (all-approved-fcds (if new-fcd
                  (cons new-fcd all-approved-fcds)
                  all-approved-fcds)))
            (case signal
              (:contradiction (mv t new-ttree nil nil new-approved-fcds all-approved-fcds))
              (:delete (exploit-disjunction-triples1 (cdr disjunction-triples)
                  new-type-alist
                  ens
                  wrld
                  new-approved-fcds
                  all-approved-fcds))
              (otherwise (mv-let (contradictionp ttree
                    new-disjunction-triples
                    new-type-alist
                    new-approved-fcds
                    all-approved-fcds)
                  (exploit-disjunction-triples1 (cdr disjunction-triples)
                    new-type-alist
                    ens
                    wrld
                    new-approved-fcds
                    all-approved-fcds)
                  (cond (contradictionp (mv contradictionp
                        ttree
                        new-disjunction-triples
                        new-type-alist
                        new-approved-fcds
                        all-approved-fcds))
                    (t (mv nil
                        nil
                        (cons (if (eq signal :unchanged)
                            (car disjunction-triples)
                            (list* new-clause new-ttree fcd))
                          new-disjunction-triples)
                        new-type-alist
                        new-approved-fcds
                        all-approved-fcds))))))))))))

(defun exploit-disjunction-triples
  (disjunction-triples type-alist
    ens
    wrld
    new-approved-fcds
    all-approved-fcds)
  (mv-let (contradictionp ttree
      new-disjunction-triples
      new-type-alist
      new-approved-fcds
      all-approved-fcds)
    (exploit-disjunction-triples1 disjunction-triples
      type-alist
      ens
      wrld
      new-approved-fcds
      all-approved-fcds)
    (cond (contradictionp (mv contradictionp
          ttree
          new-disjunction-triples
          new-type-alist
          new-approved-fcds
          all-approved-fcds))
      ((and (equal new-disjunction-triples disjunction-triples)
         (equal new-type-alist type-alist)) (mv nil
          nil
          new-disjunction-triples
          new-type-alist
          new-approved-fcds
          all-approved-fcds))
      (t (exploit-disjunction-triples new-disjunction-triples
          new-type-alist
          ens
          wrld
          new-approved-fcds
          all-approved-fcds)))))

(defun process-disjunction-triples
  (approved-this-round disjunction-triples
    type-alist
    ens
    wrld
    new-approved-fcds
    all-approved-fcds)
  (exploit-disjunction-triples (collect-disjunction-triples approved-this-round
      disjunction-triples)
    type-alist
    ens
    wrld
    new-approved-fcds
    all-approved-fcds))

(defun concls-from-fcds
  (fcd-lst)
  (cond ((endp fcd-lst) nil)
    (t (cons (access fc-derivation (car fcd-lst) :concl)
        (concls-from-fcds (cdr fcd-lst))))))

(defun strip-ttrees-from-type-alist
  (ta)
  (cond ((endp ta) nil)
    (t (cons (list (caar ta) (decode-type-set (cadar ta)))
        (strip-ttrees-from-type-alist (cdr ta))))))

(defun cw-round-by-round-fn
  (fc-round fcds1
    type-alist1
    contrap1
    fcds2
    type-alist2
    contrap2)
  (cw "(Round ~x0:~%~
       ~ (new conclusions:~%  ~Y12)~%~
       ~ (new type-alist:~%  ~Y32)~%~
       ~ (disjuncts dislodged:~%  ~Y42)~%~
       ~ (final type-alist:~%  ~Y52)~%~
       ~ )~%"
    fc-round
    (concls-from-fcds fcds1)
    nil
    (if contrap1
      'contradiction!
      (cons 'make-type-alist
        (strip-ttrees-from-type-alist type-alist1)))
    (concls-from-fcds fcds2)
    (if contrap2
      'contradiction!
      (cons 'make-type-alist
        (strip-ttrees-from-type-alist type-alist2)))))

(defun forward-chain1
  (cl fc-round
    trigger-terms
    activations
    disjunction-triples
    type-alist
    force-flg
    wrld
    do-not-reconsiderp
    ens
    oncep-override
    state
    all-approved-fcds)
  (mv-let (activations1 fcd-lst1)
    (advance-fc-activations activations
      fc-round
      type-alist
      ens
      force-flg
      wrld
      state
      oncep-override
      nil
      nil)
    (prog2$ (filter-all-satisfying-fc-derivations fcd-lst1)
      (mv-let (new-approved-fcds all-approved-fcds)
        (approve-fc-derivations fcd-lst1 cl nil all-approved-fcds)
        (let ((sorted-fcds (sort-fcds new-approved-fcds wrld)))
          (mv-let (contradictionp x)
            (type-alist-fcd-lst sorted-fcds
              type-alist
              do-not-reconsiderp
              force-flg
              ens
              wrld)
            (cond (contradictionp (cw-round-by-round nil
                  fc-round
                  sorted-fcds
                  nil
                  t
                  nil
                  nil
                  nil
                  (mv t x all-approved-fcds fc-round activations1)))
              (t (mv-let (contradictionp ttree
                    new-disjunction-triples
                    new-type-alist
                    new-approved-fcds1
                    all-approved-fcds)
                  (process-disjunction-triples new-approved-fcds
                    disjunction-triples
                    x
                    ens
                    wrld
                    new-approved-fcds
                    all-approved-fcds)
                  (cw-round-by-round nil
                    fc-round
                    sorted-fcds
                    x
                    nil
                    (set-difference-equal new-approved-fcds1 new-approved-fcds)
                    new-type-alist
                    contradictionp
                    (cond (contradictionp (mv t ttree all-approved-fcds fc-round activations1))
                      ((and (equal new-type-alist type-alist)
                         (every-concl-member-equalp new-approved-fcds1 trigger-terms)) (mv nil nil all-approved-fcds fc-round activations1))
                      (t (mv-let (trigger-terms1 activations1)
                          (collect-terms-and-activations-from-fcd-lst new-approved-fcds1
                            wrld
                            ens
                            trigger-terms
                            activations1)
                          (forward-chain1 cl
                            (+ 1 fc-round)
                            trigger-terms1
                            activations1
                            new-disjunction-triples
                            new-type-alist
                            force-flg
                            wrld
                            do-not-reconsiderp
                            ens
                            oncep-override
                            state
                            all-approved-fcds))))))))))))))

(defun forward-chain-top
  (caller cl
    pts
    force-flg
    do-not-reconsiderp
    wrld
    ens
    oncep-override
    state)
  (prog2$ (new-fc-call caller
      cl
      pts
      force-flg
      do-not-reconsiderp
      wrld
      ens
      oncep-override)
    (mv-let (contradictionp type-alist ttree1)
      (mv-let (cl-sorted ttree-lst)
        (if (eq caller 'simplify-clause-settled-down)
          (sort-lits cl (pts-to-ttree-lst pts))
          (mv cl (pts-to-ttree-lst pts)))
        (type-alist-clause cl-sorted
          ttree-lst
          nil
          nil
          ens
          wrld
          nil
          nil))
      (cond (contradictionp (mv t nil ttree1))
        (t (mv-let (trigger-terms activations)
            (collect-terms-and-activations-lst cl nil wrld ens nil nil)
            (mv-let (contradictionp ttree2
                all-approved-fcds
                rounds
                activations1)
              (pstk (forward-chain1 cl
                  1
                  trigger-terms
                  activations
                  nil
                  type-alist
                  force-flg
                  wrld
                  do-not-reconsiderp
                  ens
                  oncep-override
                  state
                  nil))
              (cond (contradictionp (fc-exit t
                    nil
                    (expunge-fc-derivations ttree2)
                    caller
                    rounds
                    all-approved-fcds
                    activations1))
                (t (let ((fc-pair-lst (fc-pair-lst all-approved-fcds)))
                    (mv-let (contradictionp type-alist3 ttree3)
                      (fc-pair-lst-type-alist fc-pair-lst
                        all-approved-fcds
                        type-alist
                        force-flg
                        ens
                        wrld)
                      (cond (contradictionp (fc-exit t
                            nil
                            ttree3
                            caller
                            rounds
                            all-approved-fcds
                            activations1))
                        (t (mv-let (contradictionp type-alist4 ttree4)
                            (type-alist-equality-loop type-alist3
                              ens
                              wrld
                              *type-alist-equality-loop-max-depth*)
                            (cond (contradictionp (fc-exit t
                                  nil
                                  ttree4
                                  caller
                                  rounds
                                  all-approved-fcds
                                  activations1))
                              (t (fc-exit nil
                                  type-alist4
                                  fc-pair-lst
                                  caller
                                  rounds
                                  all-approved-fcds
                                  activations1)))))))))))))))))

(defun forward-chain
  (cl pts
    force-flg
    do-not-reconsiderp
    wrld
    ens
    oncep-override
    state)
  (forward-chain-top 'miscellaneous
    cl
    pts
    force-flg
    do-not-reconsiderp
    wrld
    ens
    oncep-override
    state))

(defun select-forward-chained-concls-and-ttrees
  (fc-pair-lst pt lits ttree-lst)
  (cond ((null fc-pair-lst) (mv lits ttree-lst))
    ((to-be-ignoredp (cdr (car fc-pair-lst)) pt) (select-forward-chained-concls-and-ttrees (cdr fc-pair-lst)
        pt
        lits
        ttree-lst))
    (t (select-forward-chained-concls-and-ttrees (cdr fc-pair-lst)
        pt
        (cons (dumb-negate-lit (car (car fc-pair-lst))) lits)
        (cons (cdr (car fc-pair-lst)) ttree-lst)))))

(defun rewrite-clause-type-alist
  (tail new-clause fc-pair-lst rcnst wrld pot-lst)
  (let ((pt (access rewrite-constant rcnst :pt)))
    (mv-let (lits ttree-lst)
      (select-forward-chained-concls-and-ttrees fc-pair-lst
        pt
        nil
        nil)
      (mv-let (current-clause current-ttree-lst)
        (mv (append new-clause (cdr tail) lits)
          (make-list-ac (+ (len new-clause) (len (cdr tail)))
            nil
            ttree-lst))
        (mv-let (contradictionp type-alist ttree)
          (type-alist-clause current-clause
            current-ttree-lst
            nil
            nil
            (access rewrite-constant rcnst :current-enabled-structure)
            wrld
            pot-lst
            pt)
          (mv contradictionp type-alist ttree current-clause))))))

(defun maximal-multiples1
  (term-lst new-vars avoid-vars pkg-witness)
  (let ((e (maximal-multiple-lst term-lst term-lst nil)))
    (cond ((equal e nil) (mv new-vars term-lst))
      (t (let ((var (genvar pkg-witness "V" (+ 1 (len new-vars)) avoid-vars)))
          (maximal-multiples1 (cons e (subst-expr1-lst var e term-lst))
            (cons var new-vars)
            (cons var avoid-vars)
            pkg-witness))))))

(defun maximal-multiples
  (term pkg-witness)
  (maximal-multiples1 (list term)
    nil
    (all-vars term)
    pkg-witness))

(defun mutually-exclusive-tests
  (a b)
  (and (ffn-symb-p a 'equal)
    (ffn-symb-p b 'equal)
    (or (and (quotep (fargn a 1))
        (quotep (fargn b 1))
        (not (equal (cadr (fargn a 1)) (cadr (fargn b 1))))
        (equal (fargn a 2) (fargn b 2)))
      (and (quotep (fargn a 2))
        (quotep (fargn b 2))
        (not (equal (cadr (fargn a 2)) (cadr (fargn b 2))))
        (equal (fargn a 1) (fargn b 1)))
      (and (quotep (fargn a 1))
        (quotep (fargn b 2))
        (not (equal (cadr (fargn a 1)) (cadr (fargn b 2))))
        (equal (fargn a 2) (fargn b 1)))
      (and (quotep (fargn a 2))
        (quotep (fargn b 1))
        (not (equal (cadr (fargn a 2)) (cadr (fargn b 1))))
        (equal (fargn a 1) (fargn b 2))))))

(defun mutually-exclusive-subsumptionp
  (a b c)
  (cond ((equal b c) t)
    ((and (ffn-symb-p c 'if)
       (mutually-exclusive-tests a (fargn c 1))) (mutually-exclusive-subsumptionp a b (fargn c 3)))
    (t nil)))

(defun all-type-reasoning-tags-p1
  (lemmas)
  (cond ((endp lemmas) t)
    ((or (eq (car (car lemmas)) :fake-rune-for-type-set)
       (eq (car (car lemmas)) :type-prescription)) (all-type-reasoning-tags-p1 (cdr lemmas)))
    (t nil)))

(defun all-type-reasoning-tags-p
  (ttree)
  (all-type-reasoning-tags-p1 (tagged-objects 'lemma ttree)))

(defun try-clause
  (atm clause wrld)
  (cond ((endp clause) nil)
    ((and (eq (fn-symb (car clause)) 'not)
       (equal-mod-commuting atm (fargn (car clause) 1) wrld)) t)
    ((equal-mod-commuting atm (car clause) wrld) t)
    (t (try-clause atm (cdr clause) wrld))))

(defun make-non-nil-ttree
  (ttree)
  (or ttree *trivial-non-nil-ttree*))

(defun try-type-set-and-clause
  (atm ans
    ttree
    ttree0
    current-clause
    wrld
    ens
    knownp
    knownp-ttree)
  (mv-let (ts ttree1)
    (type-set atm nil nil nil ens wrld nil nil nil)
    (cond ((ts= ts *ts-nil*) (mv *nil* (cons-tag-trees ttree1 ttree0) nil))
      ((ts-subsetp ts *ts-non-nil*) (mv *t* (cons-tag-trees ttree1 ttree0) nil))
      ((try-clause atm current-clause wrld) (mv ans ttree nil))
      (t (mv atm
          ttree0
          (and knownp (or knownp-ttree (make-non-nil-ttree ttree))))))))

(defun rewrite-atm
  (atm not-flg
    bkptr
    gstack
    type-alist
    wrld
    simplify-clause-pot-lst
    rcnst
    current-clause
    state
    step-limit
    ttree0)
  (mv-let (knownp nilp knownp-ttree)
    (known-whether-nil atm
      type-alist
      (access rewrite-constant rcnst :current-enabled-structure)
      (ok-to-force rcnst)
      t
      wrld
      ttree0)
    (cond ((and knownp not-flg nilp) (mv step-limit *nil* knownp-ttree nil))
      ((and knownp (not not-flg) (not nilp)) (mv step-limit *t* knownp-ttree nil))
      (t (let ((lemmas0 (tagged-objects 'lemma ttree0)) (ttree00 (remove-tag-from-tag-tree 'lemma ttree0)))
          (sl-let (ans1 ans2)
            (rewrite-entry (rewrite atm nil bkptr)
              :rdepth (rewrite-stack-limit wrld)
              :step-limit step-limit
              :type-alist type-alist
              :obj '?
              :geneqv *geneqv-iff*
              :pequiv-info nil
              :wrld wrld
              :fnstack nil
              :ancestors nil
              :backchain-limit (access rewrite-constant rcnst :backchain-limit-rw)
              :simplify-clause-pot-lst simplify-clause-pot-lst
              :rcnst rcnst
              :gstack gstack
              :ttree ttree00)
            (let* ((old-lemmas lemmas0) (new-lemmas (tagged-objects 'lemma ans2))
                (final-lemmas (if old-lemmas
                    (union-equal new-lemmas old-lemmas)
                    new-lemmas))
                (ttree (maybe-extend-tag-tree 'lemma
                    final-lemmas
                    (remove-tag-from-tag-tree 'lemma ans2))))
              (cond ((not (or (equal ans1 *nil*) (equal ans1 *t*))) (mv step-limit ans1 ttree (and knownp knownp-ttree)))
                ((and (nvariablep atm)
                   (not (fquotep atm))
                   (equivalence-relationp (ffn-symb atm) wrld)) (mv step-limit ans1 ttree nil))
                ((equal ans1
                   (if not-flg
                     *nil*
                     *t*)) (mv step-limit ans1 ttree nil))
                ((all-type-reasoning-tags-p ans2) (cond ((lambda-subtermp atm) (mv step-limit ans1 ttree nil))
                    ((eq (fn-symb atm) 'implies) (prepend-step-limit 3
                        (try-type-set-and-clause (subcor-var (formals 'implies wrld)
                            (list (fargn atm 1) (fargn atm 2))
                            (bbody 'implies))
                          ans1
                          ttree
                          ttree0
                          current-clause
                          wrld
                          (access rewrite-constant rcnst :current-enabled-structure)
                          knownp
                          knownp-ttree)))
                    (t (prepend-step-limit 3
                        (try-type-set-and-clause atm
                          ans1
                          ttree
                          ttree0
                          current-clause
                          wrld
                          (access rewrite-constant rcnst :current-enabled-structure)
                          knownp
                          knownp-ttree)))))
                (t (mv step-limit ans1 ttree nil))))))))))

(defun every-occurrence-equiv-hittablep
  (equiv old geneqv term ens wrld)
  (cond ((and (nvariablep old) (fquotep old)) (subst-expr-error old))
    ((eq equiv 'equal) t)
    (t (every-occurrence-equiv-hittablep1 equiv
        old
        geneqv
        term
        nil
        ens
        wrld))))

(defun every-occurrence-equiv-hittablep-in-clausep
  (equiv old cl ens wrld)
  (cond ((null cl) t)
    (t (and (every-occurrence-equiv-hittablep1 equiv
          old
          *geneqv-iff*
          (car cl)
          nil
          ens
          wrld)
        (every-occurrence-equiv-hittablep-in-clausep equiv
          old
          (cdr cl)
          ens
          wrld)))))

(defun some-occurrence-equiv-hittablep
  (equiv old geneqv term ens wrld)
  (cond ((and (nvariablep old) (fquotep old)) (subst-expr-error old))
    (t (some-occurrence-equiv-hittablep1 equiv
        old
        geneqv
        term
        ens
        wrld))))

(defun equiv-hittable-in-some-other-lit
  (equiv term n cl i ens wrld)
  (cond ((null cl) nil)
    ((int= n i) (equiv-hittable-in-some-other-lit equiv
        term
        n
        (cdr cl)
        (1+ i)
        ens
        wrld))
    ((some-occurrence-equiv-hittablep equiv
       term
       *geneqv-iff*
       (car cl)
       ens
       wrld) t)
    (t (equiv-hittable-in-some-other-lit equiv
        term
        n
        (cdr cl)
        (1+ i)
        ens
        wrld))))

(defun find-trivial-equivalence1
  (not-just-quotep-flg tail i cl ens wrld avoid-lst)
  (cond ((null tail) (mv nil nil nil nil nil nil))
    ((member-equal (car tail) avoid-lst) (find-trivial-equivalence1 not-just-quotep-flg
        (cdr tail)
        (1+ i)
        cl
        ens
        wrld
        avoid-lst))
    ((quotep (car tail)) (if (equal (car tail) *nil*)
        (find-trivial-equivalence1 not-just-quotep-flg
          (cdr tail)
          (1+ i)
          cl
          ens
          wrld
          avoid-lst)
        (mv nil nil nil nil nil nil)))
    ((or (variablep (car tail))
       (and (eq (ffn-symb (car tail)) 'not)
         (or (variablep (fargn (car tail) 1))
           (and (not (fquotep (fargn (car tail) 1)))
             (equivalence-relationp (ffn-symb (fargn (car tail) 1)) wrld))))) (let* ((atm (if (variablep (car tail))
             (fcons-term* 'equal (car tail) *nil*)
             (fargn (car tail) 1))) (equiv (if (variablep atm)
              'iff
              (ffn-symb atm)))
          (lhs (if (variablep atm)
              atm
              (fargn atm 1)))
          (rhs (if (variablep atm)
              *t*
              (fargn atm 2))))
        (cond ((and (quotep lhs) (quotep rhs)) (cond ((eq equiv 'equal) (if (equal lhs rhs)
                  (find-trivial-equivalence1 not-just-quotep-flg
                    (cdr tail)
                    (1+ i)
                    cl
                    ens
                    wrld
                    avoid-lst)
                  (mv nil nil nil nil nil nil)))
              (t (find-trivial-equivalence1 not-just-quotep-flg
                  (cdr tail)
                  (1+ i)
                  cl
                  ens
                  wrld
                  avoid-lst))))
          ((and not-just-quotep-flg
             (variablep lhs)
             (every-occurrence-equiv-hittablep-in-clausep equiv
               lhs
               cl
               ens
               wrld)
             (not (dumb-occur lhs rhs))) (cond ((and (variablep rhs)
                 (every-occurrence-equiv-hittablep-in-clausep equiv
                   rhs
                   cl
                   ens
                   wrld)) (cond ((term-order lhs rhs) (mv 'disposable i equiv rhs lhs (car tail)))
                  (t (mv 'disposable i equiv lhs rhs (car tail)))))
              (t (mv 'disposable i equiv lhs rhs (car tail)))))
          ((and not-just-quotep-flg
             (variablep rhs)
             (every-occurrence-equiv-hittablep-in-clausep equiv
               rhs
               cl
               ens
               wrld)
             (not (dumb-occur rhs lhs))) (mv 'disposable i equiv rhs lhs (car tail)))
          ((and (quotep rhs)
             (equiv-hittable-in-some-other-lit equiv lhs i cl 0 ens wrld)) (mv 'keeper i equiv lhs rhs (car tail)))
          ((and (quotep lhs)
             (equiv-hittable-in-some-other-lit equiv rhs i cl 0 ens wrld)) (mv 'keeper i equiv rhs lhs (car tail)))
          (t (find-trivial-equivalence1 not-just-quotep-flg
              (cdr tail)
              (1+ i)
              cl
              ens
              wrld
              avoid-lst)))))
    (t (find-trivial-equivalence1 not-just-quotep-flg
        (cdr tail)
        (1+ i)
        cl
        ens
        wrld
        avoid-lst))))

(defun find-trivial-equivalence
  (not-just-quotep-flg cl ens wrld avoid-lst)
  (find-trivial-equivalence1 not-just-quotep-flg
    cl
    0
    cl
    ens
    wrld
    avoid-lst))

(defun add-literal-and-pt1
  (cl-tail pt cl pt-lst)
  (cond ((null cl) (er hard
        'add-literal-and-pt1
        "We failed to find the literal!"))
    ((equal cl-tail cl) (cond ((null (car pt-lst)) (cons pt (cdr pt-lst)))
        (t (cons (cons pt (car pt-lst)) (cdr pt-lst)))))
    (t (cons (car pt-lst)
        (add-literal-and-pt1 cl-tail pt (cdr cl) (cdr pt-lst))))))

(defun add-literal-and-pt
  (lit pt cl pt-lst ttree)
  (cond ((quotep lit) (cond ((equal lit *nil*) (mv cl pt-lst ttree))
        (t (mv *true-clause* nil ttree))))
    ((or (equal cl *true-clause*)
       (member-complement-term lit cl)) (mv *true-clause* nil ttree))
    (t (let ((cl0 (member-term lit cl)))
        (cond ((null cl0) (mv (cons lit cl) (cons pt pt-lst) ttree))
          ((null pt) (mv cl pt-lst ttree))
          (t (mv cl (add-literal-and-pt1 cl0 pt cl pt-lst) ttree)))))))

(defun add-binding-to-tag-tree
  (var term ttree)
  (let* ((tag 'binding-lst) (binding (cons var term))
      (old (tagged-object tag ttree)))
    (cond (old (extend-tag-tree tag
          (list (cons binding old))
          (remove-tag-from-tag-tree! tag ttree)))
      (t (extend-tag-tree tag (list (cons binding nil)) ttree)))))

(defun subst-equiv-and-maybe-delete-lit
  (equiv new
    old
    n
    cl
    i
    pt-lst
    delete-flg
    ens
    wrld
    state
    ttree)
  (cond ((null cl) (mv nil nil ttree))
    ((int= n i) (mv-let (cl1 pt-lst1 ttree)
        (subst-equiv-and-maybe-delete-lit equiv
          new
          old
          n
          (cdr cl)
          (1+ i)
          (cdr pt-lst)
          delete-flg
          ens
          wrld
          state
          ttree)
        (cond (delete-flg (mv cl1 pt-lst1 (add-binding-to-tag-tree old new ttree)))
          (t (add-literal-and-pt (car cl) (car pt-lst) cl1 pt-lst1 ttree)))))
    ((dumb-occur old (car cl)) (mv-let (hitp lit ttree)
        (subst-equiv-expr equiv
          new
          old
          *geneqv-iff*
          (car cl)
          ens
          wrld
          state
          ttree)
        (declare (ignore hitp))
        (mv-let (cl1 pt-lst1 ttree)
          (subst-equiv-and-maybe-delete-lit equiv
            new
            old
            n
            (cdr cl)
            (1+ i)
            (cdr pt-lst)
            delete-flg
            ens
            wrld
            state
            ttree)
          (add-literal-and-pt lit (car pt-lst) cl1 pt-lst1 ttree))))
    (t (mv-let (cl1 pt-lst1 ttree)
        (subst-equiv-and-maybe-delete-lit equiv
          new
          old
          n
          (cdr cl)
          (1+ i)
          (cdr pt-lst)
          delete-flg
          ens
          wrld
          state
          ttree)
        (add-literal-and-pt (car cl) (car pt-lst) cl1 pt-lst1 ttree)))))

(defun remove-trivial-equivalences-rec
  (cl pt-lst remove-flg ens wrld state ttree hitp avoid-lst)
  (mv-let (condition lit-position equiv lhs rhs lit)
    (find-trivial-equivalence remove-flg cl ens wrld avoid-lst)
    (cond (lit-position (mv-let (new-cl new-pt-lst ttree)
          (subst-equiv-and-maybe-delete-lit equiv
            rhs
            lhs
            lit-position
            cl
            0
            pt-lst
            (and remove-flg (eq condition 'disposable))
            ens
            wrld
            state
            ttree)
          (remove-trivial-equivalences-rec new-cl
            new-pt-lst
            remove-flg
            ens
            wrld
            state
            ttree
            t
            (cons lit avoid-lst))))
      (t (mv hitp cl pt-lst ttree)))))

(defun remove-trivial-equivalences
  (cl pt-lst remove-flg ens wrld state ttree)
  (cond ((remove-trivial-equivalences-enabled-p) (remove-trivial-equivalences-rec cl
        pt-lst
        remove-flg
        ens
        wrld
        state
        ttree
        nil
        nil))
    (t (mv nil cl pt-lst ttree))))

(defun built-in-clausep2
  (bic-lst cl fns ens)
  (cond ((null bic-lst) nil)
    ((and (let ((nume (access built-in-clause (car bic-lst) :nume)))
         (if (null ens)
           (null nume)
           (enabled-numep nume ens)))
       (subsetp-eq (access built-in-clause (car bic-lst) :all-fnnames)
         fns)
       (eq (subsumes *init-subsumes-count*
           (access built-in-clause (car bic-lst) :clause)
           cl
           nil)
         t)) (access built-in-clause (car bic-lst) :rune))
    (t (built-in-clausep2 (cdr bic-lst) cl fns ens))))

(defun built-in-clausep1
  (bic-alist cl fns ens)
  (cond ((null bic-alist) nil)
    ((or (null (caar bic-alist))
       (member-eq (caar bic-alist) fns)) (or (built-in-clausep2 (cdr (car bic-alist)) cl fns ens)
        (built-in-clausep1 (cdr bic-alist) cl fns ens)))
    (t (built-in-clausep1 (cdr bic-alist) cl fns ens))))

(defun possible-trivial-clause-p
  (cl)
  (if (null cl)
    nil
    (mv-let (not-flg atm)
      (strip-not (car cl))
      (declare (ignore not-flg))
      (or (ffnnamesp '(if not
            iff
            implies
            eq
            atom
            eql
            =
            /=
            null
            zerop
            plusp
            minusp
            listp
            mv-list
            cons-with-hint
            return-last
            wormhole-eval
            force
            case-split
            double-rewrite)
          atm)
        (possible-trivial-clause-p (cdr cl))))))

(defun trivial-clause-p
  (cl wrld)
  (or (member-equal *t* cl)
    (and (possible-trivial-clause-p cl)
      (tautologyp (disjoin cl) wrld))))

(defun built-in-clausep
  (caller cl ens match-free-override wrld state)
  (let ((rune (built-in-clausep1 (global-val 'built-in-clauses wrld)
         cl
         (all-fnnames-lst cl)
         ens)))
    (cond (rune (mv t (push-lemma rune nil)))
      ((null ens) (cond ((trivial-clause-p cl wrld) (mv t nil))
          (t (mv nil nil))))
      (t (mv-let (contradictionp type-alist ttree)
          (forward-chain-top caller
            cl
            nil
            nil
            nil
            wrld
            ens
            match-free-override
            state)
          (declare (ignore type-alist))
          (cond ((not contradictionp) (cond ((trivial-clause-p cl wrld) (mv t nil))
                (t (mv nil nil))))
            ((tagged-objectsp 'assumption ttree) (mv (er hard
                  'built-in-clausep
                  "It was thought that the forward-chain call in ~
                                this function could not produce an ~
                                'assumption but it did!  Try running ~
                                forward-chain on ~X01 with ~
                                match-free-override = ~x2.  The ens and wrld ~
                                used here must be recovered by other means if ~
                                (ens state) and (w state) don't work."
                  (kwote cl)
                  nil
                  (kwote match-free-override))
                nil))
            (t (mv t ttree))))))))

(defun crunch-clause-segments1
  (seg1 pts1 cl pts)
  (cond ((null seg1) (mv cl pts))
    (t (mv-let (cl pts ttree)
        (add-literal-and-pt (car seg1) (car pts1) cl pts nil)
        (declare (ignore ttree))
        (crunch-clause-segments1 (cdr seg1) (cdr pts1) cl pts)))))

(defun crunch-clause-segments2
  (cl pts seg1 pts1)
  (cond ((null cl) (mv seg1 pts1 nil))
    ((and (consp (car cl))
       (eq (ffn-symb (car cl)) 'car)
       (eq (fargn (car cl) 1) :crunch-clause-segments-marker)) (mv seg1 pts1 (cdr cl)))
    (t (crunch-clause-segments2 (cdr cl)
        (cdr pts)
        (cons (car cl) seg1)
        (cons (car pts) pts1)))))

(defun crunch-clause-segments
  (seg1 pts1 seg2 ens wrld state ttree)
  (let ((marker '(car :crunch-clause-segments-marker)))
    (mv-let (cl pts)
      (crunch-clause-segments1 seg1 pts1 (cons marker seg2) nil)
      (mv-let (hitp cl pts ttree)
        (remove-trivial-equivalences cl
          pts
          nil
          ens
          wrld
          state
          ttree)
        (cond ((null hitp) (mv seg1 pts1 seg2 ttree))
          (t (mv-let (seg1 pts1 seg2)
              (crunch-clause-segments2 cl pts nil nil)
              (mv seg1 pts1 seg2 ttree))))))))

(defun strip-non-rewrittenp-assumptions1
  (recs acc)
  (cond ((endp recs) (mv nil acc))
    (t (mv-let (rest acc)
        (strip-non-rewrittenp-assumptions1 (cdr recs) acc)
        (cond ((access assumption (car recs) :rewrittenp) (cond (acc (mv (cons (car recs) rest) acc))
              (t (mv recs nil))))
          (t (mv rest (cons (car recs) acc))))))))

(defun strip-non-rewrittenp-assumptions
  (ttree)
  (let ((recs (tagged-objects 'assumption ttree)))
    (cond (recs (let ((ttree0 (remove-tag-from-tag-tree! 'assumption ttree)))
          (mv-let (rewritten unrewritten)
            (strip-non-rewrittenp-assumptions1 recs nil)
            (mv (cond (rewritten (extend-tag-tree 'assumption rewritten ttree0))
                (t ttree0))
              unrewritten))))
      (t (mv ttree nil)))))

(defun assumnote-list-to-token-list
  (assumnote-list)
  (if (null assumnote-list)
    nil
    (cons (access assumnote (car assumnote-list) :rune)
      (assumnote-list-to-token-list (cdr assumnote-list)))))

(defun resume-suspended-assumption-rewriting1
  (assumptions ancestors
    gstack
    simplify-clause-pot-lst
    rcnst
    wrld
    state
    step-limit
    ttree)
  (cond ((endp assumptions) (mv step-limit nil ttree))
    (t (let* ((assn (car assumptions)) (term (access assumption assn :term)))
        (mv-let (on-ancestorsp assumed-true)
          (ancestors-check term
            ancestors
            (assumnote-list-to-token-list (access assumption assn :assumnotes)))
          (cond (on-ancestorsp (resume-suspended-assumption-rewriting1 (cdr assumptions)
                ancestors
                gstack
                simplify-clause-pot-lst
                rcnst
                wrld
                state
                step-limit
                (if assumed-true
                  ttree
                  (add-to-tag-tree 'assumption
                    (change assumption assn :rewrittenp term)
                    ttree))))
            (t (let ((new-ancestors (push-ancestor (dumb-negate-lit term)
                     (assumnote-list-to-token-list (access assumption assn :assumnotes))
                     ancestors
                     nil)))
                (mv-let (not-flg atm)
                  (strip-not term)
                  (sl-let (val ttree1)
                    (rewrite-entry (rewrite atm nil 'forced-assumption)
                      :rdepth (rewrite-stack-limit wrld)
                      :step-limit step-limit
                      :type-alist (access assumption assn :type-alist)
                      :obj '?
                      :geneqv *geneqv-iff*
                      :pequiv-info nil
                      :wrld wrld
                      :fnstack nil
                      :ancestors new-ancestors
                      :backchain-limit (access rewrite-constant rcnst :backchain-limit-rw)
                      :simplify-clause-pot-lst simplify-clause-pot-lst
                      :rcnst rcnst
                      :gstack gstack
                      :ttree nil)
                    (let ((val (if not-flg
                           (dumb-negate-lit val)
                           val)))
                      (cond ((equal val *nil*) (mv step-limit assn (cons-tag-trees ttree1 ttree)))
                        (t (mv-let (ttree1 assumptions1)
                            (strip-non-rewrittenp-assumptions ttree1)
                            (sl-let (bad-ass ttree)
                              (resume-suspended-assumption-rewriting1 assumptions1
                                new-ancestors
                                gstack
                                simplify-clause-pot-lst
                                rcnst
                                wrld
                                state
                                step-limit
                                (cons-tag-trees ttree1
                                  (if (equal val *t*)
                                    ttree
                                    (add-to-tag-tree 'assumption
                                      (change assumption assn :term val :rewrittenp term)
                                      ttree))))
                              (cond (bad-ass (mv step-limit bad-ass ttree))
                                (t (resume-suspended-assumption-rewriting1 (cdr assumptions)
                                    ancestors
                                    gstack
                                    simplify-clause-pot-lst
                                    rcnst
                                    wrld
                                    state
                                    step-limit
                                    ttree))))))))))))))))))

(defun resume-suspended-assumption-rewriting
  (ttree ancestors
    gstack
    simplify-clause-pot-lst
    rcnst
    wrld
    state
    step-limit)
  (mv-let (ttree assumptions)
    (strip-non-rewrittenp-assumptions ttree)
    (resume-suspended-assumption-rewriting1 assumptions
      ancestors
      gstack
      simplify-clause-pot-lst
      rcnst
      wrld
      state
      step-limit
      ttree)))

(defun helpful-little-ecnt-msg
  (case-limit ecnt)
  (cond ((and (null case-limit) (> ecnt 1000)) (prog2$ (cw "~%~%Helpful Little Message:  The simplifier is now expected to ~
          produce approximately ~n0 subgoals.  See :DOC ~
          case-split-limitations and see :DOC splitter.~%~%"
          ecnt)
        ecnt))
    (t ecnt)))

(defun setup-simplify-clause-pot-lst1
  (cl ttrees type-alist rcnst wrld state step-limit)
  (sl-let (contradictionp simplify-clause-pot-lst)
    (let ((gstack (initial-gstack 'setup-simplify-clause-pot-lst nil cl)))
      (rewrite-entry (add-terms-and-lemmas cl ttrees nil)
        :rdepth (rewrite-stack-limit wrld)
        :step-limit step-limit
        :type-alist type-alist
        :obj '?
        :geneqv nil
        :pequiv-info nil
        :wrld wrld
        :fnstack nil
        :ancestors nil
        :backchain-limit (access rewrite-constant rcnst :backchain-limit-rw)
        :simplify-clause-pot-lst nil
        :pot-lst-terms nil
        :rcnst rcnst
        :gstack gstack
        :ttree nil))
    (cond (contradictionp (mv step-limit contradictionp nil))
      (t (mv step-limit nil simplify-clause-pot-lst)))))

(defun setup-simplify-clause-pot-lst
  (cl ttrees
    fc-pair-lst
    type-alist
    rcnst
    wrld
    state
    step-limit)
  (cond ((null fc-pair-lst) (setup-simplify-clause-pot-lst1 cl
        ttrees
        type-alist
        rcnst
        wrld
        state
        step-limit))
    (t (setup-simplify-clause-pot-lst (cons (dumb-negate-lit (caar fc-pair-lst)) cl)
        (cons (cdar fc-pair-lst) ttrees)
        (cdr fc-pair-lst)
        type-alist
        rcnst
        wrld
        state
        step-limit))))

(defun sequential-subst-var-term
  (alist term)
  (cond ((null alist) term)
    (t (sequential-subst-var-term (cdr alist)
        (subst-var (cdar alist) (caar alist) term)))))

(defun process-equational-polys
  (cl hist rcnst type-alist wrld pot-lst flg ttree)
  (cond ((null pot-lst) (mv flg cl ttree))
    (t (mv-let (ttree1 lhs rhs)
        (find-equational-poly (car pot-lst) hist)
        (if (null ttree1)
          (process-equational-polys cl
            hist
            rcnst
            type-alist
            wrld
            (cdr pot-lst)
            flg
            ttree)
          (let ((derived-equation (cond ((and (variablep lhs) (not (dumb-occur lhs rhs))) (cons-term 'equal (list lhs rhs)))
                 ((and (variablep rhs) (not (dumb-occur rhs lhs))) (cons-term 'equal (list rhs lhs)))
                 (t (cons-term 'equal (list lhs rhs))))) (ok-to-force (ok-to-force rcnst))
              (ens (access rewrite-constant rcnst :current-enabled-structure)))
            (mv-let (flag1 ttree2)
              (add-linear-assumption derived-equation
                (mcons-term* 'acl2-numberp lhs)
                type-alist
                ens
                (immediate-forcep nil ens)
                ok-to-force
                wrld
                ttree1)
              (mv-let (flag2 ttree3)
                (cond ((eq flag1 :failed) (mv :failed ttree1))
                  (t (add-linear-assumption derived-equation
                      (mcons-term* 'acl2-numberp rhs)
                      type-alist
                      ens
                      (immediate-forcep nil ens)
                      ok-to-force
                      wrld
                      ttree2)))
                (let* ((lhs (if (eq flag1 :known-false)
                       *0*
                       lhs)) (rhs (if (eq flag2 :known-false)
                        *0*
                        rhs))
                    (new-lit (dumb-negate-lit (mcons-term* 'equal lhs rhs)))
                    (hitp (not (or (eq flag2 :failed)
                          (and (eq flag1 :added) (eq flag2 :added))
                          (and (equal lhs *0*) (equal rhs *0*))
                          (member-term new-lit cl)))))
                  (process-equational-polys (if hitp
                      (add-literal new-lit cl nil)
                      cl)
                    hist
                    rcnst
                    type-alist
                    wrld
                    (cdr pot-lst)
                    (or flg hitp)
                    (cons-tag-trees (cond (hitp ttree3) (t ttree1)) ttree)))))))))))

(defun enumerate-elements
  (lst i)
  (cond ((null lst) nil)
    (t (cons i (enumerate-elements (cdr lst) (1+ i))))))

(defun already-used-by-fertilize-clausep
  (lit hist get-clause-id)
  (cond ((null hist) nil)
    ((and (eq (access history-entry (car hist) :processor)
         'fertilize-clause)
       (tag-tree-occur 'literal
         lit
         (access history-entry (car hist) :ttree))) (or get-clause-id
        (tagged-object 'clause-id
          (access history-entry (car hist) :ttree))))
    (t (already-used-by-fertilize-clausep lit
        (cdr hist)
        get-clause-id))))

(defun unhidden-lit-info
  (hist clause pos wrld)
  (cond ((null clause) (mv nil nil nil))
    (t (let ((lit (car clause)))
        (case-match lit
          (('not ('hide (equiv & &))) (cond ((equivalence-relationp equiv wrld) (let* ((new-lit (fcons-term* 'not (fargn (fargn lit 1) 1))) (cl-id (already-used-by-fertilize-clausep new-lit hist nil)))
                  (cond (cl-id (mv pos new-lit cl-id))
                    (t (unhidden-lit-info hist (cdr clause) (1+ pos) wrld)))))
              (t (unhidden-lit-info hist (cdr clause) (1+ pos) wrld))))
          (& (unhidden-lit-info hist (cdr clause) (1+ pos) wrld)))))))

(defun tilde-@-hyp-phrase
  (len-tail cl)
  (let* ((len (length cl)) (n (- len len-tail)))
    (cond ((int= n len) '("the conclusion"))
      ((and (int= len 2) (int= n 1)) "the hypothesis")
      (t (msg "the ~n0 hypothesis" (cons n 'th))))))

(defun equational-polyp-limit
  (wrld)
  (cdr (assoc-eq t
      (table-alist 'equational-polyp-limit-table wrld))))

(defun equational-polyp-ok-rec
  (hist n)
  (cond ((zp n) nil)
    ((endp hist) t)
    ((and (eq (access history-entry (car hist) :processor)
         'simplify-clause)
       (tagged-objects 'find-equational-poly
         (access history-entry (car hist) :ttree))) (cond ((zp n) nil)
        (t (equational-polyp-ok-rec (cdr hist) (1- n)))))
    (t (equational-polyp-ok-rec (cdr hist) n))))

(defun equational-polyp-ok
  (hist wrld)
  (let ((limit (equational-polyp-limit wrld)))
    (or (null limit) (equational-polyp-ok-rec hist limit))))

(defun simplify-clause1
  (top-clause hist rcnst wrld state step-limit)
  (mv-let (hitp current-clause pts remove-trivial-equivalences-ttree)
    (remove-trivial-equivalences top-clause
      nil
      t
      (access rewrite-constant rcnst :current-enabled-structure)
      wrld
      state
      nil)
    (declare (ignore pts))
    (let ((local-rcnst (change rewrite-constant
           rcnst
           :top-clause top-clause
           :current-clause current-clause)) (current-clause-pts (enumerate-elements current-clause 0)))
      (mv-let (contradictionp type-alist fc-pair-lst)
        (forward-chain-top (if (eq (access rewrite-constant rcnst :rewriter-state)
              'settled-down)
            'simplify-clause-settled-down
            'simplify-clause)
          current-clause
          current-clause-pts
          (ok-to-force local-rcnst)
          nil
          wrld
          (access rewrite-constant rcnst :current-enabled-structure)
          (access rewrite-constant rcnst :oncep-override)
          state)
        (cond (contradictionp (mv step-limit
              'hit
              nil
              (cons-tag-trees remove-trivial-equivalences-ttree
                fc-pair-lst)))
          (t (sl-let (contradictionp simplify-clause-pot-lst)
              (pstk (setup-simplify-clause-pot-lst current-clause
                  (pts-to-ttree-lst current-clause-pts)
                  fc-pair-lst
                  type-alist
                  local-rcnst
                  wrld
                  state
                  step-limit))
              (cond (contradictionp (mv step-limit
                    'hit
                    nil
                    (cons-tag-trees remove-trivial-equivalences-ttree
                      (push-lemma *fake-rune-for-linear*
                        (access poly contradictionp :ttree)))))
                (t (mv-let (flg new-current-clause ttree)
                    (if (equational-polyp-ok hist wrld)
                      (pstk (process-equational-polys current-clause
                          hist
                          local-rcnst
                          type-alist
                          wrld
                          simplify-clause-pot-lst
                          nil
                          remove-trivial-equivalences-ttree))
                      (mv nil current-clause remove-trivial-equivalences-ttree))
                    (cond (flg (mv-let (hitp newest-current-clause pts ttree1)
                          (pstk (remove-trivial-equivalences new-current-clause
                              nil
                              t
                              (access rewrite-constant
                                local-rcnst
                                :current-enabled-structure)
                              wrld
                              state
                              ttree))
                          (declare (ignore pts hitp))
                          (mv step-limit
                            'hit
                            (list newest-current-clause)
                            (push-lemma *fake-rune-for-linear-equalities* ttree1))))
                      (t (sl-let (flg ecnt ans ttree)
                          (rewrite-clause current-clause
                            current-clause-pts
                            1
                            (initial-gstack 'simplify-clause nil current-clause)
                            nil
                            fc-pair-lst
                            wrld
                            simplify-clause-pot-lst
                            local-rcnst
                            hitp
                            1
                            nil
                            remove-trivial-equivalences-ttree
                            *trivial-non-nil-ttree*
                            nil
                            state
                            step-limit)
                          (declare (ignore ecnt))
                          (cond ((null flg) (mv-let (pos unhidden-lit old-cl-id)
                                (unhidden-lit-info hist top-clause 0 wrld)
                                (cond (pos (let ((tail (nthcdr (1+ pos) top-clause)))
                                      (mv step-limit
                                        'hit-rewrite
                                        (list (append (take pos top-clause) (cons unhidden-lit tail)))
                                        (add-to-tag-tree! 'hyp-phrase
                                          (tilde-@-hyp-phrase (len tail) top-clause)
                                          (add-to-tag-tree! 'clause-id
                                            old-cl-id
                                            (push-lemma (fn-rune-nume 'hide nil nil wrld)
                                              (rw-cache ttree)))))))
                                  (t (mv step-limit nil ans ttree)))))
                            (t (mv step-limit 'hit-rewrite ans ttree))))))))))))))))

(defun some-element-dumb-occur-lst
  (lst1 lst2)
  (cond ((null lst1) nil)
    ((dumb-occur-lst (car lst1) lst2) t)
    (t (some-element-dumb-occur-lst (cdr lst1) lst2))))

(defun abort-info-stack
  (abort-info)
  (declare (xargs :guard t :mode :logic))
  (and (consp abort-info)
    (if (symbolp (car abort-info))
      (cdr abort-info)
      abort-info)))

(defun abort-info-cause
  (abort-info)
  (declare (xargs :guard t :mode :logic))
  (if (consp abort-info)
    (and (symbolp (car abort-info)) (car abort-info))
    abort-info))

(defun update-gag-info-for-abort
  (abort-cause gag-state)
  (let ((abort-info (access gag-state gag-state :abort-info)))
    (change gag-state
      gag-state
      :abort-info (cond ((consp abort-info) (assert$ (not (symbolp (car abort-info)))
            (cons abort-cause abort-info)))
        (t (assert$ (null abort-info) abort-cause))))))

(defun controller-unify-subst2
  (vars acc)
  (cond ((endp vars) acc)
    ((assoc-eq (car vars) acc) acc)
    (t (controller-unify-subst2 (cdr vars)
        (acons (car vars) (car vars) acc)))))

(defun controller-unify-subst1
  (actuals controllers acc)
  (cond ((endp actuals) acc)
    ((car controllers) (controller-unify-subst2 (all-vars (car actuals))
        (controller-unify-subst1 (cdr actuals)
          (cdr controllers)
          acc)))
    (t (controller-unify-subst1 (cdr actuals)
        (cdr controllers)
        acc))))

(defun controller-unify-subst
  (name term def-body)
  (let* ((controller-alist (access def-body def-body :controller-alist)) (controllers (cdr (assoc-eq name controller-alist))))
    (cond (controllers (controller-unify-subst1 (fargs term) controllers nil))
      (t :none))))

(defun filter-disabled-expand-terms
  (terms ens wrld)
  (cond ((null terms) nil)
    ((or (variablep (car terms)) (fquotep (car terms))) nil)
    (t (cond ((flambdap (ffn-symb (car terms))) (cons (make expand-hint
              :pattern (car terms)
              :alist :none :rune nil
              :equiv 'equal
              :hyp nil
              :lhs (car terms)
              :rhs (subcor-var (lambda-formals (ffn-symb (car terms)))
                (fargs (car terms))
                (lambda-body (ffn-symb (car terms)))))
            (filter-disabled-expand-terms (cdr terms) ens wrld)))
        (t (let* ((term (car terms)) (name (ffn-symb term))
              (def-body (def-body name wrld))
              (formals (access def-body def-body :formals)))
            (cond ((and def-body
                 (enabled-numep (access def-body def-body :nume) ens)) (cons (make expand-hint
                    :pattern term
                    :alist (let ((alist (controller-unify-subst name term def-body)))
                      (if (eq alist :none)
                        :none (cons :constants alist)))
                    :rune (access def-body def-body :rune)
                    :equiv (access def-body def-body :equiv)
                    :hyp (access def-body def-body :hyp)
                    :lhs (cons-term name formals)
                    :rhs (access def-body def-body :concl))
                  (filter-disabled-expand-terms (cdr terms) ens wrld)))
              (t (filter-disabled-expand-terms (cdr terms) ens wrld)))))))))

(defun found-hit-rewrite-hist-entry
  (hist)
  (if (endp hist)
    nil
    (or (car (member-eq (access history-entry (car hist) :signal)
          '(hit-rewrite hit-rewrite2)))
      (found-hit-rewrite-hist-entry (cdr hist)))))

(defun simplify-clause-rcnst
  (cl hist pspv wrld)
  (let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
    (cond ((assoc-eq 'settled-down-clause hist) (mv (if (eq 'settled-down-clause
              (access history-entry (car hist) :processor))
            (change rewrite-constant
              rcnst
              :force-info (if (ffnnamep-lst 'if cl)
                'weak
                t)
              :rewriter-state 'settled-down)
            (change rewrite-constant
              rcnst
              :force-info (if (ffnnamep-lst 'if cl)
                'weak
                t)))
          'hit))
      (t (let* ((new-force-info (if (ffnnamep-lst 'if cl)
               'weak
               t)) (induction-concl-terms (access prove-spec-var pspv :induction-concl-terms))
            (hist-entry-hit (found-hit-rewrite-hist-entry hist))
            (hit-rewrite2 (or (eq hist-entry-hit 'hit-rewrite2)
                (and (eq hist-entry-hit 'hit-rewrite)
                  (not (some-element-dumb-occur-lst induction-concl-terms cl))))))
          (cond (hit-rewrite2 (mv (change rewrite-constant rcnst :force-info new-force-info)
                'hit-rewrite2))
            (t (mv (change rewrite-constant
                  rcnst
                  :force-info new-force-info
                  :terms-to-be-ignored-by-rewrite (append (access prove-spec-var pspv :induction-hyp-terms)
                    (access rewrite-constant
                      rcnst
                      :terms-to-be-ignored-by-rewrite))
                  :expand-lst (append? (access rewrite-constant rcnst :expand-lst)
                    (filter-disabled-expand-terms induction-concl-terms
                      (access rewrite-constant rcnst :current-enabled-structure)
                      wrld)))
                nil))))))))

(defun simplify-clause
  (cl hist pspv wrld state step-limit)
  (mv-let (local-rcnst signal)
    (simplify-clause-rcnst cl hist pspv wrld)
    (sl-let (hitp clauses ttree)
      (simplify-clause1 cl hist local-rcnst wrld state step-limit)
      (cond (hitp (mv step-limit (or signal hitp) clauses ttree pspv))
        (t (mv step-limit 'miss nil ttree nil))))))

(defun settled-down-clause
  (clause hist pspv wrld state)
  (declare (ignore wrld state))
  (cond ((assoc-eq 'settled-down-clause hist) (mv 'miss nil nil nil))
    (t (mv 'hit (list clause) nil pspv))))

(defun member-class-name-runes
  (class name runes)
  (cond ((endp runes) nil)
    ((let ((rune (car runes)))
       (and (eq (car rune) class) (eq (base-symbol rune) name))) t)
    (t (member-class-name-runes class name (cdr runes)))))

(defun extract-and-classify-lemmas2
  (names class
    ignore-lst
    if-intro
    case-split
    immed-forced
    forced-runes)
  (cond ((endp names) nil)
    ((member-eq (car names) ignore-lst) (extract-and-classify-lemmas2 (cdr names)
        class
        ignore-lst
        if-intro
        case-split
        immed-forced
        forced-runes))
    (t (let ((name (car names)))
        (acons name
          (append (if (member-class-name-runes class name if-intro)
              '("if-intro")
              nil)
            (if (member-class-name-runes class name case-split)
              '("case-split")
              nil)
            (if (member-class-name-runes class name immed-forced)
              '("immed-forced")
              nil)
            (if (member-class-name-runes class name forced-runes)
              '("forced")
              nil))
          (extract-and-classify-lemmas2 (cdr names)
            class
            ignore-lst
            if-intro
            case-split
            immed-forced
            forced-runes))))))

(defun extract-and-classify-lemmas1
  (class-alist ignore-lst
    if-intro
    case-split
    immed-forced
    forced-runes)
  (cond ((endp class-alist) nil)
    (t (let* ((class (caar class-alist)) (symbol-alist (extract-and-classify-lemmas2 (cdar class-alist)
              class
              ignore-lst
              if-intro
              case-split
              immed-forced
              forced-runes))
          (rest (extract-and-classify-lemmas1 (cdr class-alist)
              ignore-lst
              if-intro
              case-split
              immed-forced
              forced-runes)))
        (cond (symbol-alist (acons class symbol-alist rest))
          (t rest))))))

(defun runes-to-class-alist1
  (runes alist)
  (cond ((endp runes) alist)
    (t (let* ((rune (car runes)) (type (car rune))
          (sym (base-symbol rune))
          (old (cdr (assoc-eq type alist))))
        (runes-to-class-alist1 (cdr runes)
          (put-assoc-eq type (cons sym old) alist))))))

(defun strict-merge-symbol<
  (l1 l2 acc)
  (declare (xargs :guard (and (symbol-listp l1) (symbol-listp l2) (true-listp acc))
      :mode :program))
  (cond ((endp l1) (revappend acc l2))
    ((endp l2) (revappend acc l1))
    ((eq (car l1) (car l2)) (strict-merge-symbol< (cdr l1) (cdr l2) (cons (car l1) acc)))
    ((symbol< (car l1) (car l2)) (strict-merge-symbol< (cdr l1) l2 (cons (car l1) acc)))
    (t (strict-merge-symbol< l1 (cdr l2) (cons (car l2) acc)))))

(defun strict-merge-sort-symbol<
  (l)
  (declare (xargs :guard (symbol-listp l) :mode :program))
  (cond ((endp (cdr l)) l)
    (t (strict-merge-symbol< (strict-merge-sort-symbol< (evens l))
        (strict-merge-sort-symbol< (odds l))
        nil))))

(defun sort-symbol-listp
  (x)
  (declare (xargs :guard (symbol-listp x)))
  (cond ((strict-symbol<-sortedp x) x)
    (t (strict-merge-sort-symbol< x))))

(defun strict-merge-sort-symbol<-cdrs
  (alist)
  (cond ((endp alist) nil)
    (t (acons (caar alist)
        (strict-merge-sort-symbol< (cdar alist))
        (strict-merge-sort-symbol<-cdrs (cdr alist))))))

(defun runes-to-class-alist
  (runes)
  (strict-merge-sort-symbol<-cdrs (runes-to-class-alist1 runes
      (pairlis$ (strict-merge-sort-symbol< (strip-cars runes))
        nil))))

(defun extract-and-classify-lemmas
  (ttree ignore-lst forced-runes)
  (extract-and-classify-lemmas1 (runes-to-class-alist (tagged-objects 'lemma ttree))
    ignore-lst
    (tagged-objects 'splitter-if-intro ttree)
    (tagged-objects 'splitter-case-split ttree)
    (tagged-objects 'splitter-immed-forced ttree)
    forced-runes))

(defun tilde-*-conjunction-of-possibly-forced-names-phrase1
  (alist)
  (cond ((null alist) nil)
    (t (cons (let ((name (caar alist)) (splitter-types (cdar alist)))
          (cond ((null splitter-types) (msg "~x0" name))
            (t (msg "~x0 (~*1)"
                name
                (list "" "~s*" "~s*," "~s*," splitter-types)))))
        (tilde-*-conjunction-of-possibly-forced-names-phrase1 (cdr alist))))))

(defun tilde-*-conjunction-of-possibly-forced-names-phrase
  (lst)
  (list ""
    "~@*"
    "~@* and "
    "~@*, "
    (tilde-*-conjunction-of-possibly-forced-names-phrase1 lst)))

(defun tilde-*-simp-phrase1
  (alist abbreviations-flg)
  (cond ((null alist) (mv nil nil))
    (t (let ((pair (assoc-eq (caar alist) *fake-rune-alist*)))
        (cond (pair (mv-let (rest-msgs rest-pairs)
              (tilde-*-simp-phrase1 (cdr alist) abbreviations-flg)
              (mv (cons (cdr pair) rest-msgs) rest-pairs)))
          (t (let ((names (tilde-*-conjunction-of-possibly-forced-names-phrase (cdar alist))) (pluralp (if (cdr (cdar alist))
                    t
                    nil)))
              (mv-let (msg pair)
                (case (caar alist)
                  (:definition (mv (if abbreviations-flg
                        (if pluralp
                          "the simple :definitions ~*D"
                          "the simple :definition ~*D")
                        (if pluralp
                          "the :definitions ~*D"
                          "the :definition ~*D"))
                      (cons #\D names)))
                  (:executable-counterpart (mv (if pluralp
                        "the :executable-counterparts of ~*X"
                        "the :executable-counterpart of ~*X")
                      (cons #\X names)))
                  (:rewrite (mv (if abbreviations-flg
                        (if pluralp
                          "the simple :rewrite rules ~*R"
                          "the simple :rewrite rule ~*R")
                        (if pluralp
                          "the :rewrite rules ~*R"
                          "the :rewrite rule ~*R"))
                      (cons #\R names)))
                  (:rewrite-quoted-constant (mv (if pluralp
                        "the :rewrite-quoted-constant rules ~*Q"
                        "the :rewrite-quoted-constant rule ~*Q")
                      (cons #\Q names)))
                  (:linear (mv (if pluralp
                        "the :linear rules ~*L"
                        "the :linear rule ~*L")
                      (cons #\L names)))
                  (:built-in-clause (mv (if pluralp
                        "the :built-in-clause rules ~*B"
                        "the :built-in-clause rule ~*B")
                      (cons #\B names)))
                  (:compound-recognizer (mv (if pluralp
                        "the :compound-recognizer rules ~*C"
                        "the :compound-recognizer rule ~*C")
                      (cons #\C names)))
                  (:elim (mv (if pluralp
                        "the :elim rules ~*e"
                        "the :elim rule ~*e")
                      (cons #\e names)))
                  (:generalize (mv (if pluralp
                        "the :generalize rules ~*G"
                        "the :generalize rule ~*G")
                      (cons #\G names)))
                  (:induction (mv (if pluralp
                        "the :induction rules ~*I"
                        "the :induction rule ~*I")
                      (cons #\I names)))
                  (:meta (mv (if pluralp
                        "the :meta rules ~*M"
                        "the :meta rule ~*M")
                      (cons #\M names)))
                  (:forward-chaining (mv (if pluralp
                        "the :forward-chaining rules ~*F"
                        "the :forward-chaining rule ~*F")
                      (cons #\F names)))
                  (:equivalence (mv (if pluralp
                        "the :equivalence rules ~*E"
                        "the :equivalence rule ~*E")
                      (cons #\E names)))
                  (:refinement (mv (if pluralp
                        "the :refinement rules ~*r"
                        "the :refinement rule ~*r")
                      (cons #\r names)))
                  (:congruence (mv (if pluralp
                        "the :congruence rules ~*c"
                        "the :congruence rule ~*c")
                      (cons #\c names)))
                  (:type-prescription (mv (if pluralp
                        "the :type-prescription rules ~*T"
                        "the :type-prescription rule ~*T")
                      (cons #\T names)))
                  (:type-set-inverter (mv (if pluralp
                        "the :type-set-inverter rules ~*t"
                        "the :type-set-inverter rule ~*t")
                      (cons #\t names)))
                  (otherwise (mv (er hard
                        'tilde-*-simp-phrase1
                        "We did not expect to see the simplifier report a rune ~
                       of type ~x0."
                        (caar alist))
                      nil)))
                (mv-let (rest-msgs rest-pairs)
                  (tilde-*-simp-phrase1 (cdr alist) abbreviations-flg)
                  (mv (cons msg rest-msgs) (cons pair rest-pairs)))))))))))

(defun tilde-*-raw-simp-phrase1
  (runes forced-runes punct ignore-lst phrase acc)
  (cond ((null runes) (cond ((null acc) (mv nil
            (list (cons #\p
                (if phrase
                  (msg "  " phrase)
                  "")))))
        (t (mv (list (concatenate 'string
                "~@Fthe list of runes,~|~% ~YRe"
                (case punct (#\, ",~|~%") (#\. ".~|") (otherwise "~|"))
                "~@p"))
            (list (cons #\F
                (if forced-runes
                  (msg "(forcing with ~&0) " forced-runes)
                  ""))
              (cons #\p
                (if phrase
                  (msg "~@0~|" phrase)
                  ""))
              (cons #\R (merge-sort-runes (reverse acc)))
              (cons #\e nil))))))
    (t (let ((pair (assoc-eq (caar runes) *fake-rune-alist*)))
        (cond (pair (mv-let (rest-msgs rest-pairs)
              (tilde-*-raw-simp-phrase1 (cdr runes)
                forced-runes
                punct
                ignore-lst
                phrase
                acc)
              (mv (cons (if (null rest-msgs)
                    (concatenate 'string
                      (cdr pair)
                      (case punct (#\, ",") (#\. ".") (otherwise "")))
                    (cdr pair))
                  rest-msgs)
                rest-pairs)))
          (t (tilde-*-raw-simp-phrase1 (cdr runes)
              forced-runes
              punct
              ignore-lst
              phrase
              (if (member-eq (base-symbol (car runes)) ignore-lst)
                acc
                (cons (car runes) acc)))))))))

(defun recover-forced-runes1
  (recs ans)
  (cond ((endp recs) ans)
    (t (recover-forced-runes1 (cdr recs)
        (let ((rune (access assumnote
               (car (access assumption (car recs) :assumnotes))
               :rune)))
          (cond ((not (symbolp rune)) (add-to-set-equal rune ans))
            (t ans)))))))

(defun recover-forced-runes
  (ttree)
  (recover-forced-runes1 (tagged-objects 'assumption ttree)
    nil))

(defun tilde-*-raw-simp-phrase
  (ttree punct phrase)
  (let ((forced-runes (recover-forced-runes ttree)))
    (let ((runes (all-runes-in-ttree ttree nil)))
      (mv-let (message-lst char-alist)
        (tilde-*-raw-simp-phrase1 runes
          forced-runes
          punct
          nil
          phrase
          nil)
        (list* (concatenate 'string
            "trivial ob~-ser~-va~-tions"
            (case punct (#\, ", ") (#\. ".") (otherwise "")))
          "~@*"
          "~@* and "
          "~@*, "
          message-lst
          char-alist)))))

(defun tilde-*-simp-phrase
  (ttree)
  (let ((forced-runes (recover-forced-runes ttree)))
    (mv-let (message-lst char-alist)
      (tilde-*-simp-phrase1 (extract-and-classify-lemmas ttree nil forced-runes)
        nil)
      (list* "trivial ob~-ser~-va~-tions"
        "~@*"
        "~@* and "
        "~@*, "
        message-lst
        char-alist))))

(defun tilde-@-pool-name-phrase
  (forcing-round pool-lst)
  (cond ((= forcing-round 0) (cons "*~*0"
        (list (cons #\0 (list "" "~x*" "~x*." "~x*." pool-lst)))))
    (t (cons "[~xr]*~*0"
        (list (cons #\r forcing-round)
          (cons #\0 (list "" "~x*" "~x*." "~x*." pool-lst)))))))

(defun tilde-@-pool-name-phrase-lst
  (forcing-round lst)
  (cond ((null lst) nil)
    (t (cons (tilde-@-pool-name-phrase forcing-round (car lst))
        (tilde-@-pool-name-phrase-lst forcing-round (cdr lst))))))

(defun tilde-@-clause-id-phrase
  (id)
  (cons (cond ((= (access clause-id id :forcing-round) 0) (cond ((null (access clause-id id :pool-lst)) (cond ((null (access clause-id id :case-lst)) "Goal~#q~[~/'~/''~/'''~/'~xn'~]")
              (t "Subgoal ~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
          (t "Subgoal ~@p/~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
      (t (cond ((null (access clause-id id :pool-lst)) (cond ((null (access clause-id id :case-lst)) "[~xr]Goal~#q~[~/'~/''~/'''~/'~xn'~]")
              (t "[~xr]Subgoal ~@c~#q~[~/'~/''~/'''~/'~xn'~]")))
          (t "[~xr]Subgoal ~@p/~@c~#q~[~/'~/''~/'''~/'~xn'~]"))))
    (list (cons #\r (access clause-id id :forcing-round))
      (cons #\p
        (tilde-@-pool-name-phrase 0 (access clause-id id :pool-lst)))
      (cons #\c
        (cons "~*0"
          (list (cons #\0
              (list ""
                "~x*"
                "~x*."
                "~x*."
                (access clause-id id :case-lst))))))
      (cons #\q
        (cond ((> (access clause-id id :primes) 3) 4)
          (t (access clause-id id :primes))))
      (cons #\n (access clause-id id :primes)))))

(defun tilde-@-bddnote-phrase
  (x)
  (cond ((null x) "")
    (t (msg " with BDDs (~x0 nodes)" (access bddnote x :mx-id)))))

(defun parse-natural1
  (str i maximum ans)
  (cond ((>= i maximum) (mv ans maximum))
    (t (let* ((c (char str i)) (d (case c
              (#\0 0)
              (#\1 1)
              (#\2 2)
              (#\3 3)
              (#\4 4)
              (#\5 5)
              (#\6 6)
              (#\7 7)
              (#\8 8)
              (#\9 9)
              (otherwise nil))))
        (cond (d (parse-natural1 str
              (1+ i)
              maximum
              (cond ((null ans) d) (t (+ (* 10 ans) d)))))
          (t (mv ans i)))))))

(defun parse-natural
  (dflg str i maximum)
  (cond ((>= i maximum) (mv nil maximum))
    ((and dflg (eql (char str i) #\D)) (mv-let (ans k)
        (parse-natural1 str (+ 1 i) maximum nil)
        (cond ((null ans) (mv nil i))
          (t (mv (packn (list 'd ans)) k)))))
    (t (parse-natural1 str i maximum nil))))

(defun parse-dotted-naturals
  (dflg str i maximum ans)
  (cond ((>= i maximum) (mv (reverse ans) maximum))
    (t (mv-let (nat j)
        (parse-natural dflg str i maximum)
        (cond ((null nat) (mv (reverse ans) i))
          ((>= j maximum) (mv (reverse (cons nat ans)) maximum))
          ((and (eql (char str j) #\.)
             (< (1+ j) maximum)
             (or (member (char str (1+ j))
                 '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9))
               (and dflg (eql (char str (1+ j)) #\D)))) (parse-dotted-naturals dflg
              str
              (1+ j)
              maximum
              (cons nat ans)))
          (t (mv (reverse (cons nat ans)) j)))))))

(defun parse-match
  (pat j patmax str i strmax)
  (cond ((>= j patmax) i)
    ((>= i strmax) nil)
    ((or (eql (char pat j) (char str i))
       (eql (char-downcase (char pat j))
         (char-downcase (char str i)))) (parse-match pat (1+ j) patmax str (1+ i) strmax))
    (t nil)))

(defun parse-primes
  (str i maximum)
  (cond ((>= i maximum) (mv 0 maximum))
    ((eql (char str i) #\') (cond ((= (+ 1 i) maximum) (mv 1 maximum))
        ((eql (char str (+ 1 i)) #\') (cond ((= (+ 2 i) maximum) (mv 2 maximum))
            ((eql (char str (+ 2 i)) #\') (mv 3 (+ 3 i)))
            (t (mv 2 (+ 2 i)))))
        (t (mv-let (nat j)
            (parse-natural nil str (+ 1 i) maximum)
            (cond ((null nat) (mv 1 (+ 1 i)))
              ((< nat 4) (mv 1 (+ 1 i)))
              ((= j maximum) (mv 1 (+ 1 i)))
              ((eql (char str j) #\') (mv nat (+ 1 j)))
              (t (mv 1 (+ 1 i))))))))
    (t (mv 0 i))))

(defun parse-clause-id2
  (forcing-round pool-lst str i maximum)
  (mv-let (case-lst j)
    (parse-dotted-naturals t str i maximum nil)
    (cond ((member 0 case-lst) nil)
      (t (mv-let (n j)
          (parse-primes str j maximum)
          (cond ((= j maximum) (make clause-id
                :forcing-round forcing-round
                :pool-lst pool-lst
                :case-lst case-lst
                :primes n))
            (t nil)))))))

(defun parse-clause-id1
  (forcing-round str i maximum)
  (cond ((< maximum (+ i 4)) nil)
    ((member (char str i) '(#\G #\g)) (let ((k (parse-match "Goal" 0 4 str i maximum)))
        (cond (k (mv-let (n j)
              (parse-primes str k maximum)
              (cond ((= j maximum) (make clause-id
                    :forcing-round forcing-round
                    :pool-lst nil
                    :case-lst nil
                    :primes n))
                (t nil))))
          (t nil))))
    (t (let ((k (parse-match "Subgoal " 0 8 str i maximum)))
        (cond ((null k) nil)
          ((>= k maximum) nil)
          ((eql (char str k) #\*) (mv-let (pool-lst j)
              (parse-dotted-naturals nil str (1+ k) maximum nil)
              (cond ((or (null pool-lst)
                   (member 0 pool-lst)
                   (> (+ 1 j) maximum)
                   (not (eql (char str j) #\/))) nil)
                (t (parse-clause-id2 forcing-round
                    pool-lst
                    str
                    (+ 1 j)
                    maximum)))))
          (t (parse-clause-id2 forcing-round nil str k maximum)))))))

(defun parse-clause-id
  (str)
  (cond ((stringp str) (let* ((maximum (length str)))
        (cond ((< maximum 4) nil)
          ((eql (char str 0) #\[) (mv-let (forcing-round i)
              (parse-natural nil str 1 maximum)
              (cond ((and forcing-round (eql (char str i) #\])) (parse-clause-id1 forcing-round str (1+ i) maximum))
                (t nil))))
          (t (parse-clause-id1 0 str 0 maximum)))))
    ((eq str t) *initial-clause-id*)
    (t nil)))

(defun tilde-@-case-split-limitations-phrase
  (sr-flg case-flg prefix)
  (if (or sr-flg case-flg)
    (msg "~@0(By the way, the ~@1 affected this analysis.  See :DOC ~
            case-split-limitations.)"
      prefix
      (if sr-flg
        (if case-flg
          "subsumption/replacement and case limits"
          "subsumption/replacement limit")
        "case limit"))
    ""))

(defun simplify-clause-msg1
  (signal cl-id clauses speciousp ttree pspv state)
  (declare (ignore signal pspv))
  (let ((raw-proof-format (f-get-global 'raw-proof-format state)))
    (cond (speciousp (fms "This ~#0~[~/forcibly ~]simplifies~@b, using ~*1~@pto a set of ~
            conjectures including ~@3 itself!  Therefore, we ignore this ~
            specious simp~-li~-fi~-ca~-tion.  See :DOC ~
            specious-simplification.~@c~|"
          (list (cons #\0
              (if (tagged-objectsp 'assumption ttree)
                1
                0))
            (cons #\1
              (if raw-proof-format
                (tilde-*-raw-simp-phrase ttree #\, "")
                (tilde-*-simp-phrase ttree)))
            (cons #\p
              (if raw-proof-format
                ""
                ", "))
            (cons #\3 (tilde-@-clause-id-phrase cl-id))
            (cons #\b
              (tilde-@-bddnote-phrase (tagged-object 'bddnote ttree)))
            (cons #\c
              (tilde-@-case-split-limitations-phrase (tagged-objects 'sr-limit ttree)
                (tagged-objects 'case-limit ttree)
                "  ")))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      ((null clauses) (cond (raw-proof-format (fms "But ~#0~[~/forced ~]simplification~@b reduces this to T, using ~
              ~*1~|"
              (list (cons #\0
                  (if (tagged-objectsp 'assumption ttree)
                    1
                    0))
                (cons #\1
                  (tilde-*-raw-simp-phrase ttree
                    #\.
                    (tilde-@-case-split-limitations-phrase (tagged-objects 'sr-limit ttree)
                      (tagged-objects 'case-limit ttree)
                      "")))
                (cons #\b
                  (tilde-@-bddnote-phrase (tagged-object 'bddnote ttree))))
              (proofs-co state)
              state
              (term-evisc-tuple nil state)))
          (t (fms "But ~#0~[~/forced ~]simplification~@b reduces this to T, using ~
              ~*1.~@c~|"
              (list (cons #\0
                  (if (tagged-objectsp 'assumption ttree)
                    1
                    0))
                (cons #\1 (tilde-*-simp-phrase ttree))
                (cons #\b
                  (tilde-@-bddnote-phrase (tagged-object 'bddnote ttree)))
                (cons #\c
                  (tilde-@-case-split-limitations-phrase (tagged-objects 'sr-limit ttree)
                    (tagged-objects 'case-limit ttree)
                    "  ")))
              (proofs-co state)
              state
              (term-evisc-tuple nil state)))))
      (t (let ((hyp-phrase (tagged-object 'hyp-phrase ttree)))
          (cond (hyp-phrase (fms "We remove HIDE from ~@0, which was used heuristically to ~
                     transform ~@1 by substituting into the rest of that ~
                     goal.  This produces~|"
                (list (cons #\0 hyp-phrase)
                  (cons #\1
                    (tilde-@-clause-id-phrase (tagged-object 'clause-id ttree))))
                (proofs-co state)
                state
                (term-evisc-tuple nil state)))
            (raw-proof-format (fms "This ~#0~[~/forcibly ~]simplifies~#a~[~/ (dropping false ~
                     conclusion; see :DOC clause)~]~@b, using ~*1to~#2~[~/ ~
                     the following ~n3 conjectures.~@c~]~|"
                (list (cons #\0
                    (if (tagged-objectsp 'assumption ttree)
                      1
                      0))
                  (cons #\1 (tilde-*-raw-simp-phrase ttree #\, ""))
                  (cons #\2 clauses)
                  (cons #\3 (length clauses))
                  (cons #\a
                    (if (tagged-objectsp 'dropped-last-literal ttree)
                      1
                      0))
                  (cons #\b
                    (tilde-@-bddnote-phrase (tagged-object 'bddnote ttree)))
                  (cons #\c
                    (tilde-@-case-split-limitations-phrase (tagged-objectsp 'sr-limit ttree)
                      (tagged-objectsp 'case-limit ttree)
                      "  ")))
                (proofs-co state)
                state
                (term-evisc-tuple nil state)))
            (t (fms "This ~#0~[~/forcibly ~]simplifies~#a~[~/ (dropping false ~
                     conclusion; see :DOC clause)~]~@b, using ~*1, to~#2~[~/ ~
                     the following ~n3 conjectures.~@c~]~|"
                (list (cons #\0
                    (if (tagged-objectsp 'assumption ttree)
                      1
                      0))
                  (cons #\1 (tilde-*-simp-phrase ttree))
                  (cons #\2 clauses)
                  (cons #\3 (length clauses))
                  (cons #\a
                    (if (tagged-objectsp 'dropped-last-literal ttree)
                      1
                      0))
                  (cons #\b
                    (tilde-@-bddnote-phrase (tagged-object 'bddnote ttree)))
                  (cons #\c
                    (tilde-@-case-split-limitations-phrase (tagged-objectsp 'sr-limit ttree)
                      (tagged-objectsp 'case-limit ttree)
                      "  ")))
                (proofs-co state)
                state
                (term-evisc-tuple nil state)))))))))

(defun settled-down-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal clauses ttree pspv))
  state)