other-processes

(defun strip-final-digits1
  (lst)
  (cond ((null lst) (mv "" 0))
    ((member (car lst)
       '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)) (mv-let (str n)
        (strip-final-digits1 (cdr lst))
        (mv str
          (+ (let ((c (car lst)))
              (case c
                (#\0 0)
                (#\1 1)
                (#\2 2)
                (#\3 3)
                (#\4 4)
                (#\5 5)
                (#\6 6)
                (#\7 7)
                (#\8 8)
                (otherwise 9)))
            (* 10 n)))))
    (t (mv (coerce (reverse lst) 'string) 0))))

(defun strip-final-digits
  (str)
  (strip-final-digits1 (reverse (coerce str 'list))))

(defun assoc-ts-subsetp
  (ts alist)
  (cond ((null alist) nil)
    ((ts-subsetp ts (caar alist)) (car alist))
    (t (assoc-ts-subsetp ts (cdr alist)))))

(defun first-non-member-eq
  (lst1 lst2)
  (cond ((null lst1) nil)
    ((member-eq (car lst1) lst2) (first-non-member-eq (cdr lst1) lst2))
    (t (car lst1))))

(defun abbreviate-hyphenated-string1
  (str i maximum prev-c)
  (cond ((< i maximum) (let ((c (char str i)))
        (cond ((member c '(#\- #\_ #\. #\/ #\+)) (abbreviate-hyphenated-string1 str (1+ i) maximum nil))
          ((null prev-c) (cons c
              (abbreviate-hyphenated-string1 str (1+ i) maximum t)))
          (t (abbreviate-hyphenated-string1 str (1+ i) maximum c)))))
    ((characterp prev-c) (list prev-c))
    (t nil)))

(defun abbreviate-hyphenated-string
  (str)
  (let ((lst (abbreviate-hyphenated-string1 str 0 (length str) nil)))
    (coerce (cond ((or (null lst)
           (member (car lst) *suspiciously-first-numeric-chars*)) (cons #\V lst))
        (t lst))
      'string)))

(defun generate-variable-root1
  (term avoid-lst type-alist ens wrld)
  (mv-let (ts ttree)
    (type-set term t nil type-alist ens wrld nil nil nil)
    (declare (ignore ttree))
    (let* ((family (cdr (assoc-ts-subsetp ts *var-families-by-type*))) (var (first-non-member-eq family avoid-lst)))
      (cond (var (mv (symbol-name var) nil))
        (family (mv (symbol-name (car family)) 0))
        (t (mv (abbreviate-hyphenated-string (symbol-name (cond ((variablep term) 'z)
                  ((fquotep term) 'z)
                  ((flambda-applicationp term) 'z)
                  (t (ffn-symb term)))))
            nil))))))

(defun generate-variable-root
  (term avoid-lst type-alist ens wrld)
  (cond ((variablep term) (mv-let (str n)
        (strip-final-digits (symbol-name term))
        (mv str (1+ n))))
    ((fquotep term) (mv "CONST" 0))
    ((eq (ffn-symb term) 'car) (mv-let (str n)
        (generate-variable-root (fargn term 1)
          avoid-lst
          type-alist
          ens
          wrld)
        (mv str (or n 0))))
    ((eq (ffn-symb term) 'cdr) (mv-let (str n)
        (generate-variable-root (fargn term 1)
          avoid-lst
          type-alist
          ens
          wrld)
        (mv str (or n 0))))
    (t (generate-variable-root1 term avoid-lst type-alist ens wrld))))

(defun generate-variable
  (term avoid-lst type-alist ens wrld)
  (mv-let (str n)
    (generate-variable-root term avoid-lst type-alist ens wrld)
    (genvar (find-pkg-witness term) str n avoid-lst)))

(defun generate-variable-lst
  (term-lst avoid-lst type-alist ens wrld)
  (cond ((null term-lst) nil)
    (t (let ((var (generate-variable (car term-lst)
             avoid-lst
             type-alist
             ens
             wrld)))
        (cons var
          (generate-variable-lst (cdr term-lst)
            (cons var avoid-lst)
            type-alist
            ens
            wrld))))))

(defun occurs-nowhere-else
  (var args c i)
  (cond ((null args) t)
    ((int= c i) (occurs-nowhere-else var (cdr args) c (1+ i)))
    ((dumb-occur var (car args)) nil)
    (t (occurs-nowhere-else var (cdr args) c (1+ i)))))

(defun first-nomination
  (term votes nominations)
  (cons (cons term (cons term votes)) nominations))

(defun second-nomination
  (term votes nominations)
  (cond ((null nominations) nil)
    ((equal term (car (car nominations))) (cons (cons term (union-equal votes (cdr (car nominations))))
        (cdr nominations)))
    (t (cons (car nominations)
        (second-nomination term votes (cdr nominations))))))

(defun some-hyp-probably-nilp
  (hyps type-alist ens wrld)
  (cond ((null hyps) nil)
    (t (mv-let (knownp nilp ttree)
        (known-whether-nil (car hyps)
          type-alist
          ens
          (ok-to-force-ens ens)
          nil
          wrld
          nil)
        (declare (ignore ttree))
        (cond ((and knownp nilp) t)
          (t (some-hyp-probably-nilp (cdr hyps) type-alist ens wrld)))))))

(defun most-recent-enabled-elim-rule1
  (lst ens)
  (cond ((endp lst) nil)
    ((enabled-numep (access elim-rule (car lst) :nume) ens) (car lst))
    (t (most-recent-enabled-elim-rule1 (cdr lst) ens))))

(defun most-recent-enabled-elim-rule
  (fn wrld ens)
  (let ((lst (getpropc fn 'eliminate-destructors-rules nil wrld)))
    (and lst (most-recent-enabled-elim-rule1 lst ens))))

(defun nominate-destructor-candidate
  (term eliminables
    type-alist
    clause
    ens
    wrld
    votes
    nominations)
  (cond ((flambda-applicationp term) nominations)
    (t (let ((rule (most-recent-enabled-elim-rule (ffn-symb term) wrld ens)))
        (cond ((null rule) nominations)
          (t (let ((crucial-arg (nth (access elim-rule rule :crucial-position) (fargs term))))
              (cond ((variablep crucial-arg) (let* ((alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
                         (fargs term))) (inst-destructors (sublis-var-lst alist
                          (cons (access elim-rule rule :destructor-term)
                            (access elim-rule rule :destructor-terms))))
                      (pseudo-clause (sublis-expr-lst (pairlis$ inst-destructors nil) clause)))
                    (cond ((not (every-occurrence-equiv-hittablep-in-clausep (access elim-rule rule :equiv)
                           crucial-arg
                           pseudo-clause
                           ens
                           wrld)) nominations)
                      ((assoc-equal term nominations) (second-nomination term votes nominations))
                      ((member crucial-arg eliminables) (cond ((occurs-nowhere-else crucial-arg
                             (fargs term)
                             (access elim-rule rule :crucial-position)
                             0) (let* ((inst-hyps (sublis-var-lst alist (access elim-rule rule :hyps))))
                              (cond ((some-hyp-probably-nilp inst-hyps type-alist ens wrld) nominations)
                                (t (first-nomination term votes nominations)))))
                          (t nominations)))
                      (t nominations))))
                (t (nominate-destructor-candidate crucial-arg
                    eliminables
                    type-alist
                    clause
                    ens
                    wrld
                    (cons term votes)
                    nominations))))))))))

(defun sum-level-nos
  (lst wrld)
  (cond ((null lst) 0)
    (t (+ (if (flambda-applicationp (car lst))
          (max-level-no (lambda-body (ffn-symb (car lst))) wrld)
          (or (getpropc (ffn-symb (car lst)) 'level-no nil wrld) 0))
        (sum-level-nos (cdr lst) wrld)))))

(defun pick-highest-sum-level-nos
  (nominations wrld dterm max-score)
  (cond ((null nominations) dterm)
    (t (let ((score (sum-level-nos (cdr (car nominations)) wrld)))
        (cond ((> score max-score) (pick-highest-sum-level-nos (cdr nominations)
              wrld
              (caar nominations)
              score))
          (t (pick-highest-sum-level-nos (cdr nominations)
              wrld
              dterm
              max-score)))))))

(defun select-instantiated-elim-rule
  (clause type-alist eliminables ens wrld)
  (let ((nominations (nominate-destructor-candidates-lst clause
         eliminables
         type-alist
         clause
         ens
         wrld
         nil)))
    (cond ((null nominations) nil)
      (t (let* ((dterm (pick-highest-sum-level-nos nominations wrld nil -1)) (rule (most-recent-enabled-elim-rule (ffn-symb dterm) wrld ens))
            (alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
                (fargs dterm))))
          (change elim-rule
            rule
            :hyps (sublis-var-lst alist (access elim-rule rule :hyps))
            :lhs (sublis-var alist (access elim-rule rule :lhs))
            :rhs (sublis-var alist (access elim-rule rule :rhs))
            :destructor-term (sublis-var alist (access elim-rule rule :destructor-term))
            :destructor-terms (sublis-var-lst alist
              (access elim-rule rule :destructor-terms))))))))

(defun type-restriction-segment
  (cl terms vars type-alist ens wrld)
  (cond ((null terms) (mv nil nil nil))
    (t (mv-let (ts ttree1)
        (type-set (car terms)
          nil
          nil
          type-alist
          ens
          wrld
          nil
          nil
          nil)
        (mv-let (term ttree1)
          (convert-type-set-to-term (car terms) ts ens wrld ttree1)
          (let ((clauses (clausify (dumb-negate-lit term) nil t (sr-limit wrld))))
            (mv-let (lits restricted-vars ttree)
              (type-restriction-segment cl
                (cdr terms)
                (cdr vars)
                type-alist
                ens
                wrld)
              (cond ((null clauses) (mv (add-to-set-equal *nil* lits)
                    (cons (car vars) restricted-vars)
                    (cons-tag-trees ttree1 ttree)))
                ((and (null (cdr clauses)) (not (null (car clauses)))) (cond ((subsetp-equal (car clauses) cl) (mv lits restricted-vars ttree))
                    (t (mv (disjoin-clauses (car clauses) lits)
                        (cons (car vars) restricted-vars)
                        (cons-tag-trees ttree1 ttree)))))
                (t (mv lits restricted-vars ttree))))))))))

(defun apply-generalize-rule
  (gen-rule term ens)
  (cond ((not (enabled-numep (access generalize-rule gen-rule :nume) ens)) (mv nil nil))
    (t (mv-let (ans unify-subst)
        (subterm-one-way-unify (access generalize-rule gen-rule :formula)
          term)
        (cond ((null ans) (mv nil nil))
          ((free-varsp (access generalize-rule gen-rule :formula)
             unify-subst) (mv nil nil))
          (t (let ((inst-formula (sublis-var unify-subst
                   (access generalize-rule gen-rule :formula))))
              (cond ((ffnnamep (ffn-symb term) (subst-expr 'x term inst-formula)) (mv nil nil))
                (t (mv t inst-formula))))))))))

(defun generalize-rule-segment1
  (generalize-rules term ens)
  (cond ((null generalize-rules) (mv nil nil))
    (t (mv-let (ans formula)
        (apply-generalize-rule (car generalize-rules) term ens)
        (mv-let (formulas runes)
          (generalize-rule-segment1 (cdr generalize-rules) term ens)
          (cond (ans (mv (add-literal (dumb-negate-lit formula) formulas nil)
                (cons (access generalize-rule (car generalize-rules) :rune)
                  runes)))
            (t (mv formulas runes))))))))

(defun generalize-rule-segment
  (terms vars ens wrld)
  (cond ((null terms) (mv nil nil))
    (t (mv-let (segment1 runes1)
        (generalize-rule-segment1 (global-val 'generalize-rules wrld)
          (car terms)
          ens)
        (mv-let (segment2 alist)
          (generalize-rule-segment (cdr terms) (cdr vars) ens wrld)
          (cond ((null runes1) (mv segment2 alist))
            (t (mv (disjoin-clauses segment1 segment2)
                (cons (cons (car vars) runes1) alist)))))))))

(defun generalize1
  (cl type-alist terms vars ens wrld)
  (mv-let (tr-seg restricted-vars ttree)
    (type-restriction-segment cl terms vars type-alist ens wrld)
    (mv-let (gr-seg alist)
      (generalize-rule-segment terms vars ens wrld)
      (mv (sublis-expr-lst (pairlis$ terms vars)
          (disjoin-clauses tr-seg (disjoin-clauses gr-seg cl)))
        restricted-vars
        alist
        ttree))))

(defun apply-instantiated-elim-rule
  (rule cl type-alist avoid-vars ens wrld)
  (let* ((rune (access elim-rule rule :rune)) (hyps (access elim-rule rule :hyps))
      (lhs (access elim-rule rule :lhs))
      (rhs (access elim-rule rule :rhs))
      (dests (access elim-rule rule :destructor-terms))
      (negated-hyps (dumb-negate-lit-lst hyps)))
    (mv-let (contradictionp type-alist0 ttree0)
      (type-alist-clause negated-hyps
        nil
        nil
        type-alist
        ens
        wrld
        nil
        nil)
      (let* ((type-alist (if contradictionp
             type-alist
             type-alist0)) (cl-with-hyps (disjoin-clauses negated-hyps cl))
          (elim-vars (generate-variable-lst dests
              (all-vars1-lst cl-with-hyps avoid-vars)
              type-alist
              ens
              wrld))
          (alist (pairlis$ dests elim-vars))
          (generalized-lhs (sublis-expr alist lhs)))
        (cond (contradictionp (mv *true-clause*
              nil
              (list rune rhs generalized-lhs alist nil nil ttree0)))
          (t (let* ((cl-with-hyps (disjoin-clauses negated-hyps cl)) (elim-vars (generate-variable-lst dests
                    (all-vars1-lst cl-with-hyps avoid-vars)
                    type-alist
                    ens
                    wrld)))
              (mv-let (generalized-cl-with-hyps restricted-vars
                  var-to-runes-alist
                  ttree)
                (generalize1 cl-with-hyps
                  type-alist
                  dests
                  elim-vars
                  ens
                  wrld)
                (let* ((final-cl (subst-var-lst generalized-lhs rhs generalized-cl-with-hyps)) (actual-elim-vars (intersection-eq elim-vars (all-vars1-lst final-cl nil))))
                  (mv final-cl
                    actual-elim-vars
                    (list rune
                      rhs
                      generalized-lhs
                      alist
                      restricted-vars
                      var-to-runes-alist
                      (cons-tag-trees ttree0 ttree))))))))))))

(defun eliminate-destructors-clause1
  (cl eliminables avoid-vars ens wrld top-flg)
  (mv-let (contradictionp type-alist ttree)
    (type-alist-clause cl nil nil nil ens wrld nil nil)
    (declare (ignore ttree))
    (cond (contradictionp (mv (list cl) nil nil))
      (t (let ((rule (select-instantiated-elim-rule cl
               type-alist
               eliminables
               ens
               wrld)))
          (cond ((null rule) (mv (list cl) nil nil))
            (t (mv-let (new-clause elim-vars1 ele)
                (apply-instantiated-elim-rule rule
                  cl
                  type-alist
                  avoid-vars
                  ens
                  wrld)
                (let ((clauses1 (split-on-assumptions (access elim-rule rule :hyps) cl nil)))
                  (cond ((equal new-clause *true-clause*) (mv clauses1 elim-vars1 (list ele)))
                    (t (mv-let (clauses2 elim-vars2 elim-seq)
                        (eliminate-destructors-clause1 new-clause
                          (if top-flg
                            elim-vars1
                            (union-eq elim-vars1
                              (remove1-eq (access elim-rule rule :rhs) eliminables)))
                          avoid-vars
                          ens
                          wrld
                          nil)
                        (mv (conjoin-clause-sets clauses1 clauses2)
                          (union-eq elim-vars1 elim-vars2)
                          (cons ele elim-seq))))))))))))))

(defun owned-vars
  (process mine-flg history)
  (cond ((null history) nil)
    ((eq mine-flg
       (eq (access history-entry (car history) :processor) process)) (union-eq (tagged-object 'variables
          (access history-entry (car history) :ttree))
        (owned-vars process mine-flg (cdr history))))
    (t (owned-vars process mine-flg (cdr history)))))

(defun ens-from-pspv
  (pspv)
  (access rewrite-constant
    (access prove-spec-var pspv :rewrite-constant)
    :current-enabled-structure))

(defun eliminate-destructors-clause
  (clause hist pspv wrld state)
  (declare (ignore state))
  (mv-let (clauses elim-vars elim-seq)
    (eliminate-destructors-clause1 clause
      (set-difference-eq (all-vars1-lst clause nil)
        (owned-vars 'eliminate-destructors-clause t hist))
      (owned-vars 'eliminate-destructors-clause nil hist)
      (ens-from-pspv pspv)
      wrld
      t)
    (cond (elim-seq (mv 'hit
          clauses
          (add-to-tag-tree! 'variables
            elim-vars
            (add-to-tag-tree! 'elim-sequence elim-seq nil))
          pspv))
      (t (mv 'miss nil nil nil)))))

(defun prettyify-clause1
  (cl wrld)
  (cond ((null (cdr cl)) nil)
    (t (cons (untranslate (dumb-negate-lit (car cl)) t wrld)
        (prettyify-clause1 (cdr cl) wrld)))))

(defun prettyify-clause2
  (cl wrld)
  (cond ((null cl) nil)
    ((null (cdr cl)) (untranslate (car cl) t wrld))
    ((null (cddr cl)) (list 'implies
        (untranslate (dumb-negate-lit (car cl)) t wrld)
        (untranslate (cadr cl) t wrld)))
    (t (list 'implies
        (cons 'and (prettyify-clause1 cl wrld))
        (untranslate (car (last cl)) t wrld)))))

(defun prettyify-clause
  (cl let*-abstractionp wrld)
  (if let*-abstractionp
    (mv-let (vars terms)
      (maximal-multiples (cons 'list cl) let*-abstractionp)
      (cond ((null vars) (prettyify-clause2 cl wrld))
        (t `(let* ,(LISTLIS VARS (UNTRANSLATE-LST (ALL-BUT-LAST TERMS) NIL WRLD))
            ,(PRETTYIFY-CLAUSE2 (CDR (CAR (LAST TERMS))) WRLD)))))
    (prettyify-clause2 cl wrld)))

(defun prettyify-clause-lst
  (clauses let*-abstractionp wrld)
  (cond ((null clauses) nil)
    (t (cons (prettyify-clause (car clauses) let*-abstractionp wrld)
        (prettyify-clause-lst (cdr clauses) let*-abstractionp wrld)))))

(defun prettyify-clause-set
  (clauses let*-abstractionp wrld)
  (cond ((null clauses) t)
    ((null (cdr clauses)) (prettyify-clause (car clauses) let*-abstractionp wrld))
    (t (cons 'and
        (prettyify-clause-lst clauses let*-abstractionp wrld)))))

(defun tilde-*-elim-phrase/alist1
  (alist wrld)
  (cond ((null alist) nil)
    (t (cons (msg "~p0 by ~x1"
          (untranslate (caar alist) nil wrld)
          (cdar alist))
        (tilde-*-elim-phrase/alist1 (cdr alist) wrld)))))

(defun tilde-*-elim-phrase/alist
  (alist wrld)
  (list* ""
    " and ~@*"
    ", ~@*"
    ", ~@*"
    (tilde-*-elim-phrase/alist1 alist wrld)
    nil))

(defun tilde-*-elim-phrase3
  (var-to-runes-alist)
  (cond ((null var-to-runes-alist) nil)
    (t (cons (msg "noting the condition imposed on ~x0 by the ~
                       generalization rule~#1~[~/s~] ~&1"
          (caar var-to-runes-alist)
          (strip-base-symbols (cdar var-to-runes-alist)))
        (tilde-*-elim-phrase3 (cdr var-to-runes-alist))))))

(defun tilde-*-elim-phrase2
  (alist restricted-vars var-to-runes-alist ttree wrld)
  (list* ""
    "~@*"
    "~@* and "
    "~@*, "
    (append (list (msg "~*0" (tilde-*-elim-phrase/alist alist wrld)))
      (cond (restricted-vars (let ((simp-phrase (tilde-*-simp-phrase ttree)))
            (cond ((null (cdr restricted-vars)) (list (msg "restrict the type of the new ~
                                  variable ~&0 to be that of the term ~
                                  it replaces~#1~[~/, as established ~
                                  by ~*2~]"
                    restricted-vars
                    (if (nth 4 simp-phrase)
                      1
                      0)
                    simp-phrase)))
              (t (list (msg "restrict the types of the new ~
                                    variables ~&0 to be those of the ~
                                    terms they replace~#1~[~/, as ~
                                    established by ~*2~]"
                    restricted-vars
                    (if (nth 4 simp-phrase)
                      1
                      0)
                    simp-phrase))))))
        (t nil))
      (tilde-*-elim-phrase3 var-to-runes-alist))
    nil))

(defun tilde-*-elim-phrase1
  (lst i already-used wrld)
  (cond ((null lst) nil)
    (t (cons (cons "(~xi) ~#f~[Use~/Finally, use~] ~#a~[~x0~/~x0, again,~] to ~
              replace ~x1 by ~p2~*3.  "
          (list (cons #\i i)
            (cons #\f
              (if (and (null (cdr lst)) (> i 2))
                1
                0))
            (cons #\a
              (if (member-equal (nth 0 (car lst)) already-used)
                (if (member-equal (nth 0 (car lst))
                    (cdr (member-equal (nth 0 (car lst)) already-used)))
                  0
                  1)
                0))
            (cons #\0 (base-symbol (nth 0 (car lst))))
            (cons #\1 (nth 1 (car lst)))
            (cons #\2 (untranslate (nth 2 (car lst)) nil wrld))
            (cons #\3
              (tilde-*-elim-phrase2 (nth 3 (car lst))
                (nth 4 (car lst))
                (nth 5 (car lst))
                (nth 6 (car lst))
                wrld))))
        (tilde-*-elim-phrase1 (cdr lst)
          (1+ i)
          (cons (nth 0 (car lst)) already-used)
          wrld)))))

(defun tilde-*-elim-phrase
  (lst wrld)
  (list* ""
    "~@*"
    "~@*"
    "~@*"
    (tilde-*-elim-phrase1 lst 1 nil wrld)
    nil))

(defun tilde-*-untranslate-lst-phrase
  (lst final-punct flg wrld)
  (list* ""
    (cond ((eql final-punct #\.) "~p*.")
      ((eql final-punct #\,) "~p*,")
      (final-punct (coerce (append '(#\~ #\p #\*) (list final-punct)) 'string))
      (t "~p*"))
    "~p* and "
    "~p*, "
    (untranslate-lst lst flg wrld)
    nil))

(defun eliminate-destructors-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal pspv))
  (let ((lst (tagged-object 'elim-sequence ttree)) (n (length clauses))
      (wrld (w state)))
    (cond ((null (cdr lst)) (fms "The destructor term~#p~[~/s~] ~*0 can be eliminated by using ~x1 ~
             to replace ~p2 by ~p3~*4.  ~#5~[All the clauses produced are ~
             tautological.~/This produces the following goal.~/This produces ~
             the following ~n6 goals.~]~|"
          (list (cons #\p (nth 3 (car lst)))
            (cons #\0
              (tilde-*-untranslate-lst-phrase (strip-cars (nth 3 (car lst)))
                nil
                nil
                wrld))
            (cons #\1 (base-symbol (nth 0 (car lst))))
            (cons #\2 (nth 1 (car lst)))
            (cons #\3 (untranslate (nth 2 (car lst)) nil wrld))
            (cons #\4
              (tilde-*-elim-phrase2 (nth 3 (car lst))
                (nth 4 (car lst))
                (nth 5 (car lst))
                (nth 6 (car lst))
                wrld))
            (cons #\5 (zero-one-or-more n))
            (cons #\6 n))
          (proofs-co state)
          state
          (term-evisc-tuple nil state)))
      (t (fms "The destructor term~#p~[~/s~] ~*0 can be eliminated.  ~
             Furthermore, ~#p~[that term is~/those terms are~] at the root of ~
             a chain of ~n1 rounds of destructor elimination.  ~*2These steps ~
             produce ~#3~[no nontautological goals~/the following goal~/the ~
             following ~n4 goals~].~|"
          (list (cons #\p (nth 3 (car lst)))
            (cons #\0
              (tilde-*-untranslate-lst-phrase (strip-cars (nth 3 (car lst)))
                nil
                nil
                wrld))
            (cons #\1 (length lst))
            (cons #\2 (tilde-*-elim-phrase lst wrld))
            (cons #\3 (zero-one-or-more n))
            (cons #\4 n))
          (proofs-co state)
          state
          (term-evisc-tuple nil state))))))

(defun almost-quotep
  (term)
  (and (nvariablep term) (almost-quotep1 term)))

(defun destructor-applied-to-varsp
  (term ens wrld)
  (cond ((variablep term) nil)
    ((fquotep term) nil)
    ((flambda-applicationp term) nil)
    (t (and (all-variablep (fargs term))
        (most-recent-enabled-elim-rule (ffn-symb term) wrld ens)))))

(defun dumb-occur-lst-except
  (term lst lit)
  (cond ((null lst) nil)
    ((equal lit (car lst)) (dumb-occur-lst term (cdr lst)))
    (t (or (dumb-occur term (car lst))
        (dumb-occur-lst-except term (cdr lst) lit)))))

(defun fertilize-feasible
  (lit cl hist term ens wrld)
  (and (not (almost-quotep term))
    (not (destructor-applied-to-varsp term ens wrld))
    (dumb-occur-lst-except term cl lit)
    (every-occurrence-equiv-hittablep-in-clausep (ffn-symb (fargn lit 1))
      term
      cl
      ens
      wrld)
    (not (already-used-by-fertilize-clausep lit hist t))))

(defun first-fertilize-lit
  (lst cl hist ens wrld)
  (cond ((null lst) (mv nil nil nil nil nil nil))
    (t (let ((lit (car lst)))
        (case-match lit
          (('not (equiv lhs rhs)) (cond ((equivalence-relationp equiv wrld) (cond ((fertilize-feasible lit cl hist lhs ens wrld) (cond ((fertilize-feasible lit cl hist rhs ens wrld) (cond ((< (fertilize-complexity lhs wrld)
                             (fertilize-complexity rhs wrld)) (mv 'left-for-right lit equiv lhs rhs (len (cdr lst))))
                          (t (mv 'right-for-left lit equiv lhs rhs (len (cdr lst))))))
                      (t (mv 'right-for-left lit equiv lhs rhs (len (cdr lst))))))
                  ((fertilize-feasible lit cl hist rhs ens wrld) (mv 'left-for-right lit equiv lhs rhs (len (cdr lst))))
                  (t (first-fertilize-lit (cdr lst) cl hist ens wrld))))
              (t (first-fertilize-lit (cdr lst) cl hist ens wrld))))
          (& (first-fertilize-lit (cdr lst) cl hist ens wrld)))))))

(defun cross-fertilizep/c
  (equiv cl direction lhs1 rhs1)
  (cond ((null cl) nil)
    ((and (nvariablep (car cl))
       (not (fquotep (car cl)))
       (equal (ffn-symb (car cl)) equiv)
       (if (eq direction 'left-for-right)
         (dumb-occur rhs1 (fargn (car cl) 2))
         (dumb-occur lhs1 (fargn (car cl) 1)))) t)
    (t (cross-fertilizep/c equiv (cdr cl) direction lhs1 rhs1))))

(defun cross-fertilizep/d
  (equiv cl direction lhs1 rhs1)
  (cond ((null cl) nil)
    ((and (nvariablep (car cl))
       (not (fquotep (car cl)))
       (equal (ffn-symb (car cl)) equiv)
       (if (eq direction 'left-for-right)
         (dumb-occur rhs1 (fargn (car cl) 1))
         (dumb-occur lhs1 (fargn (car cl) 2)))) t)
    (t (cross-fertilizep/d equiv (cdr cl) direction lhs1 rhs1))))

(defun cross-fertilizep
  (equiv cl pspv direction lhs1 rhs1)
  (and (not (quotep lhs1))
    (not (quotep rhs1))
    (assoc-eq 'being-proved-by-induction
      (access prove-spec-var pspv :pool))
    (not (member-eq 'generalize-clause
        (cdr (assoc-eq :do-not (access prove-spec-var pspv :hint-settings)))))
    (cross-fertilizep/c equiv cl direction lhs1 rhs1)
    (cross-fertilizep/d equiv cl direction lhs1 rhs1)))

(defun delete-from-ttree
  (tag val ttree)
  (let ((objects (tagged-objects tag ttree)))
    (cond (objects (cond ((member-equal val objects) (let ((new-objects (remove1-equal val objects)) (new-ttree (remove-tag-from-tag-tree! tag ttree)))
              (cond (new-objects (extend-tag-tree tag new-objects new-ttree))
                (t new-ttree))))
          (t ttree)))
      (t ttree))))

(defun fertilize-clause1
  (cl lit1
    equiv
    lhs1
    rhs1
    direction
    cross-fert-flg
    delete-lit-flg
    ens
    wrld
    state
    ttree)
  (cond ((null cl) (mv nil ttree))
    (t (let* ((lit2 (car cl)) (lit2-is-lit1p (equal lit2 lit1)))
        (mv-let (hitp new-lit2 ttree)
          (cond (lit2-is-lit1p (mv nil lit2 ttree))
            ((or (not cross-fert-flg)
               (case-match lit2
                 (('not (equiv-sym & &)) (equal equiv-sym equiv))
                 (& nil))) (cond ((eq direction 'left-for-right) (subst-equiv-expr equiv
                    lhs1
                    rhs1
                    *geneqv-iff*
                    lit2
                    ens
                    wrld
                    state
                    ttree))
                (t (subst-equiv-expr equiv
                    rhs1
                    lhs1
                    *geneqv-iff*
                    lit2
                    ens
                    wrld
                    state
                    ttree))))
            (t (case-match lit2
                ((equiv-sym lhs2 rhs2) (cond ((not (equal equiv-sym equiv)) (mv nil lit2 ttree))
                    ((eq direction 'left-for-right) (mv-let (hitp new-rhs2 ttree)
                        (subst-equiv-expr equiv
                          lhs1
                          rhs1
                          (cadr (geneqv-lst equiv *geneqv-iff* ens wrld))
                          rhs2
                          ens
                          wrld
                          state
                          ttree)
                        (declare (ignore hitp))
                        (mv nil (mcons-term* equiv lhs2 new-rhs2) ttree)))
                    (t (mv-let (hitp new-lhs2 ttree)
                        (subst-equiv-expr equiv
                          rhs1
                          lhs1
                          (car (geneqv-lst equiv *geneqv-iff* ens wrld))
                          lhs2
                          ens
                          wrld
                          state
                          ttree)
                        (declare (ignore hitp))
                        (mv nil (mcons-term* equiv new-lhs2 rhs2) ttree)))))
                (& (mv nil lit2 ttree)))))
          (declare (ignore hitp))
          (mv-let (new-tail ttree)
            (fertilize-clause1 (cdr cl)
              lit1
              equiv
              lhs1
              rhs1
              direction
              cross-fert-flg
              (if lit2-is-lit1p
                nil
                delete-lit-flg)
              ens
              wrld
              state
              ttree)
            (cond (lit2-is-lit1p (cond (delete-lit-flg (mv new-tail
                      (cond ((eq direction 'left-for-right) (add-binding-to-tag-tree rhs1 lhs1 ttree))
                        (t (add-binding-to-tag-tree lhs1 rhs1 ttree)))))
                  (t (mv-let (not-flg atm)
                      (strip-not lit2)
                      (prog2$ (or not-flg
                          (er hard
                            'fertilize-clause1
                            "We had thought that we only ~
                                            fertilize with negated literals, ~
                                            unlike ~x0!"
                            new-lit2))
                        (prog2$ (or (equal lit2 new-lit2)
                            (er hard
                              'fertilize-clause1
                              "Internal error in ~
                                             fertilize-clause1!~|Old lit2: ~
                                             ~x0.~|New lit2: ~x1"
                              lit2
                              new-lit2))
                          (mv (cons (mcons-term* 'not (mcons-term* 'hide atm)) new-tail)
                            ttree)))))))
              (t (mv (cons new-lit2 new-tail) ttree)))))))))

(defun fertilize-clause
  (cl-id cl hist pspv wrld state)
  (mv-let (direction lit equiv lhs rhs len-tail)
    (first-fertilize-lit cl cl hist (ens-from-pspv pspv) wrld)
    (cond ((null direction) (mv 'miss nil nil nil))
      (t (let ((cross-fert-flg (cross-fertilizep equiv cl pspv direction lhs rhs)) (delete-lit-flg (and (not (quotep lhs))
                (not (quotep rhs))
                (assoc-eq 'being-proved-by-induction
                  (access prove-spec-var pspv :pool)))))
          (mv-let (new-cl ttree)
            (fertilize-clause1 cl
              lit
              equiv
              lhs
              rhs
              direction
              cross-fert-flg
              delete-lit-flg
              (ens-from-pspv pspv)
              wrld
              state
              nil)
            (mv 'hit
              (list new-cl)
              (add-to-tag-tree! 'literal
                lit
                (add-to-tag-tree! 'hyp-phrase
                  (tilde-@-hyp-phrase len-tail cl)
                  (add-to-tag-tree! 'cross-fert-flg
                    cross-fert-flg
                    (add-to-tag-tree! 'equiv
                      equiv
                      (add-to-tag-tree! 'bullet
                        (if (eq direction 'left-for-right)
                          lhs
                          rhs)
                        (add-to-tag-tree! 'target
                          (if (eq direction 'left-for-right)
                            rhs
                            lhs)
                          (add-to-tag-tree! 'clause-id
                            cl-id
                            (add-to-tag-tree! 'delete-lit-flg
                              delete-lit-flg
                              (if delete-lit-flg
                                ttree
                                (push-lemma (fn-rune-nume 'hide nil nil wrld) ttree))))))))))
              pspv)))))))

(defun fertilize-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal pspv clauses))
  (let* ((hyp-phrase (tagged-object 'hyp-phrase ttree)) (wrld (w state))
      (ttree (delete-from-ttree 'lemma
          (fn-rune-nume 'hide nil nil wrld)
          ttree)))
    (fms "We now use ~@0 by ~#1~[substituting~/cross-fertilizing~] ~p2 for ~p3 ~
          and ~#4~[hiding~/throwing away~] the ~@5.~#6~[~/  The validity of ~
          this substitution relies upon ~*7.~]  This produces~|"
      (list (cons #\0 hyp-phrase)
        (cons #\1
          (if (tagged-object 'cross-fert-flg ttree)
            1
            0))
        (cons #\2
          (untranslate (tagged-object 'bullet ttree) nil wrld))
        (cons #\3
          (untranslate (tagged-object 'target ttree) nil wrld))
        (cons #\4
          (if (tagged-object 'delete-lit-flg ttree)
            1
            0))
        (cons #\5
          (if (and (consp hyp-phrase) (null (cdr hyp-phrase)))
            "conclusion"
            "hypothesis"))
        (cons #\6
          (if (tagged-objectsp 'lemma ttree)
            1
            0))
        (cons #\7 (tilde-*-simp-phrase ttree)))
      (proofs-co state)
      state
      (term-evisc-tuple nil state))))

(defun collectable-fnp
  (fn ens wrld)
  (cond ((flambdap fn) nil)
    ((eq fn 'cons) nil)
    (t (not (most-recent-enabled-elim-rule fn wrld ens)))))

(defun dumb-fn-count-1
  (flg x acc)
  (declare (xargs :guard (and (if flg
          (pseudo-term-listp x)
          (pseudo-termp x))
        (natp acc))))
  (cond (flg (cond ((null x) acc)
        (t (dumb-fn-count-1 t
            (cdr x)
            (dumb-fn-count-1 nil (car x) acc)))))
    ((or (variablep x) (fquotep x)) acc)
    (t (dumb-fn-count-1 t (fargs x) (1+ acc)))))

(defun dumb-fn-count (x) (dumb-fn-count-1 nil x 0))

(defun smallest-common-subterms
  (term1 term2 ens wrld ans)
  (mv-let (ans potential)
    (cond ((> (dumb-fn-count term1) (dumb-fn-count term2)) (smallest-common-subterms1 term2 term1 ens wrld ans))
      (t (smallest-common-subterms1 term1 term2 ens wrld ans)))
    (declare (ignore potential))
    ans))

(defun generalizing-relationp
  (term wrld)
  (mv-let (neg-flg atm)
    (strip-not term)
    (declare (ignore neg-flg))
    (cond ((or (variablep atm)
         (fquotep atm)
         (flambda-applicationp atm)) (mv nil nil nil))
      ((or (eq (ffn-symb atm) 'equal)
         (eq (ffn-symb atm) '<)
         (equivalence-relationp (ffn-symb atm) wrld)) (mv t (fargn atm 1) (fargn atm 2)))
      (t (mv nil nil nil)))))

(defun generalizable-terms-across-relations
  (cl ens wrld ans)
  (cond ((null cl) ans)
    (t (mv-let (genp lhs rhs)
        (generalizing-relationp (car cl) wrld)
        (generalizable-terms-across-relations (cdr cl)
          ens
          wrld
          (if genp
            (smallest-common-subterms lhs rhs ens wrld ans)
            ans))))))

(defun generalizable-terms-across-literals1
  (lit1 cl ens wrld ans)
  (cond ((null cl) ans)
    (t (generalizable-terms-across-literals1 lit1
        (cdr cl)
        ens
        wrld
        (smallest-common-subterms lit1 (car cl) ens wrld ans)))))

(defun generalizable-terms-across-literals
  (cl ens wrld ans)
  (cond ((null cl) ans)
    (t (generalizable-terms-across-literals (cdr cl)
        ens
        wrld
        (generalizable-terms-across-literals1 (car cl)
          (cdr cl)
          ens
          wrld
          ans)))))

(defun generalizable-terms
  (cl ens wrld)
  (generalizable-terms-across-literals cl
    ens
    wrld
    (generalizable-terms-across-relations cl ens wrld nil)))

(defun generalize-clause
  (cl hist pspv wrld state)
  (declare (ignore state))
  (cond ((not (assoc-eq 'being-proved-by-induction
         (access prove-spec-var pspv :pool))) (mv 'miss nil nil nil))
    (t (let* ((ens (ens-from-pspv pspv)) (terms (generalizable-terms cl ens wrld)))
        (cond ((null terms) (mv 'miss nil nil nil))
          (t (mv-let (contradictionp type-alist ttree)
              (type-alist-clause cl nil nil nil ens wrld nil nil)
              (declare (ignore ttree))
              (cond (contradictionp (mv 'miss nil nil nil))
                (t (let ((gen-vars (generate-variable-lst terms
                         (all-vars1-lst cl (owned-vars 'generalize-clause nil hist))
                         type-alist
                         ens
                         wrld)))
                    (mv-let (generalized-cl restricted-vars var-to-runes-alist ttree)
                      (generalize1 cl type-alist terms gen-vars ens wrld)
                      (mv 'hit
                        (list generalized-cl)
                        (add-to-tag-tree! 'variables
                          gen-vars
                          (add-to-tag-tree! 'terms
                            terms
                            (add-to-tag-tree! 'restricted-vars
                              restricted-vars
                              (add-to-tag-tree! 'var-to-runes-alist
                                var-to-runes-alist
                                (add-to-tag-tree! 'ts-ttree ttree nil)))))
                        pspv))))))))))))

(defun tilde-*-gen-phrase/alist1
  (alist wrld)
  (cond ((null alist) nil)
    (t (cons (msg "~p0 by ~x1"
          (untranslate (caar alist) nil wrld)
          (cdar alist))
        (tilde-*-gen-phrase/alist1 (cdr alist) wrld)))))

(defun tilde-*-gen-phrase/alist
  (alist wrld)
  (list* ""
    "~@*"
    "~@* and "
    "~@*, "
    (tilde-*-gen-phrase/alist1 alist wrld)
    nil))

(defun tilde-*-gen-phrase
  (alist restricted-vars var-to-runes-alist ttree wrld)
  (list* ""
    "~@*"
    "~@* and "
    "~@*, "
    (append (list (msg "~*0" (tilde-*-gen-phrase/alist alist wrld)))
      (cond (restricted-vars (let* ((runes (tagged-objects 'lemma ttree)) (primitive-type-reasoningp (member-equal *fake-rune-for-type-set* runes))
              (symbols (strip-base-symbols (remove1-equal *fake-rune-for-type-set* runes))))
            (cond ((member-eq nil symbols) (er hard
                  'tilde-*-gen-phrase
                  "A fake rune other than ~
                          *fake-rune-for-type-set* was found in the ~
                          ts-ttree generated by generalize-clause.  ~
                          The list of runes in the ttree is ~x0."
                  runes))
              ((null (cdr restricted-vars)) (list (msg "restricting the type of the new ~
                                 variable ~&0 to be that of the term ~
                                 it replaces~#1~[~/, as established ~
                                 by primitive type reasoning~/, as ~
                                 established by ~&2~/, as established ~
                                 by primitive type reasoning and ~&2~]"
                    restricted-vars
                    (cond ((and symbols primitive-type-reasoningp) 3)
                      (symbols 2)
                      (primitive-type-reasoningp 1)
                      (t 0))
                    symbols)))
              (t (list (msg "restricting the types of the new ~
                                   variables ~&0 to be those of the ~
                                   terms they replace~#1~[~/, as ~
                                   established by primitive type ~
                                   reasoning~/, as established by ~
                                   ~&2~/, as established by primitive ~
                                   type reasoning and ~&2~]"
                    restricted-vars
                    (cond ((and symbols primitive-type-reasoningp) 3)
                      (symbols 2)
                      (primitive-type-reasoningp 1)
                      (t 0))
                    symbols))))))
        (t nil))
      (tilde-*-elim-phrase3 var-to-runes-alist))
    nil))

(defun generalize-clause-msg1
  (signal clauses ttree pspv state)
  (declare (ignore signal pspv clauses))
  (fms "We generalize this conjecture, replacing ~*0.  This produces~|"
    (list (cons #\0
        (tilde-*-gen-phrase (pairlis$ (tagged-object 'terms ttree)
            (tagged-object 'variables ttree))
          (tagged-object 'restricted-vars ttree)
          (tagged-object 'var-to-runes-alist ttree)
          (tagged-object 'ts-ttree ttree)
          (w state))))
    (proofs-co state)
    state
    (term-evisc-tuple nil state)))