tau

(defun almost-lexorder-singletons
  (x y)
  (cond ((eq (car x) nil) t)
    ((eq (car y) nil) nil)
    (t (lexorder (car x) (car y)))))

(defun member-nil-neg-evgs
  (neg-evg-lst)
  (and (consp neg-evg-lst) (eq (car (car neg-evg-lst)) nil)))

(defun member-neg-evgs1
  (evg neg-evg-lst)
  (cond ((endp neg-evg-lst) nil)
    ((lexorder (car (car neg-evg-lst)) evg) (or (equal evg (car (car neg-evg-lst)))
        (member-neg-evgs1 evg (cdr neg-evg-lst))))
    (t nil)))

(defun member-neg-evgs
  (x neg-evg-lst)
  (cond ((endp neg-evg-lst) nil)
    ((equal (car x) (car (car neg-evg-lst))) t)
    ((eq (car x) nil) nil)
    (t (member-neg-evgs1 (car x) (cdr neg-evg-lst)))))

(defun insert-neg-evgs1
  (evg x neg-evg-lst)
  (cond ((endp neg-evg-lst) (cons x nil))
    ((lexorder (car (car neg-evg-lst)) evg) (cons (car neg-evg-lst)
        (insert-neg-evgs1 evg x (cdr neg-evg-lst))))
    (t (cons x neg-evg-lst))))

(defun insert-neg-evgs
  (x neg-evg-lst)
  (cond ((endp neg-evg-lst) (cons x neg-evg-lst))
    ((eq (car x) nil) (cons x neg-evg-lst))
    ((eq (car (car neg-evg-lst)) nil) (cons (car neg-evg-lst)
        (insert-neg-evgs1 (car x) x (cdr neg-evg-lst))))
    (t (insert-neg-evgs1 (car x) x neg-evg-lst))))

(defun merge-car-<
  (l1 l2)
  (cond ((null l1) l2)
    ((null l2) l1)
    ((< (car (car l1)) (car (car l2))) (cons (car l1) (merge-car-< (cdr l1) l2)))
    (t (cons (car l2) (merge-car-< l1 (cdr l2))))))

(defun merge-sort-car-<
  (l)
  (cond ((null (cdr l)) l)
    (t (merge-car-< (merge-sort-car-< (evens l))
        (merge-sort-car-< (odds l))))))

(defun merge-cadr-<
  (l1 l2)
  (cond ((null l1) l2)
    ((null l2) l1)
    ((< (cadr (car l1)) (cadr (car l2))) (cons (car l1) (merge-cadr-< (cdr l1) l2)))
    (t (cons (car l2) (merge-cadr-< l1 (cdr l2))))))

(defun merge-sort-cadr-<
  (l)
  (cond ((null (cdr l)) l)
    (t (merge-cadr-< (merge-sort-cadr-< (evens l))
        (merge-sort-cadr-< (odds l))))))

(defun strip-caddrs
  (x)
  (declare (xargs :guard (all->=-len x 3)))
  (cond ((endp x) nil)
    (t (cons (caddar x) (strip-caddrs (cdr x))))))

(defun unprettyify/add-hyps-to-pairs
  (hyps lst)
  (cond ((null lst) nil)
    (t (cons (cons (append hyps (caar lst)) (cdar lst))
        (unprettyify/add-hyps-to-pairs hyps (cdr lst))))))

(defun unprettyify
  (term)
  (case-match term
    (('if t1 t2 t3) (cond ((equal t2 *nil*) (append (unprettyify (dumb-negate-lit t1)) (unprettyify t3)))
        ((equal t3 *nil*) (append (unprettyify t1) (unprettyify t2)))
        (t (list (cons nil term)))))
    (('implies t1 t2) (unprettyify/add-hyps-to-pairs (flatten-ands-in-lit t1)
        (unprettyify t2)))
    ((('lambda vars body) . args) (unprettyify (subcor-var vars args body)))
    (& (list (cons nil term)))))

(defun reprettyify
  (hyps concl wrld)
  (cond ((null hyps) (untranslate concl t wrld))
    ((null (cdr hyps)) `(implies ,(UNTRANSLATE (CAR HYPS) T WRLD)
        ,(UNTRANSLATE CONCL T WRLD)))
    (t `(implies (and ,@(UNTRANSLATE-LST HYPS T WRLD))
        ,(UNTRANSLATE CONCL T WRLD)))))

(defun convert-returned-vars-to-term-lst
  (term vars)
  (cond ((null vars) nil)
    (t (cons (mcons-term* 'equal term (car vars))
        (convert-returned-vars-to-term-lst term (cdr vars))))))

(defun implicate
  (t1 t2)
  (declare (xargs :guard (and (pseudo-termp t1) (pseudo-termp t2))))
  (cond ((equal t1 *t*) t2)
    ((equal t1 *nil*) *t*)
    ((equal t2 *t*) *t*)
    ((equal t2 *nil*) (dumb-negate-lit t1))
    (t (mcons-term* 'implies t1 t2))))

(defun convert-type-set-to-term-lst
  (ts rules ens lst ttree)
  (cond ((null rules) (mv (reverse lst) ttree))
    ((and (enabled-numep (access type-set-inverter-rule (car rules) :nume)
         ens)
       (ts= (access type-set-inverter-rule (car rules) :ts)
         (ts-intersection (access type-set-inverter-rule (car rules) :ts)
           ts))) (convert-type-set-to-term-lst (ts-intersection ts
          (ts-complement (access type-set-inverter-rule (car rules) :ts)))
        (cdr rules)
        ens
        (add-to-set-equal (conjoin (access type-set-inverter-rule (car rules) :terms))
          lst)
        (push-lemma (access type-set-inverter-rule (car rules) :rune)
          ttree)))
    (t (convert-type-set-to-term-lst ts (cdr rules) ens lst ttree))))

(defun convert-type-set-to-term1
  (x ts flg ens w ttree)
  (cond ((ts= ts *ts-unknown*) (mv *t* ttree))
    ((and flg (ts= ts *ts-t*) (ts-booleanp x ens w)) (mv x ttree))
    ((ts-complementp ts) (mv-let (lst ttree)
        (convert-type-set-to-term-lst (ts-complement ts)
          (global-val 'type-set-inverter-rules w)
          ens
          nil
          ttree)
        (mv (subst-var x 'x (conjoin (dumb-negate-lit-lst lst)))
          ttree)))
    (t (mv-let (lst ttree)
        (convert-type-set-to-term-lst ts
          (global-val 'type-set-inverter-rules w)
          ens
          nil
          ttree)
        (mv (subst-var x 'x (disjoin lst)) ttree)))))

(defun convert-type-set-to-term
  (x ts ens w ttree)
  (convert-type-set-to-term1 x ts nil ens w ttree))

(defun convert-type-prescription-to-term
  (tp ens wrld)
  (mv-let (concl ttree)
    (convert-type-set-to-term (access type-prescription tp :term)
      (access type-prescription tp :basic-ts)
      ens
      wrld
      nil)
    (mv (implicate (conjoin (access type-prescription tp :hyps))
        (disjoin (cons concl
            (convert-returned-vars-to-term-lst (access type-prescription tp :term)
              (access type-prescription tp :vars)))))
      ttree)))

(defun all-runes-in-var-to-runes-alist
  (alist ans)
  (cond ((null alist) ans)
    (t (all-runes-in-var-to-runes-alist (cdr alist)
        (union-equal (cdr (car alist)) ans)))))

(defun all-runes-in-var-to-runes-alist-lst
  (lst ans)
  (cond ((endp lst) ans)
    (t (all-runes-in-var-to-runes-alist-lst (cdr lst)
        (all-runes-in-var-to-runes-alist (car lst) ans)))))

(defun union-equal-removing-duplicates
  (x y)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) y)
    (t (union-equal-removing-duplicates (cdr x)
        (add-to-set-equal (car x) y)))))

(defun tau-empty-intervalp
  (int)
  (and int
    (access tau-interval int :lo)
    (access tau-interval int :hi)
    (if (or (access tau-interval int :lo-rel)
        (access tau-interval int :hi-rel))
      (<= (access tau-interval int :hi)
        (access tau-interval int :lo))
      (< (access tau-interval int :hi)
        (access tau-interval int :lo)))))

(defun <?-number-v-rational
  (rel x k)
  (cond ((real/rationalp x) (if rel
        (< x k)
        (<= x k)))
    (t (or (< (realpart x) k)
        (and (= (realpart x) k) (< (imagpart x) 0))))))

(defun <?-rational-v-number
  (rel k x)
  (cond ((real/rationalp x) (if rel
        (< k x)
        (<= k x)))
    (t (or (< k (realpart x))
        (and (= k (realpart x)) (< 0 (imagpart x)))))))

(defun eval-tau-interval1
  (interval x)
  (let ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi)))
    (and (or (null lo)
        (<?-rational-v-number (access tau-interval interval :lo-rel)
          lo
          x))
      (or (null hi)
        (<?-number-v-rational (access tau-interval interval :hi-rel)
          x
          hi)))))

(defun eval-tau-interval
  (interval evg)
  (cond ((null interval) t)
    (t (case (access tau-interval interval :domain)
        (integerp (and (integerp evg) (eval-tau-interval1 interval evg)))
        (rationalp (and (rationalp evg) (eval-tau-interval1 interval evg)))
        (acl2-numberp (and (acl2-numberp evg) (eval-tau-interval1 interval evg)))
        (otherwise (eval-tau-interval1 interval (fix evg)))))))

(defun decode-tau-interval
  (interval e skip-domain-flg)
  (cond ((null interval) nil)
    ((and (eq (access tau-interval interval :domain) nil)
       (eq (access tau-interval interval :lo-rel) nil)
       (eq (access tau-interval interval :lo) nil)
       (eq (access tau-interval interval :hi-rel) nil)
       (eq (access tau-interval interval :hi) nil)) '(non-canonical-universal-interval))
    (t (let ((lst `(,@(IF SKIP-DOMAIN-FLG
      NIL
      (IF (ACCESS TAU-INTERVAL INTERVAL :DOMAIN)
          `((,(ACCESS TAU-INTERVAL INTERVAL :DOMAIN) ,E))
          NIL)) ,@(IF (AND (NULL (ACCESS TAU-INTERVAL INTERVAL :LO))
           (NULL (ACCESS TAU-INTERVAL INTERVAL :LO-REL)))
      NIL
      `((,(IF (ACCESS TAU-INTERVAL INTERVAL :LO-REL)
              '<
              '<=)
         ,(IF (ACCESS TAU-INTERVAL INTERVAL :LO)
              (ACCESS TAU-INTERVAL INTERVAL :LO)
              'NON-CANONICAL-NEG-INFINITY)
         ,E)))
             ,@(IF (AND (NULL (ACCESS TAU-INTERVAL INTERVAL :HI))
           (NULL (ACCESS TAU-INTERVAL INTERVAL :HI-REL)))
      NIL
      `((,(IF (ACCESS TAU-INTERVAL INTERVAL :HI-REL)
              '<
              '<=)
         ,E
         ,(IF (ACCESS TAU-INTERVAL INTERVAL :HI)
              (ACCESS TAU-INTERVAL INTERVAL :HI)
              'NON-CANONICAL-POS-INFINITY)))))))
        lst))))

(defun tau-simple-implicants
  (sign pred wrld)
  (getpropc pred
    (if sign
      'pos-implicants
      'neg-implicants)
    nil
    wrld))

(defun tau-pair-member1
  (index pairs)
  (cond ((endp pairs) nil)
    ((>= (car (car pairs)) index) (or (equal (car (car pairs)) index)
        (tau-pair-member1 index (cdr pairs))))
    (t nil)))

(defun tau-pair-member
  (pair pairs)
  (tau-pair-member1 (car pair) pairs))

(defun ev-fncall-w-tau-recog
  (fn evg-lst ens wrld)
  (cond ((eq fn 'integerp) (integerp (car evg-lst)))
    ((eq fn 'rationalp) (rationalp (car evg-lst)))
    ((eq fn 'acl2-numberp) (acl2-numberp (car evg-lst)))
    ((enabled-xfnp fn ens wrld) (let* ((ubk (getpropc fn 'unevalable-but-known nil wrld)) (temp (if ubk
              (assoc-equal (car evg-lst) ubk)
              nil)))
        (cond (temp (cdr temp))
          (t (mv-let (erp val)
              (ev-fncall-w fn evg-lst wrld nil nil t t nil)
              (cond (erp :unevalable) (val t) (t nil)))))))
    (t :unevalable)))

(defun bad-val-or-unknowns
  (bad-val pairs evg-lst ens wrld)
  (cond ((endp pairs) nil)
    (t (let ((val (ev-fncall-w-tau-recog (cdr (car pairs)) evg-lst ens wrld)))
        (cond ((eq val :unevalable) (let ((rest (bad-val-or-unknowns bad-val (cdr pairs) evg-lst ens wrld)))
              (cond ((eq rest t) t) (t (cons (car pairs) rest)))))
          (bad-val (if val
              t
              (bad-val-or-unknowns bad-val (cdr pairs) evg-lst ens wrld)))
          (t (if val
              (bad-val-or-unknowns bad-val (cdr pairs) evg-lst ens wrld)
              t)))))))

(defun exists-bad-valp
  (bad-val pairs evg-lst ens wrld)
  (cond ((endp pairs) nil)
    (t (let ((val (ev-fncall-w-tau-recog (cdr (car pairs)) evg-lst ens wrld)))
        (cond ((eq val :unevalable) (exists-bad-valp bad-val (cdr pairs) evg-lst ens wrld))
          (bad-val (if val
              t
              (exists-bad-valp bad-val (cdr pairs) evg-lst ens wrld)))
          (t (if val
              (exists-bad-valp bad-val (cdr pairs) evg-lst ens wrld)
              t)))))))

(defun all-eval-valp
  (good-val pairs evg-lst ens wrld)
  (cond ((endp pairs) t)
    (t (let ((val (ev-fncall-w-tau-recog (cdr (car pairs)) evg-lst ens wrld)))
        (cond ((eq val :unevalable) nil)
          (good-val (if val
              (all-eval-valp val (cdr pairs) evg-lst ens wrld)
              nil))
          (t (if val
              nil
              (all-eval-valp val (cdr pairs) evg-lst ens wrld))))))))

(defun delete-bad-vals
  (neg-evgs pos-pairs neg-pairs ens wrld)
  (cond ((endp neg-evgs) (mv nil nil))
    (t (mv-let (changedp result)
        (delete-bad-vals (cdr neg-evgs)
          pos-pairs
          neg-pairs
          ens
          wrld)
        (cond ((exists-bad-valp nil pos-pairs (car neg-evgs) ens wrld) (mv t result))
          ((exists-bad-valp t neg-pairs (car neg-evgs) ens wrld) (mv t result))
          ((null changedp) (mv nil neg-evgs))
          (t (mv t (cons (car neg-evgs) result))))))))

(defun delete-bad-vals1
  (neg-evgs sign tau-pair ens wrld)
  (cond ((endp neg-evgs) (mv nil nil))
    (t (let ((val (ev-fncall-w-tau-recog (cdr tau-pair)
             (car neg-evgs)
             ens
             wrld)))
        (mv-let (changedp result)
          (delete-bad-vals1 (cdr neg-evgs) sign tau-pair ens wrld)
          (cond ((eq val :unevalable) (if changedp
                (mv t (cons (car neg-evgs) result))
                (mv nil neg-evgs)))
            (val (if sign
                (if changedp
                  (mv t (cons (car neg-evgs) result))
                  (mv nil neg-evgs))
                (mv t result)))
            (t (if sign
                (mv t result)
                (if changedp
                  (mv t (cons (car neg-evgs) result))
                  (mv nil neg-evgs))))))))))

(defun tau-pairs-subsetp
  (pairs1 pairs2)
  (cond ((endp pairs1) t)
    ((endp pairs2) nil)
    ((>= (car (car pairs1)) (car (car pairs2))) (if (equal (car (car pairs1)) (car (car pairs2)))
        (tau-pairs-subsetp (cdr pairs1) (cdr pairs2))
        nil))
    (t (tau-pairs-subsetp pairs1 (cdr pairs2)))))

(defun tau-pairs-near-subsetp
  (pairs1 pairs2 e)
  (cond ((endp pairs1) (if e
        e
        t))
    ((endp pairs2) (if e
        nil
        (if (endp (cdr pairs1))
          (car pairs1)
          nil)))
    ((>= (car (car pairs1)) (car (car pairs2))) (if (equal (car (car pairs1)) (car (car pairs2)))
        (tau-pairs-near-subsetp (cdr pairs1) (cdr pairs2) e)
        (if e
          nil
          (tau-pairs-near-subsetp (cdr pairs1) pairs2 (car pairs1)))))
    (t (tau-pairs-near-subsetp pairs1 (cdr pairs2) e))))

(defun tau-pairs-intersectionp
  (pairs1 pairs2)
  (cond ((endp pairs1) nil)
    ((endp pairs2) nil)
    ((>= (car (car pairs1)) (car (car pairs2))) (if (equal (car (car pairs1)) (car (car pairs2)))
        t
        (tau-pairs-intersectionp (cdr pairs1) pairs2)))
    (t (tau-pairs-intersectionp pairs1 (cdr pairs2)))))

(defun insert-tau-pair
  (pair pairs)
  (cond ((endp pairs) (cons pair pairs))
    ((>= (car (car pairs)) (car pair)) (if (eql (car (car pairs)) (car pair))
        t
        (let ((rest (insert-tau-pair pair (cdr pairs))))
          (if (eq rest t)
            t
            (cons (car pairs) rest)))))
    (t (cons pair pairs))))

(defun interval-decider
  (lo-rel lo hi-rel hi rel k)
  (if rel
    (cond ((and hi
         (if hi-rel
           (<= hi k)
           (< hi k))) t)
      ((and lo (<= k lo)) nil)
      (t '?))
    (cond ((and hi (<= hi k)) t)
      ((and lo
         (if lo-rel
           (<= k lo)
           (< k lo))) nil)
      (t '?))))

(defun signate
  (sign x)
  (if sign
    x
    (if (eq x '?)
      '?
      (not x))))

(defun reduce-sign/recog
  (tau sign recog ens wrld)
  (let ((discriminator (cdr recog)))
    (cond ((eq tau *tau-contradiction*) t)
      ((eq discriminator nil) (cond (sign (cond ((access tau tau :pos-evg) (equal recog (access tau tau :pos-evg)))
              ((member-neg-evgs recog (access tau tau :neg-evgs)) nil)
              ((not (eval-tau-interval (access tau tau :interval) (car recog))) nil)
              ((exists-bad-valp nil
                 (access tau tau :pos-pairs)
                 recog
                 ens
                 wrld) nil)
              ((exists-bad-valp t
                 (access tau tau :neg-pairs)
                 recog
                 ens
                 wrld) nil)
              (t '?)))
          (t (cond ((access tau tau :pos-evg) (not (equal recog (access tau tau :pos-evg))))
              ((member-neg-evgs recog (access tau tau :neg-evgs)) t)
              ((not (eval-tau-interval (access tau tau :interval) (car recog))) t)
              ((exists-bad-valp nil
                 (access tau tau :pos-pairs)
                 recog
                 ens
                 wrld) t)
              ((exists-bad-valp t
                 (access tau tau :neg-pairs)
                 recog
                 ens
                 wrld) t)
              (t '?)))))
      ((eq discriminator :lessp-x-k) (let ((k (car recog)) (interval (access tau tau :interval)))
          (cond ((null interval) (cond ((tau-pair-member *tau-acl2-numberp-pair*
                   (access tau tau :neg-pairs)) (signate sign (< 0 k)))
                (t '?)))
            (t (let ((ans (interval-decider (access tau-interval interval :lo-rel)
                     (access tau-interval interval :lo)
                     (access tau-interval interval :hi-rel)
                     (access tau-interval interval :hi)
                     t
                     k)))
                (signate sign ans))))))
      ((eq discriminator :lessp-k-x) (let ((k (car recog)) (interval (access tau tau :interval)))
          (cond ((null interval) (cond ((tau-pair-member *tau-acl2-numberp-pair*
                   (access tau tau :neg-pairs)) (signate sign (< k 0)))
                (t '?)))
            (t (let ((ans (interval-decider (access tau-interval interval :lo-rel)
                     (access tau-interval interval :lo)
                     (access tau-interval interval :hi-rel)
                     (access tau-interval interval :hi)
                     nil
                     k)))
                (signate (not sign) ans))))))
      (t (cond ((access tau tau :pos-evg) (let ((val (ev-fncall-w-tau-recog discriminator
                   (access tau tau :pos-evg)
                   ens
                   wrld)))
              (cond ((eq val :unevalable) (cond ((tau-pair-member recog
                       (if sign
                         (access tau tau :pos-pairs)
                         (access tau tau :neg-pairs))) t)
                    ((tau-pair-member recog
                       (if sign
                         (access tau tau :neg-pairs)
                         (access tau tau :pos-pairs))) nil)
                    (t '?)))
                (sign (if val
                    t
                    nil))
                (t (if val
                    nil
                    t)))))
          ((tau-pair-member recog
             (if sign
               (access tau tau :pos-pairs)
               (access tau tau :neg-pairs))) t)
          ((tau-pair-member recog
             (if sign
               (access tau tau :neg-pairs)
               (access tau tau :pos-pairs))) nil)
          (t '?))))))

(defun every-neg-evg-in-tau-p1
  (neg-evgs1 neg-evgs2
    pos-pairs2
    neg-pairs2
    interval2
    ens
    wrld)
  (cond ((endp neg-evgs1) t)
    ((endp neg-evgs2) (and (or (not (eval-tau-interval interval2 (car (car neg-evgs1))))
          (exists-bad-valp nil pos-pairs2 (car neg-evgs1) ens wrld)
          (exists-bad-valp t neg-pairs2 (car neg-evgs1) ens wrld))
        (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
          nil
          pos-pairs2
          neg-pairs2
          interval2
          ens
          wrld)))
    ((lexorder (car (car neg-evgs1)) (car (car neg-evgs2))) (cond ((equal (car (car neg-evgs1)) (car (car neg-evgs2))) (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
            (cdr neg-evgs2)
            pos-pairs2
            neg-pairs2
            interval2
            ens
            wrld))
        (t (and (or (not (eval-tau-interval interval2 (car (car neg-evgs1))))
              (exists-bad-valp nil pos-pairs2 (car neg-evgs1) ens wrld)
              (exists-bad-valp t neg-pairs2 (car neg-evgs1) ens wrld))
            (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
              neg-evgs2
              pos-pairs2
              neg-pairs2
              interval2
              ens
              wrld)))))
    (t (every-neg-evg-in-tau-p1 neg-evgs1
        (cdr neg-evgs2)
        pos-pairs2
        neg-pairs2
        interval2
        ens
        wrld))))

(defun every-neg-evg-in-tau-p
  (neg-evgs tau ens wrld)
  (cond ((endp neg-evgs) t)
    ((access tau tau :pos-evg) (not (member-neg-evgs (access tau tau :pos-evg) neg-evgs)))
    (t (let ((neg-evgs1 neg-evgs) (neg-evgs2 (access tau tau :neg-evgs))
          (pos-pairs2 (access tau tau :pos-pairs))
          (neg-pairs2 (access tau tau :neg-pairs))
          (interval2 (access tau tau :interval)))
        (cond ((eq (car (car neg-evgs1)) nil) (cond ((endp neg-evgs2) (and (or (not (eval-tau-interval interval2 nil))
                    (exists-bad-valp nil
                      pos-pairs2
                      *nil-singleton-evg-list*
                      ens
                      wrld)
                    (exists-bad-valp t
                      neg-pairs2
                      *nil-singleton-evg-list*
                      ens
                      wrld))
                  (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
                    nil
                    pos-pairs2
                    neg-pairs2
                    interval2
                    ens
                    wrld)))
              ((eq (car (car neg-evgs2)) nil) (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
                  (cdr neg-evgs2)
                  pos-pairs2
                  neg-pairs2
                  interval2
                  ens
                  wrld))
              (t (and (or (not (eval-tau-interval interval2 nil))
                    (exists-bad-valp nil
                      pos-pairs2
                      *nil-singleton-evg-list*
                      ens
                      wrld)
                    (exists-bad-valp t
                      neg-pairs2
                      *nil-singleton-evg-list*
                      ens
                      wrld))
                  (every-neg-evg-in-tau-p1 (cdr neg-evgs1)
                    neg-evgs2
                    pos-pairs2
                    neg-pairs2
                    interval2
                    ens
                    wrld)))))
          ((and (consp neg-evgs2) (eq (car (car neg-evgs2)) nil)) (every-neg-evg-in-tau-p1 neg-evgs1
              (cdr neg-evgs2)
              pos-pairs2
              neg-pairs2
              interval2
              ens
              wrld))
          (t (every-neg-evg-in-tau-p1 neg-evgs1
              neg-evgs2
              pos-pairs2
              neg-pairs2
              interval2
              ens
              wrld)))))))

(defun lower-bound-<=
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    t
    (if (null b)
      nil
      (if (and a-rel (not b-rel))
        (< a b)
        (<= a b)))))

(defun upper-bound->=
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    t
    (if (null b)
      nil
      (if (and a-rel (not b-rel))
        (< b a)
        (<= b a)))))

(defun lower-bound->
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    nil
    (if (null b)
      t
      (if (and a-rel (not b-rel))
        (>= a b)
        (> a b)))))

(defun upper-bound-<
  (a-rel a b-rel b)
  (declare (xargs :guard (and (booleanp a-rel)
        (or (null a) (rationalp a))
        (booleanp b-rel)
        (or (null b) (rationalp b)))))
  (if (null a)
    nil
    (if (null b)
      t
      (if (and a-rel (not b-rel))
        (<= a b)
        (< a b)))))

(defun tau-subintervalp
  (interval1 interval2)
  (let ((dom1 (access tau-interval interval1 :domain)) (dom2 (access tau-interval interval2 :domain)))
    (and (case dom1
        (integerp t)
        (rationalp (not (eq dom2 'integerp)))
        (acl2-numberp (or (eq dom2 'acl2-numberp) (null dom2)))
        (otherwise (null dom2)))
      (lower-bound-<= (access tau-interval interval2 :lo-rel)
        (access tau-interval interval2 :lo)
        (access tau-interval interval1 :lo-rel)
        (access tau-interval interval1 :lo))
      (upper-bound->= (access tau-interval interval2 :hi-rel)
        (access tau-interval interval2 :hi)
        (access tau-interval interval1 :hi-rel)
        (access tau-interval interval1 :hi)))))

(defun tau-implies
  (tau1 tau2 ens wrld)
  (cond ((eq tau1 *tau-contradiction*) t)
    ((eq tau2 *tau-contradiction*) nil)
    ((access tau tau2 :pos-evg) (if (access tau tau1 :pos-evg)
        (equal (access tau tau2 :pos-evg)
          (access tau tau1 :pos-evg))
        nil))
    ((access tau tau1 :pos-evg) (and (not (member-neg-evgs (access tau tau1 :pos-evg)
            (access tau tau2 :neg-evgs)))
        (all-eval-valp t
          (access tau tau2 :pos-pairs)
          (access tau tau1 :pos-evg)
          ens
          wrld)
        (all-eval-valp nil
          (access tau tau2 :neg-pairs)
          (access tau tau1 :pos-evg)
          ens
          wrld)
        (eval-tau-interval (access tau tau2 :interval)
          (car (access tau tau1 :pos-evg)))))
    (t (and (every-neg-evg-in-tau-p (access tau tau2 :neg-evgs)
          tau1
          ens
          wrld)
        (tau-pairs-subsetp (access tau tau2 :pos-pairs)
          (access tau tau1 :pos-pairs))
        (tau-pairs-subsetp (access tau tau2 :neg-pairs)
          (access tau tau1 :neg-pairs))
        (tau-subintervalp (access tau tau1 :interval)
          (access tau tau2 :interval))))))

(defun empty-tau-intervalp
  (lo-rel lo hi-rel hi)
  (cond ((null lo) nil)
    ((null hi) nil)
    ((or lo-rel hi-rel) (<= hi lo))
    (t (< hi lo))))

(defun singleton-tau-intervalp
  (lo-rel lo hi-rel hi)
  (and lo (equal lo hi) (not lo-rel) (not hi-rel)))

(defun make-identity-interval
  (interval evg)
  (let ((dom (cond ((integerp evg) 'integerp)
         ((rationalp evg) 'rationalp)
         (t nil))))
    (cond ((null dom) nil)
      ((and (eq dom (access tau-interval interval :domain))
         (eql evg (access tau-interval interval :lo))
         (eq nil (access tau-interval interval :lo-rel))
         (eql evg (access tau-interval interval :hi))
         (eq nil (access tau-interval interval :hi-rel))) interval)
      (t (make tau-interval
          :domain dom
          :lo evg
          :lo-rel nil
          :hi-rel nil
          :hi evg)))))

(defun identity-intervalp
  (int)
  (and (or (eq (access tau-interval int :domain) 'integerp)
      (eq (access tau-interval int :domain) 'rationalp))
    (null (access tau-interval int :lo-rel))
    (null (access tau-interval int :hi-rel))
    (access tau-interval int :lo)
    (eql (access tau-interval int :lo)
      (access tau-interval int :hi))))

(defun delete-consecutive-integers-upward
  (k neg-evgs)
  (cond ((endp neg-evgs) (mv k nil))
    ((< (car (car neg-evgs)) k) (delete-consecutive-integers-upward k (cdr neg-evgs)))
    ((eql (car (car neg-evgs)) k) (delete-consecutive-integers-upward (+ k 1) (cdr neg-evgs)))
    (t (mv k neg-evgs))))

(defun delete-consecutive-integers-downward
  (k neg-evgs)
  (cond ((endp neg-evgs) (mv k neg-evgs))
    ((> (car (car neg-evgs)) k) (mv k nil))
    ((eql (car (car neg-evgs)) k) (mv (- k 1) nil))
    (t (mv-let (k1 neg-evgs1)
        (delete-consecutive-integers-downward k (cdr neg-evgs))
        (cond ((eql (car (car neg-evgs)) k1) (mv (- k1 1) neg-evgs1))
          (t (mv k1 (cons (car neg-evgs) neg-evgs1))))))))

(defun collect-<?-x-k
  (rel k neg-evgs)
  (cond ((endp neg-evgs) nil)
    ((acl2-numberp (car (car neg-evgs))) (if (<?-number-v-rational rel (car (car neg-evgs)) k)
        (cons (car neg-evgs) (collect-<?-x-k rel k (cdr neg-evgs)))
        (collect-<?-x-k rel k (cdr neg-evgs))))
    ((if rel
       (< 0 k)
       (<= 0 k)) neg-evgs)
    (t nil)))

(defun collect-<?-k-x
  (rel k neg-evgs)
  (cond ((endp neg-evgs) nil)
    ((acl2-numberp (car (car neg-evgs))) (if (<?-rational-v-number rel k (car (car neg-evgs)))
        (cons (car neg-evgs) (collect-<?-k-x rel k (cdr neg-evgs)))
        (collect-<?-k-x rel k (cdr neg-evgs))))
    ((if rel
       (< k 0)
       (<= k 0)) neg-evgs)
    (t nil)))

(defun adjust-upper-bound-with-neg-evgs
  (domain rel k neg-evgs)
  (if (eq domain 'integerp)
    (mv-let (k1 neg-evgs1)
      (delete-consecutive-integers-downward k neg-evgs)
      (mv nil k1 neg-evgs1))
    (if (and (null domain) (eql k 0))
      (mv rel k neg-evgs)
      (let ((new-rel (or rel
             (if (assoc-equal k neg-evgs)
               t
               nil))))
        (mv new-rel k (collect-<?-x-k new-rel k neg-evgs))))))

(defun adjust-lower-bound-with-neg-evgs
  (domain rel k neg-evgs)
  (if (eq domain 'integerp)
    (mv-let (k1 neg-evgs1)
      (delete-consecutive-integers-upward k neg-evgs)
      (mv nil k1 neg-evgs1))
    (if (and (null domain) (eql k 0))
      (mv rel k neg-evgs)
      (let ((new-rel (or rel
             (if (assoc-equal k neg-evgs)
               t
               nil))))
        (mv new-rel k (collect-<?-k-x new-rel k neg-evgs))))))

(defun squeeze-k
  (upper-boundp rel k)
  (declare (xargs :guard (and (booleanp upper-boundp)
        (booleanp rel)
        (or (null k) (rationalp k)))))
  (if k
    (if (integerp k)
      (if rel
        (if upper-boundp
          (- k 1)
          (+ k 1))
        k)
      (if upper-boundp
        (floor k 1)
        (ceiling k 1)))
    nil))

(defun set-tau-pos-evg
  (tau recog ens wrld)
  (let ((evg (car recog)) (new-pos-pairs (bad-val-or-unknowns nil
          (access tau tau :pos-pairs)
          recog
          ens
          wrld)))
    (cond ((eq new-pos-pairs t) *tau-contradiction*)
      (t (let ((new-neg-pairs (bad-val-or-unknowns t
               (access tau tau :neg-pairs)
               recog
               ens
               wrld)))
          (cond ((eq new-neg-pairs t) *tau-contradiction*)
            (t (make tau
                :pos-evg recog
                :neg-evgs nil
                :pos-pairs new-pos-pairs
                :neg-pairs new-neg-pairs
                :interval (make-identity-interval (access tau tau :interval) evg)))))))))

(defun positive-lower-boundp
  (lo-rel lo)
  (and lo
    (if lo-rel
      (<= 0 lo)
      (< 0 lo))))

(defun nonnegative-lower-boundp (lo) (and lo (<= 0 lo)))

(defun negative-upper-boundp
  (hi-rel hi)
  (and hi
    (if hi-rel
      (<= hi 0)
      (< hi 0))))

(defun tighten-bound
  (tau domain upper-boundp rel k ens wrld)
  (if (eq tau *tau-contradiction*)
    *tau-contradiction*
    (let* ((interval (access tau tau :interval)) (neg-evgs (access tau tau :neg-evgs))
        (domain0 (access tau-interval interval :domain))
        (lo0 (access tau-interval interval :lo))
        (lo-rel0 (access tau-interval interval :lo-rel))
        (hi0 (access tau-interval interval :hi))
        (hi-rel0 (access tau-interval interval :hi-rel)))
      (let ((domain (cond ((eq domain nil) domain0)
             ((or (eq domain0 'integerp) (eq domain 'integerp)) 'integerp)
             ((or (eq domain0 'rationalp) (eq domain 'rationalp)) 'rationalp)
             ((or domain0 domain) 'acl2-numberp)
             (t nil))))
        (mv-let (lo-rel lo hi-rel hi)
          (if (and (not (eq domain domain0)) (eq domain 'integerp))
            (mv nil
              (squeeze-k nil lo-rel0 lo0)
              nil
              (squeeze-k t hi-rel0 hi0))
            (mv lo-rel0 lo0 hi-rel0 hi0))
          (mv-let (rel k)
            (if (eq domain 'integerp)
              (mv nil (squeeze-k upper-boundp rel k))
              (mv rel k))
            (mv-let (lo-rel lo)
              (if (and (not upper-boundp) (lower-bound-> rel k lo-rel lo))
                (mv rel k)
                (mv lo-rel lo))
              (mv-let (hi-rel hi)
                (if (and upper-boundp (upper-bound-< rel k hi-rel hi))
                  (mv rel k)
                  (mv hi-rel hi))
                (mv-let (new-lo-rel new-lo new-neg-evgs)
                  (if (and (equal lo-rel lo-rel0) (equal lo lo0))
                    (mv lo-rel lo neg-evgs)
                    (adjust-lower-bound-with-neg-evgs domain lo-rel lo neg-evgs))
                  (mv-let (new-hi-rel new-hi new-neg-evgs)
                    (if (and (equal hi-rel hi-rel0) (equal hi hi0))
                      (mv hi-rel hi new-neg-evgs)
                      (adjust-upper-bound-with-neg-evgs domain
                        hi-rel
                        hi
                        new-neg-evgs))
                    (let ((new-domain (if (and (null domain)
                             (or (positive-lower-boundp new-lo-rel new-lo)
                               (negative-upper-boundp new-hi-rel new-hi)))
                           'acl2-numberp
                           domain)))
                      (cond ((and (eq new-domain domain0)
                           (eq new-lo-rel lo-rel0)
                           (eql new-lo lo0)
                           (eq new-hi-rel hi-rel0)
                           (eql new-hi hi0)) tau)
                        ((empty-tau-intervalp new-lo-rel new-lo new-hi-rel new-hi) *tau-contradiction*)
                        ((and new-domain
                           (singleton-tau-intervalp new-lo-rel
                             new-lo
                             new-hi-rel
                             new-hi)) (set-tau-pos-evg tau (cons new-hi nil) ens wrld))
                        (t (change tau
                            tau
                            :interval (make tau-interval
                              :domain new-domain
                              :lo new-lo
                              :lo-rel new-lo-rel
                              :hi-rel new-hi-rel
                              :hi new-hi)
                            :neg-evgs new-neg-evgs))))))))))))))

(defun add-to-tau1
  (sign recog tau ens wrld)
  (let ((discriminator (cdr recog)))
    (cond ((or (eq tau *tau-contradiction*)
         (equal tau *contradictory-tau*)) *tau-contradiction*)
      ((eq discriminator nil) (cond (sign (cond ((access tau tau :pos-evg) (if (equal recog (access tau tau :pos-evg))
                  tau
                  *tau-contradiction*))
              ((member-neg-evgs recog (access tau tau :neg-evgs)) *tau-contradiction*)
              ((not (eval-tau-interval (access tau tau :interval) (car recog))) *tau-contradiction*)
              (t (let ((new-pos-pairs (bad-val-or-unknowns nil
                       (access tau tau :pos-pairs)
                       recog
                       ens
                       wrld)))
                  (cond ((eq new-pos-pairs t) *tau-contradiction*)
                    (t (let ((new-neg-pairs (bad-val-or-unknowns t
                             (access tau tau :neg-pairs)
                             recog
                             ens
                             wrld)))
                        (cond ((eq new-neg-pairs t) *tau-contradiction*)
                          (t (make tau
                              :pos-evg recog
                              :neg-evgs nil
                              :pos-pairs new-pos-pairs
                              :neg-pairs new-neg-pairs
                              :interval (make-identity-interval (access tau tau :interval)
                                (car recog))))))))))))
          (t (cond ((access tau tau :pos-evg) (if (equal recog (access tau tau :pos-evg))
                  *tau-contradiction*
                  tau))
              ((member-neg-evgs recog (access tau tau :neg-evgs)) tau)
              ((not (eval-tau-interval (access tau tau :interval) (car recog))) tau)
              ((exists-bad-valp nil
                 (access tau tau :pos-pairs)
                 recog
                 ens
                 wrld) tau)
              ((exists-bad-valp t
                 (access tau tau :neg-pairs)
                 recog
                 ens
                 wrld) tau)
              (t (let ((interval (access tau tau :interval)))
                  (cond ((and (or (access tau-interval interval :domain)
                         (not (eql (car recog) 0)))
                       interval
                       (rationalp (car recog))) (cond ((and (null (access tau-interval interval :lo-rel))
                           (eql (access tau-interval interval :lo) (car recog))) (tighten-bound tau nil nil t (car recog) ens wrld))
                        ((and (null (access tau-interval interval :hi-rel))
                           (eql (access tau-interval interval :hi) (car recog))) (tighten-bound tau nil t t (car recog) ens wrld))
                        (t (change tau
                            tau
                            :neg-evgs (insert-neg-evgs recog (access tau tau :neg-evgs))))))
                    (t (change tau
                        tau
                        :neg-evgs (insert-neg-evgs recog (access tau tau :neg-evgs)))))))))))
      ((or (eq discriminator :lessp-x-k)
         (eq discriminator :lessp-k-x)) (let ((k (car recog)))
          (mv-let (upper-boundp rel)
            (if (eq discriminator :lessp-x-k)
              (if sign
                (mv t t)
                (mv nil nil))
              (if sign
                (mv nil t)
                (mv t nil)))
            (tighten-bound tau nil upper-boundp rel k ens wrld))))
      (t (cond ((access tau tau :pos-evg) (let ((val (ev-fncall-w-tau-recog discriminator
                   (access tau tau :pos-evg)
                   ens
                   wrld)))
              (cond ((eq val :unevalable) (cond (sign (let ((new-pos-pairs (insert-tau-pair recog (access tau tau :pos-pairs))))
                        (cond ((eq new-pos-pairs t) tau)
                          ((tau-pair-member recog (access tau tau :neg-pairs)) *tau-contradiction*)
                          (t (change tau tau :pos-pairs new-pos-pairs)))))
                    (t (let ((new-neg-pairs (insert-tau-pair recog (access tau tau :neg-pairs))))
                        (cond ((eq new-neg-pairs t) tau)
                          ((tau-pair-member recog (access tau tau :pos-pairs)) *tau-contradiction*)
                          (t (change tau tau :neg-pairs new-neg-pairs)))))))
                ((eq val sign) tau)
                (t *tau-contradiction*))))
          ((tau-pair-member recog
             (if sign
               (access tau tau :pos-pairs)
               (access tau tau :neg-pairs))) tau)
          ((tau-pair-member recog
             (if sign
               (access tau tau :neg-pairs)
               (access tau tau :pos-pairs))) *tau-contradiction*)
          (t (mv-let (changedp new-neg-evgs)
              (delete-bad-vals1 (access tau tau :neg-evgs)
                sign
                recog
                ens
                wrld)
              (let ((tau1 (if sign
                     (if changedp
                       (change tau
                         tau
                         :neg-evgs new-neg-evgs
                         :pos-pairs (insert-tau-pair recog (access tau tau :pos-pairs)))
                       (change tau
                         tau
                         :pos-pairs (insert-tau-pair recog (access tau tau :pos-pairs))))
                     (if changedp
                       (change tau
                         tau
                         :neg-evgs new-neg-evgs
                         :neg-pairs (insert-tau-pair recog (access tau tau :neg-pairs)))
                       (change tau
                         tau
                         :neg-pairs (insert-tau-pair recog (access tau tau :neg-pairs)))))))
                (cond (sign (case discriminator
                      (natp (tighten-bound tau1 'integerp nil nil 0 ens wrld))
                      (posp (tighten-bound tau1 'integerp nil t 0 ens wrld))
                      (integerp (tighten-bound tau1 'integerp nil nil nil ens wrld))
                      (rationalp (tighten-bound tau1 'rationalp nil nil nil ens wrld))
                      (acl2-numberp (tighten-bound tau1 'acl2-numberp nil nil nil ens wrld))
                      (minusp (tighten-bound tau1 'acl2-numberp t t 0 ens wrld))
                      (otherwise tau1)))
                  (t (let ((domain (access tau-interval (access tau tau1 :interval) :domain)))
                      (case discriminator
                        (acl2-numberp (cond ((eq domain nil) (tighten-bound (tighten-bound tau1 nil nil nil 0 ens wrld)
                                nil
                                t
                                nil
                                0
                                ens
                                wrld))
                            (t *tau-contradiction*)))
                        (rationalp (if (or (eq domain 'rationalp) (eq domain 'integerp))
                            *tau-contradiction*
                            tau1))
                        (integerp (if (eq domain 'integerp)
                            *tau-contradiction*
                            tau1))
                        (minusp (tighten-bound tau1 nil nil nil 0 ens wrld))
                        (natp (cond ((eq domain 'integerp) (tighten-bound tau1 'integerp t t 0 ens wrld))
                            (t tau1)))
                        (posp (cond ((eq domain 'integerp) (tighten-bound tau1 nil t nil 0 ens wrld))
                            (t tau1)))
                        (otherwise tau1)))))))))))))

(defun add-recogs-to-tau1
  (sign recog-lst tau ens wrld)
  (cond ((endp recog-lst) tau)
    (t (let ((tau (add-to-tau1 sign (car recog-lst) tau ens wrld)))
        (cond ((eq tau *tau-contradiction*) *tau-contradiction*)
          (t (add-recogs-to-tau1 sign (cdr recog-lst) tau ens wrld)))))))

(defun tau-interval-endpoint-to-sign-k-token
  (upper-boundp rel k)
  (if upper-boundp
    (if rel
      (mv t k :lessp-x-k)
      (mv nil k :lessp-k-x))
    (if rel
      (mv t k :lessp-k-x)
      (mv nil k :lessp-x-k))))

(defun tau-union
  (tau1 tau2 ens wrld)
  (let ((tau2 (if (access tau tau1 :pos-evg)
         (add-to-tau1 t (access tau tau1 :pos-evg) tau2 ens wrld)
         tau2)))
    (let ((tau2 (if (eq tau2 *tau-contradiction*)
           *tau-contradiction*
           (add-recogs-to-tau1 nil
             (access tau tau1 :neg-evgs)
             tau2
             ens
             wrld))))
      (let ((tau2 (if (eq tau2 *tau-contradiction*)
             *tau-contradiction*
             (add-recogs-to-tau1 t
               (access tau tau1 :pos-pairs)
               tau2
               ens
               wrld))))
        (let ((tau2 (if (eq tau2 *tau-contradiction*)
               *tau-contradiction*
               (add-recogs-to-tau1 nil
                 (access tau tau1 :neg-pairs)
                 tau2
                 ens
                 wrld))))
          (if (eq tau2 *tau-contradiction*)
            *tau-contradiction*
            (let ((interval (access tau tau1 :interval)))
              (mv-let (sign1 recog1)
                (if (and interval (access tau-interval interval :lo))
                  (mv-let (sign k token)
                    (tau-interval-endpoint-to-sign-k-token nil
                      (access tau-interval interval :lo-rel)
                      (access tau-interval interval :lo))
                    (mv sign (cons k token)))
                  (mv nil nil))
                (mv-let (sign2 recog2)
                  (if (and interval (access tau-interval interval :hi))
                    (mv-let (sign k token)
                      (tau-interval-endpoint-to-sign-k-token t
                        (access tau-interval interval :hi-rel)
                        (access tau-interval interval :hi))
                      (mv sign (cons k token)))
                    (mv nil nil))
                  (let ((tau2 (if recog1
                         (add-to-tau1 sign1 recog1 tau2 ens wrld)
                         tau2)))
                    (if (eq tau2 *tau-contradiction*)
                      *tau-contradiction*
                      (let ((tau2 (if recog2
                             (add-to-tau1 sign2 recog2 tau2 ens wrld)
                             tau2)))
                        tau2))))))))))))

(defun all-integers-in-range-excludedp1
  (lo hi neg-evgs)
  (cond ((> lo hi) t)
    ((endp neg-evgs) nil)
    ((equal lo (car (car neg-evgs))) (all-integers-in-range-excludedp1 (+ 1 lo)
        hi
        (cdr neg-evgs)))
    ((or (not (rationalp (car (car neg-evgs))))
       (> (car (car neg-evgs)) hi)) nil)
    (t (all-integers-in-range-excludedp1 lo hi (cdr neg-evgs)))))

(defun all-integers-in-range-excludedp
  (lo-rel lo hi-rel hi neg-evgs)
  (let* ((ilo (squeeze-k nil lo-rel lo)) (ihi (squeeze-k t hi-rel hi))
      (lst (if (and (consp neg-evgs) (eq nil (car (car neg-evgs))))
          (cdr neg-evgs)
          neg-evgs))
      (k (+ 1 (- ihi ilo))))
    (cond ((> k (len lst)) nil)
      (t (all-integers-in-range-excludedp1 ilo ihi lst)))))

(defun add-to-tau
  (sign recog tau ens wrld)
  (let ((tau1 (let ((discriminator (cdr recog)))
         (cond ((or (eq discriminator nil)
              (eq discriminator :lessp-x-k)
              (eq discriminator :lessp-k-x)) (add-to-tau1 sign recog tau ens wrld))
           (t (tau-union (tau-simple-implicants sign discriminator wrld)
               (add-to-tau1 sign recog tau ens wrld)
               ens
               wrld))))))
    (cond ((eq tau1 *tau-contradiction*) *tau-contradiction*)
      (t (let* ((interval (access tau tau1 :interval)) (domain (access tau-interval interval :domain))
            (lo-rel (access tau-interval interval :lo-rel))
            (lo (access tau-interval interval :lo))
            (hi-rel (access tau-interval interval :hi-rel))
            (hi (access tau-interval interval :hi))
            (pos-pairs (access tau tau1 :pos-pairs))
            (neg-pairs (access tau tau1 :neg-pairs)))
          (cond ((or (null interval)
               (and (null lo) (null hi))
               (access tau tau1 :pos-evg)) tau1)
            ((and hi
               (if hi-rel
                 (<= hi 0)
                 (< hi 0))
               (not (tau-pair-member *tau-minusp-pair* pos-pairs))) (add-to-tau t *tau-minusp-pair* tau1 ens wrld))
            ((and (eq domain 'integerp)
               lo
               (< 0 lo)
               (not (tau-pair-member *tau-posp-pair* pos-pairs))) (add-to-tau t *tau-posp-pair* tau1 ens wrld))
            ((and (eq domain 'integerp)
               lo
               (<= 0 lo)
               (not (tau-pair-member *tau-natp-pair* pos-pairs))) (add-to-tau t *tau-natp-pair* tau1 ens wrld))
            ((or (and (eq domain 'integerp)
                 (not (tau-pair-member *tau-integerp-pair* pos-pairs)))
               (and (eq domain 'rationalp)
                 (not (tau-pair-member *tau-rationalp-pair* pos-pairs)))) (er hard
                'add-to-tau
                "It was thought impossible for a tau to have an :interval with ~
               domain ~x0 without that recognizer being in its :pos-pairs, ~
               but it happened with ~x1.  One way this might have happened is ~
               if the initial tau was ``incomplete,'' e.g., had NATP in it ~
               but not its implicants.  But add-to-tau is supposed to be ~
               called on complete taus and guarantees the completeness of its ~
               result."
                domain
                tau1))
            ((and (eq domain 'acl2-numberp)
               (not (tau-pair-member *tau-acl2-numberp-pair* pos-pairs))) (add-to-tau t *tau-acl2-numberp-pair* tau1 ens wrld))
            ((and (tau-pair-member *tau-natp-pair* neg-pairs)
               lo
               (<= 0 lo)
               (not (tau-pair-member *tau-integerp-pair* neg-pairs))) (add-to-tau nil *tau-integerp-pair* tau1 ens wrld))
            ((and (tau-pair-member *tau-posp-pair* neg-pairs)
               lo
               (< 0 lo)
               (not (tau-pair-member *tau-integerp-pair* neg-pairs))) (add-to-tau nil *tau-integerp-pair* tau1 ens wrld))
            ((and (tau-pair-member *tau-rationalp-pair* pos-pairs)
               lo
               hi
               (not (tau-pair-member *tau-integerp-pair* neg-pairs))
               (all-integers-in-range-excludedp lo-rel
                 lo
                 hi-rel
                 hi
                 (access tau tau1 :neg-evgs))) (add-to-tau nil *tau-integerp-pair* tau1 ens wrld))
            (t tau1)))))))

(defun pos-evg-near-subsetp
  (pos-evg1 pos-evg2)
  (if pos-evg1
    (if pos-evg2
      (if (equal pos-evg1 pos-evg2)
        t
        pos-evg1)
      pos-evg1)
    t))

(defun neg-evgs-near-subsetp
  (neg-evgs1 neg-evgs2
    e
    pos-pairs2
    neg-pairs2
    interval2
    ens
    wrld)
  (cond ((endp neg-evgs1) (if e
        e
        t))
    ((endp neg-evgs2) (cond ((or (not (eval-tau-interval interval2 (car (car neg-evgs1))))
           (exists-bad-valp nil pos-pairs2 (car neg-evgs1) ens wrld)
           (exists-bad-valp t neg-pairs2 (car neg-evgs1) ens wrld)) (neg-evgs-near-subsetp (cdr neg-evgs1)
            nil
            e
            pos-pairs2
            neg-pairs2
            interval2
            ens
            wrld))
        (t (if e
            nil
            (neg-evgs-near-subsetp (cdr neg-evgs1)
              nil
              (car neg-evgs1)
              pos-pairs2
              neg-pairs2
              interval2
              ens
              wrld)))))
    ((almost-lexorder-singletons (car neg-evgs1) (car neg-evgs2)) (if (equal (car neg-evgs1) (car neg-evgs2))
        (neg-evgs-near-subsetp (cdr neg-evgs1)
          (cdr neg-evgs2)
          e
          pos-pairs2
          neg-pairs2
          interval2
          ens
          wrld)
        (cond ((or (not (eval-tau-interval interval2 (car (car neg-evgs1))))
             (exists-bad-valp nil pos-pairs2 (car neg-evgs1) ens wrld)
             (exists-bad-valp t neg-pairs2 (car neg-evgs1) ens wrld)) (neg-evgs-near-subsetp (cdr neg-evgs1)
              (cdr neg-evgs2)
              e
              pos-pairs2
              neg-pairs2
              interval2
              ens
              wrld))
          (t (if e
              nil
              (neg-evgs-near-subsetp (cdr neg-evgs1)
                neg-evgs2
                (car neg-evgs1)
                pos-pairs2
                neg-pairs2
                interval2
                ens
                wrld))))))
    (t (neg-evgs-near-subsetp neg-evgs1
        (cdr neg-evgs2)
        e
        pos-pairs2
        neg-pairs2
        interval2
        ens
        wrld))))

(defun tau-interval-endpoint-implication
  (ap arel k bp brel d)
  (if k
    (if d
      (if ap
        (if arel
          (if bp
            (if (<= k d)
              t
              '?)
            (if (<= k d)
              nil
              '?))
          (if bp
            (if brel
              (if (< k d)
                t
                '?)
              (if (<= k d)
                t
                '?))
            (if brel
              (if (<= k d)
                nil
                '?)
              (if (< k d)
                nil
                '?))))
        (if arel
          (if bp
            (if (<= d k)
              nil
              '?)
            (if (<= d k)
              t
              '?))
          (if bp
            (if brel
              (if (<= d k)
                nil
                '?)
              (if (< d k)
                nil
                '?))
            (if brel
              (if (< d k)
                t
                '?)
              (if (<= d k)
                t
                '?)))))
      t)
    (if d
      '?
      t)))

(defun tau-interval-near-subsetp
  (interval1 interval2)
  (let ((b-lo-rel (access tau-interval interval1 :lo-rel)) (b-lo-d (access tau-interval interval1 :lo))
      (b-hi-rel (access tau-interval interval1 :hi-rel))
      (b-hi-d (access tau-interval interval1 :hi))
      (a-lo-rel (access tau-interval interval2 :lo-rel))
      (a-lo-k (access tau-interval interval2 :lo))
      (a-hi-rel (access tau-interval interval2 :hi-rel))
      (a-hi-k (access tau-interval interval2 :hi)))
    (let ((temp (tau-interval-endpoint-implication t
           a-hi-rel
           a-hi-k
           t
           b-hi-rel
           b-hi-d)))
      (cond ((eq temp t) (let ((temp (tau-interval-endpoint-implication nil
                 a-lo-rel
                 a-lo-k
                 nil
                 b-lo-rel
                 b-lo-d)))
            (cond ((eq temp t) (mv nil nil t))
              ((eq temp nil) (mv nil nil nil))
              (t (let ((temp (tau-interval-endpoint-implication t
                       a-hi-rel
                       a-hi-k
                       nil
                       b-lo-rel
                       b-lo-d)))
                  (cond ((eq temp t) (mv nil
                        nil
                        (er hard
                          'tau-interval-near-subsetp
                          "``A hi --> B lo'' returned T after ``A lo --> B ~
                          lo'' returned unknown.  This is not supposed to ~
                          happen!  The only way an upper bound like ``A hi'' ~
                          can imply a lower bound like ``B lo'' is if the ~
                          lower bound is negative infinity (i.e., the bound ~
                          is vacuous), in which case ``A lo --> B lo'' would ~
                          have succeeded.  A is this tau-interval ~x0 and B ~
                          is this one ~x1."
                          interval2
                          interval1)))
                    ((eq temp nil) (mv nil nil nil))
                    (t (tau-interval-endpoint-to-sign-k-token nil b-lo-rel b-lo-d))))))))
        ((eq temp nil) (mv nil nil nil))
        (t (let ((temp (tau-interval-endpoint-implication nil
                 a-lo-rel
                 a-lo-k
                 t
                 b-hi-rel
                 b-hi-d)))
            (cond ((eq temp t) (mv nil
                  nil
                  (er hard
                    'tau-interval-near-subsetp
                    "``A lo --> B hi'' returned T after ``A hi --> B hi'' ~
                       returned unknown (?).  This is not supposed to happen! ~
                       The only way a lower bound like ``A lo'' can imply an ~
                       upper bound like ``B hi'' is if the upper bound is ~
                       positive infinity (i.e., the bound is vacuous), in ~
                       which case ``A hi --> B hi'' would have succeeded.  A ~
                       is this tau-interval ~x0 and B is this one ~x1."
                    interval2
                    interval1)))
              ((eq temp nil) (mv nil nil nil))
              (t (let ((temp (tau-interval-endpoint-implication nil
                       a-lo-rel
                       a-lo-k
                       nil
                       b-lo-rel
                       b-lo-d)))
                  (cond ((eq temp t) (tau-interval-endpoint-to-sign-k-token t b-hi-rel b-hi-d))
                    ((eq temp nil) (mv nil nil nil))
                    (t (let ((temp (tau-interval-endpoint-implication t
                             a-hi-rel
                             a-hi-k
                             nil
                             b-lo-rel
                             b-lo-d)))
                        (cond ((eq temp t) (mv nil
                              nil
                              (er hard
                                'tau-interval-near-subsetp
                                "``A hi --> B lo'' returned T after ``A lo ~
                                  --> B lo'' returned unknown.  This is not ~
                                  supposed to happen!  The only way an upper ~
                                  bound like ``A hi'' can imply a lower bound ~
                                  like ``B lo'' is if the lower bound is ~
                                  negative infinity (i.e., the bound is ~
                                  vacuous), in which case ``A lo --> B lo'' ~
                                  would have succeeded.  A is this ~
                                  tau-interval ~x0 and B is this one ~x1."
                                interval2
                                interval1)))
                          (t (mv nil nil nil)))))))))))))))

(defun tau-near-subsetp
  (tau1 tau2 ens wrld)
  (let* ((temp1 (pos-evg-near-subsetp (access tau tau1 :pos-evg)
         (access tau tau2 :pos-evg))) (temp2 (cond ((null temp1) nil)
          (t (neg-evgs-near-subsetp (access tau tau1 :neg-evgs)
              (access tau tau2 :neg-evgs)
              nil
              (access tau tau2 :pos-pairs)
              (access tau tau2 :neg-pairs)
              (access tau tau2 :interval)
              ens
              wrld))))
      (temp3 (cond ((null temp2) nil)
          (t (tau-pairs-near-subsetp (access tau tau1 :pos-pairs)
              (access tau tau2 :pos-pairs)
              nil))))
      (temp4 (cond ((null temp3) nil)
          (t (tau-pairs-near-subsetp (access tau tau1 :neg-pairs)
              (access tau tau2 :neg-pairs)
              nil)))))
    (mv-let (sign5 k5 temp5)
      (cond ((null temp4) (mv nil nil nil))
        (t (tau-interval-near-subsetp (access tau tau1 :interval)
            (access tau tau2 :interval))))
      (cond ((null temp5) (mv nil nil nil))
        (t (if (eq temp1 t)
            (if (eq temp2 t)
              (if (eq temp3 t)
                (if (eq temp4 t)
                  (if (eq temp5 t)
                    (mv t nil nil)
                    (mv nil sign5 (cons k5 temp5)))
                  (if (eq temp5 t)
                    (mv nil nil temp4)
                    (mv nil nil nil)))
                (if (and (eq temp4 t) (eq temp5 t))
                  (mv nil t temp3)
                  (mv nil nil nil)))
              (if (and (eq temp3 t) (eq temp4 t) (eq temp5 t))
                (mv nil nil temp2)
                (mv nil nil nil)))
            (if (and (eq temp2 t) (eq temp3 t) (eq temp4 t) (eq temp5 t))
              (mv nil t temp1)
              (mv nil nil nil))))))))

(defun tau-put
  (p-sign p-recog q-sign q-recog ens wrld)
  (let ((p-discriminator (cdr p-recog)))
    (cond ((eq p-discriminator nil) (let ((a (car p-recog)) (q-discriminator (cdr q-recog)))
          (cond ((eq q-discriminator nil) (let ((b (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv (if (equal a b)
                        nil
                        t)
                      nil
                      wrld)
                    (mv (if (equal a b)
                        t
                        nil)
                      nil
                      wrld))
                  (if q-sign
                    (mv t nil wrld)
                    (mv nil nil wrld)))))
            ((eq q-discriminator :lessp-x-k) (let ((j (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv (if (< (fix a) j)
                        nil
                        t)
                      nil
                      wrld)
                    (mv (if (<= j (fix a))
                        nil
                        t)
                      nil
                      wrld))
                  (mv t nil wrld))))
            ((eq q-discriminator :lessp-k-x) (let ((j (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv (if (< j (fix a))
                        nil
                        t)
                      nil
                      wrld)
                    (mv (if (<= (fix a) j)
                        nil
                        t)
                      nil
                      wrld))
                  (mv t nil wrld))))
            (t (mv nil nil wrld)))))
      ((eq p-discriminator :lessp-x-k) (let ((i (car p-recog)) (q-discriminator (cdr q-recog)))
          (cond ((eq q-discriminator nil) (mv nil nil wrld))
            ((eq q-discriminator :lessp-x-k) (let ((j (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv (if (<= i j)
                        nil
                        t)
                      nil
                      wrld)
                    (mv t nil wrld))
                  (if q-sign
                    (mv t nil wrld)
                    (mv nil nil wrld)))))
            ((eq q-discriminator :lessp-k-x) (let ((j (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv t nil wrld)
                    (mv (if (<= i j)
                        nil
                        t)
                      nil
                      wrld))
                  (if q-sign
                    (mv (if (< j i)
                        nil
                        t)
                      nil
                      wrld)
                    (mv t nil wrld)))))
            (t (mv nil nil wrld)))))
      ((eq p-discriminator :lessp-k-x) (let ((i (car p-recog)) (q-discriminator (cdr q-recog)))
          (cond ((eq q-discriminator nil) (mv nil nil wrld))
            ((eq q-discriminator :lessp-x-k) (mv nil nil wrld))
            ((eq q-discriminator :lessp-k-x) (let ((j (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv (if (<= j i)
                        nil
                        t)
                      nil
                      wrld)
                    (mv t nil wrld))
                  (if q-sign
                    (mv t nil wrld)
                    (mv nil nil wrld)))))
            (t (mv nil nil wrld)))))
      (t (let ((p p-discriminator) (q-discriminator (cdr q-recog)))
          (cond ((eq q-discriminator nil) (let ((b (car q-recog)))
                (if p-sign
                  (if q-sign
                    (mv nil nil wrld)
                    (let ((val (ev-fncall-w-tau-recog p q-recog ens wrld)))
                      (cond ((eq val :unevalable) (mv nil
                            t
                            (putprop p
                              'unevalable-but-known
                              (cons (cons b nil)
                                (getpropc p 'unevalable-but-known nil wrld))
                              wrld)))
                        ((eq val nil) (mv nil nil wrld))
                        (t (mv t nil wrld)))))
                  (if q-sign
                    (mv nil nil wrld)
                    (let ((val (ev-fncall-w-tau-recog p q-recog ens wrld)))
                      (cond ((eq val :unevalable) (mv nil
                            t
                            (putprop p
                              'unevalable-but-known
                              (cons (cons b t)
                                (getpropc p 'unevalable-but-known nil wrld))
                              wrld)))
                        ((eq val nil) (mv t nil wrld))
                        (t (mv nil nil wrld))))))))
            (t (let* ((old-tau (tau-simple-implicants p-sign p-discriminator wrld)) (new-tau (add-to-tau1 q-sign q-recog old-tau ens wrld)))
                (cond ((eq new-tau *tau-contradiction*) (mv t
                      t
                      (putprop p-discriminator
                        (if p-sign
                          'pos-implicants
                          'neg-implicants)
                        *contradictory-tau*
                        wrld)))
                  ((equal old-tau new-tau) (mv nil nil wrld))
                  (t (mv nil
                      t
                      (putprop p-discriminator
                        (if p-sign
                          'pos-implicants
                          'neg-implicants)
                        new-tau
                        wrld))))))))))))

(defun monadic-boolean-fnp
  (fn ens wrld)
  (cond ((and (equal (arity fn wrld) 1)
       (member-eq (symbol-class fn wrld)
         '(:ideal :common-lisp-compliant))
       (not (member-eq fn *non-tau-monadic-boolean-functions*))) (mv-let (ts ttree)
        (type-set (fcons-term* fn '(v))
          nil
          nil
          nil
          ens
          wrld
          nil
          nil
          nil)
        (cond ((ts= ts *ts-boolean*) (mv t ttree)) (t (mv nil nil)))))
    (t (mv nil nil))))

(defun putprop-if-different
  (sym prop val wrld)
  (if (equal (getpropc sym prop *acl2-property-unbound* wrld) val)
    wrld
    (putprop sym prop val wrld)))

(defun tau-visit-function-introduction
  (fn wrld)
  (cond ((member-eq fn *primitive-monadic-booleans*) wrld)
    (t (putprop-if-different fn
        'tau-pair
        *acl2-property-unbound*
        (putprop-if-different fn
          'tau-pos-implicants
          *acl2-property-unbound*
          (putprop-if-different fn
            'tau-neg-implicants
            *acl2-property-unbound*
            (putprop-if-different fn
              'unevalable-but-known
              *acl2-property-unbound*
              (putprop-if-different fn
                'signature-rules-form-1
                *acl2-property-unbound*
                (putprop-if-different fn
                  'signature-rules-form-2
                  *acl2-property-unbound*
                  (putprop-if-different fn
                    'big-switch
                    *acl2-property-unbound*
                    wrld))))))))))

(defun tau-visit-function-introductions
  (fns wrld)
  (cond ((endp fns) wrld)
    (t (tau-visit-function-introductions (cdr fns)
        (tau-visit-function-introduction (car fns) wrld)))))

(defun putprop-tau-pair
  (fn wrld)
  (let ((old-pair (getpropc fn 'tau-pair-saved nil wrld)))
    (if old-pair
      (putprop fn 'tau-pair old-pair wrld)
      (let* ((nexti (global-val 'tau-next-index wrld)) (new-pair (cons nexti fn)))
        (putprop fn
          'tau-pair
          new-pair
          (putprop fn
            'tau-pair-saved
            new-pair
            (global-set 'tau-next-index (+ 1 nexti) wrld)))))))

(defun initialize-tau-pred
  (fn wrld)
  (let* ((wrld1 (putprop-tau-pair fn wrld)) (tau-pair (getpropc fn 'tau-pair nil wrld1))
      (wrld2 (putprop fn
          'pos-implicants
          (make tau
            :pos-evg nil
            :neg-evgs nil
            :pos-pairs (list tau-pair)
            :neg-pairs nil
            :interval nil)
          wrld1))
      (wrld3 (putprop fn
          'neg-implicants
          (make tau
            :pos-evg nil
            :neg-evgs nil
            :pos-pairs nil
            :neg-pairs (list tau-pair)
            :interval nil)
          wrld2)))
    wrld3))

(defun initialize-tau-preds
  (fns wrld)
  (cond ((endp fns) wrld)
    (t (initialize-tau-preds (cdr fns)
        (initialize-tau-pred (car fns) wrld)))))

(defun tau-boolean-formp
  (hyps concl wrld)
  (declare (ignore wrld))
  (and (null hyps)
    (case-match concl
      (('booleanp (f v)) (and (symbolp f) (symbolp v)))
      (& nil))))

(defun tau-eval-formp
  (hyps concl wrld)
  (and (null hyps)
    (mv-let (sign atm)
      (strip-not concl)
      (declare (ignore sign))
      (and (not (variablep atm))
        (not (fquotep atm))
        (symbolp (ffn-symb atm))
        (getpropc (ffn-symb atm) 'tau-pair nil wrld)
        (quotep (fargn atm 1))))))

(defun rune-<
  (x y)
  (cond ((eq (car x) (car y)) (or (symbol< (cadr x) (cadr y))
        (and (eq (cadr x) (cadr y))
          (cond ((null (cddr x)) (cddr y))
            ((null (cddr y)) nil)
            (t (< (cddr x) (cddr y)))))))
    ((symbol< (car x) (car y)) t)
    (t nil)))

(defun merge-runes-strict
  (l1 l2)
  (cond ((endp l1) l2)
    ((endp l2) l1)
    ((equal (car l1) (car l2)) (cons (car l1) (merge-runes-strict (cdr l1) (cdr l2))))
    ((rune-< (car l1) (car l2)) (cons (car l1) (merge-runes-strict (cdr l1) l2)))
    (t (cons (car l2) (merge-runes-strict l1 (cdr l2))))))

(defun merge-sort-runes-strict
  (lst)
  (cond ((endp (cdr lst)) lst)
    (t (let ((n (floor (length lst) 2)))
        (merge-runes-strict (merge-sort-runes-strict (take n lst))
          (merge-sort-runes-strict (nthcdr n lst)))))))

(defun get-tau-runes
  (wrld)
  (merge-sort-runes-strict (global-val 'tau-runes wrld)))

(defun set-tau-runes
  (flg val wrld)
  (let ((runes0 (global-val 'tau-runes wrld)))
    (global-set 'tau-runes
      (cond ((eq flg 'list) (append val runes0))
        (t (cons val runes0)))
      wrld)))

(defun add-tau-boolean-rule
  (rune hyps concl wrld)
  (declare (ignore hyps))
  (let ((fn (ffn-symb (fargn concl 1))))
    (cond ((getpropc fn 'tau-pair nil wrld) (set-tau-runes nil rune wrld))
      (t (initialize-tau-pred fn (set-tau-runes nil rune wrld))))))

(defun add-tau-eval-rule
  (rune hyps concl wrld)
  (declare (ignore hyps))
  (mv-let (sign atm)
    (strip-not concl)
    (let ((fn (ffn-symb atm)) (evg (cadr (fargn atm 1))))
      (putprop fn
        'unevalable-but-known
        (cons (cons evg
            (if sign
              nil
              t))
          (getpropc fn 'unevalable-but-known nil wrld))
        (set-tau-runes nil rune wrld)))))

(defun tau-like-subject-criterion
  (criterion x)
  (case criterion
    (:various-any :various-any)
    (:same-any x)
    (:various-var (if (variablep x)
        :various-var nil))
    (:same-var (if (variablep x)
        x
        nil))
    (otherwise (if (equal criterion x)
        criterion
        nil))))

(defun tau-like-term
  (term criterion wrld)
  (let ((equiv-fns '(equal eq eql =)) (inequality-fns '(< >)))
    (mv-let (sign atm)
      (if (ffn-symb-p term 'not)
        (mv nil (fargn term 1))
        (mv t term))
      (case-match atm
        ((fn e) (cond ((symbolp fn) (let ((tau-pair (getpropc fn 'tau-pair nil wrld)))
                (cond (tau-pair (let ((next-criterion (tau-like-subject-criterion criterion e)))
                      (cond (next-criterion (mv sign tau-pair e next-criterion))
                        (t (mv nil nil nil nil)))))
                  (t (mv nil nil nil nil)))))
            (t (mv nil nil nil nil))))
        ((g e ('quote . singleton-evg)) (cond ((member-eq g equiv-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)))
                (cond (next-criterion (mv sign singleton-evg e next-criterion))
                  (t (mv nil nil nil nil)))))
            ((member-eq g inequality-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)) (k (car singleton-evg)))
                (cond ((and next-criterion (rationalp k)) (mv sign
                      (if (eq g '<)
                        (cons k :lessp-x-k)
                        (cons k :lessp-k-x))
                      e
                      next-criterion))
                  (t (mv nil nil nil nil)))))
            (t (mv nil nil nil nil))))
        ((g ('quote . singleton-evg) e) (cond ((member-eq g equiv-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)))
                (cond (next-criterion (mv sign singleton-evg e next-criterion))
                  (t (mv nil nil nil nil)))))
            ((member-eq g inequality-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)) (k (car singleton-evg)))
                (cond ((and next-criterion (rationalp k)) (mv sign
                      (if (eq g '<)
                        (cons k :lessp-k-x)
                        (cons k :lessp-x-k))
                      e
                      next-criterion))
                  (t (mv nil nil nil nil)))))
            (t (mv nil nil nil nil))))
        (('if (g e ''0) ''t (g e ''1)) (cond ((member-eq g equiv-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)))
                (cond (next-criterion (mv sign *tau-bitp-pair* e next-criterion))
                  (t (mv nil nil nil nil)))))
            (t (mv nil nil nil nil))))
        (('if (g e ''1) ''t (g e ''0)) (cond ((member-eq g equiv-fns) (let ((next-criterion (tau-like-subject-criterion criterion e)))
                (cond (next-criterion (mv sign *tau-bitp-pair* e next-criterion))
                  (t (mv nil nil nil nil)))))
            (t (mv nil nil nil nil))))
        (& (mv nil nil nil nil))))))

(defun tau-like-term-listp
  (lst criterion wrld)
  (cond ((endp lst) criterion)
    (t (mv-let (sign recog e next-criterion)
        (tau-like-term (car lst) criterion wrld)
        (declare (ignore sign e))
        (cond ((null recog) nil)
          (t (tau-like-term-listp (cdr lst) next-criterion wrld)))))))

(defun tau-conjunctive-formp
  (hyps concl wrld)
  (let ((hyp-subject (and hyps (tau-like-term-listp hyps :same-var wrld))))
    (cond (hyp-subject (mv-let (sign recog e criterion)
          (tau-like-term concl hyp-subject wrld)
          (declare (ignore sign e criterion))
          (if recog
            t
            nil)))
      (t nil))))

(defun tau-simple-formp
  (hyps concl wrld)
  (and (tau-conjunctive-formp hyps concl wrld)
    (null (cdr hyps))))

(defun add-tau-simple-rule
  (rune hyps concl ens wrld)
  (mv-let (p-sign p-recog e criterion)
    (tau-like-term (car hyps) :various-any wrld)
    (declare (ignore e criterion))
    (mv-let (q-sign q-recog e criterion)
      (tau-like-term concl :various-any wrld)
      (declare (ignore e criterion))
      (mv-let (contradictionp changedp wrld)
        (tau-put* p-sign p-recog q-sign q-recog ens wrld)
        (declare (ignore contradictionp changedp))
        (set-tau-runes nil rune wrld)))))

(defun convert-tau-like-terms-to-tau
  (complete-flg terms ens wrld)
  (cond ((endp terms) *tau-empty*)
    (t (mv-let (sign recog e criterion)
        (tau-like-term (car terms) :various-any wrld)
        (declare (ignore e criterion))
        (let ((tau1 (convert-tau-like-terms-to-tau complete-flg
               (cdr terms)
               ens
               wrld)))
          (if complete-flg
            (add-to-tau sign recog tau1 ens wrld)
            (add-to-tau1 sign recog tau1 ens wrld)))))))

(defun add-tau-conjunctive-rule
  (rune hyps concl ens wrld)
  (let ((tau (convert-tau-like-terms-to-tau nil
         (append hyps
           (list (case-match concl (('not p) p) (& `(not ,CONCL)))))
         ens
         wrld)))
    (if (equal tau *tau-contradiction*)
      wrld
      (set-tau-runes nil
        rune
        (global-set 'tau-conjunctive-rules
          (cons tau (global-val 'tau-conjunctive-rules wrld))
          wrld)))))

(defun partition-signature-hyps-into-tau-alist-and-others
  (hyps alist others ens wrld)
  (cond ((endp hyps) (mv nil alist others))
    (t (mv-let (contradictionp alist others)
        (partition-signature-hyps-into-tau-alist-and-others (cdr hyps)
          alist
          others
          ens
          wrld)
        (cond (contradictionp (mv contradictionp nil nil))
          (t (mv-let (sign recog v criterion)
              (tau-like-term (car hyps) :various-var wrld)
              (declare (ignore criterion))
              (cond (recog (let ((old-tau (or (cdr (assoc-eq v alist)) *tau-empty*)))
                    (let ((new-tau (add-to-tau1 sign recog old-tau ens wrld)))
                      (cond ((eq new-tau *tau-contradiction*) (mv t nil nil))
                        (t (mv nil (put-assoc-eq v new-tau alist) others))))))
                (t (mv nil alist (cons (car hyps) others)))))))))))

(defun tau-boolean-signature-formp
  (hyps concl)
  (cond ((null hyps) (let ((e (case-match concl
             (('if ('equal e ''t) ''t ('equal e ''nil)) e)
             (('if ('equal e ''t) ('equal e ''t) ('equal e ''nil)) e)
             (('if ('equal e ''nil) ''t ('equal e ''t)) e)
             (('if ('equal e ''nil) ('equal e ''nil) ('equal e ''t)) e)
             (& nil))))
        (and e
          (nvariablep e)
          (not (fquotep e))
          (symbolp (ffn-symb e))
          (symbol-listp (fargs e))
          (no-duplicatesp-eq (fargs e)))))
    (t nil)))

(defun tau-signature-formp
  (hyps concl wrld)
  (cond ((member-equal *nil* hyps) nil)
    ((tau-boolean-signature-formp hyps concl) 1)
    (t (mv-let (sign recog e criterion)
        (tau-like-term concl :same-any wrld)
        (declare (ignore sign criterion))
        (cond ((or (null recog) (variablep e) (fquotep e)) nil)
          ((or (eq (ffn-symb e) 'mv-nth)
             (member-eq (ffn-symb e)
               (global-val 'tau-mv-nth-synonyms wrld))) (cond ((and (quotep (fargn e 1)) (natp (cadr (fargn e 1)))) (let ((e (fargn e 2)))
                  (cond ((and (nvariablep e)
                       (not (fquotep e))
                       (symbolp (ffn-symb e))
                       (symbol-listp (fargs e))
                       (no-duplicatesp-eq (fargs e))
                       (not (ffnnamep-lst (ffn-symb e) hyps))
                       (subsetp (all-vars1-lst hyps nil) (fargs e))) 2)
                    (t nil))))
              (t nil)))
          ((and (symbolp (ffn-symb e))
             (nvariablep e)
             (not (fquotep e))
             (symbolp (ffn-symb e))
             (symbol-listp (fargs e))
             (no-duplicatesp-eq (fargs e))
             (not (ffnnamep-lst (ffn-symb e) hyps))
             (subsetp (all-vars1-lst hyps nil) (fargs e))) 1)
          (t nil))))))

(defun replace-vars-by-bindings
  (vars alist)
  (cond ((endp vars) nil)
    (t (cons (or (cdr (assoc-eq (car vars) alist)) *tau-empty*)
        (replace-vars-by-bindings (cdr vars) alist)))))

(defun add-tau-signature-rule
  (rune form hyps concl ens wrld)
  (let ((concl (if (tau-boolean-signature-formp hyps concl)
         `(booleanp ,(FARGN (FARGN CONCL 1) 1))
         concl)))
    (mv-let (sign recog e criterion)
      (tau-like-term concl :various-any wrld)
      (declare (ignore criterion))
      (let* ((temp recog) (recog (if temp
              recog
              *tau-booleanp-pair*))
          (sign (if temp
              sign
              t))
          (e (if temp
              e
              (fargn concl 1))))
        (let* ((fn (if (eql form 1)
               (ffn-symb e)
               (ffn-symb (fargn e 2)))) (i (if (eql form 1)
                nil
                (cadr (fargn e 1))))
            (vars (fargs (if (eql form 1)
                  e
                  (fargn e 2)))))
          (mv-let (contradictionp alist others)
            (partition-signature-hyps-into-tau-alist-and-others hyps
              nil
              nil
              ens
              wrld)
            (cond (contradictionp wrld)
              (t (let ((rule (make signature-rule
                       :input-tau-list (replace-vars-by-bindings vars alist)
                       :vars vars
                       :dependent-hyps others
                       :output-sign sign
                       :output-recog recog)))
                  (cond ((eql form 1) (let ((sigs (getpropc fn 'signature-rules-form-1 nil wrld)))
                        (if (member-equal rule sigs)
                          wrld
                          (set-tau-runes nil
                            rune
                            (putprop fn 'signature-rules-form-1 (cons rule sigs) wrld)))))
                    (t (let ((sigs (getpropc fn 'signature-rules-form-2 nil wrld)))
                        (if (member-equal rule (nth i sigs))
                          wrld
                          (set-tau-runes nil
                            rune
                            (putprop fn
                              'signature-rules-form-2
                              (update-nth i (cons rule (nth i sigs)) sigs)
                              wrld)))))))))))))))

(defun switch-varp
  (v term wrld)
  (case-match term
    (('if x y z) (mv-let (sign recog e criterion)
        (tau-like-term x :various-any wrld)
        (declare (ignore sign criterion))
        (cond ((and recog
             (eq v e)
             (switch-varp v y wrld)
             (switch-varp v z wrld)) t)
          (t (not (occur v term))))))
    (& (not (occur v term)))))

(defun tau-big-switch-equationp
  (term wrld)
  (case-match term
    (('equal (fn . vars) ('if test x y)) (let* ((test-vars (all-vars test)) (v (car test-vars))
          (body-vars (all-vars1 y (all-vars1 x test-vars))))
        (and (symbolp fn)
          (not (equal fn 'quote))
          (not (getpropc fn 'tau-pair nil wrld))
          (not (getpropc fn 'big-switch nil wrld))
          (symbol-listp vars)
          (no-duplicatesp vars)
          test-vars
          (null (cdr test-vars))
          (subsetp-eq body-vars vars)
          (mv-let (sign recog e criterion)
            (tau-like-term test :various-any wrld)
            (declare (ignore sign criterion))
            (and recog (eq e v)))
          (not (ffnnamep fn (fargn term 2)))
          (switch-varp v x wrld)
          (switch-varp v y wrld))))
    (& nil)))

(defun tau-big-switch-var
  (term)
  (mv-let (sign test)
    (strip-not (fargn (fargn term 2) 1))
    (declare (ignore sign))
    (cond ((null (cdr (fargs test))) (fargn test 1))
      ((quotep (fargn test 1)) (fargn test 2))
      (t (fargn test 1)))))

(defun tau-big-switch-formp
  (hyps concl wrld)
  (and (null hyps) (tau-big-switch-equationp concl wrld)))

(defun add-tau-big-switch-rule
  (rune hyps concl wrld)
  (declare (ignore hyps))
  (let* ((fn (ffn-symb (fargn concl 1))) (formals (fargs (fargn concl 1)))
      (body (fargn concl 2))
      (switch-var (tau-big-switch-var concl))
      (switch-var-pos (- (length formals) (length (member-eq switch-var formals)))))
    (set-tau-runes nil
      rune
      (putprop fn
        'big-switch
        (make big-switch-rule
          :formals formals
          :switch-var switch-var
          :switch-var-pos switch-var-pos
          :body body)
        wrld))))

(defun tau-mv-nth-synonym-formp
  (hyps concl)
  (and (null hyps)
    (case-match concl
      (('equal (fn x y) ('mv-nth x y)) (and (not (flambdap fn))
          (variablep x)
          (variablep y)
          (not (eq x y))))
      (('equal ('mv-nth x y) (fn x y)) (and (not (flambdap fn))
          (variablep x)
          (variablep y)
          (not (eq x y))))
      (& nil))))

(defun add-tau-mv-nth-synonym-rule
  (rune hyps concl wrld)
  (declare (ignore hyps))
  (let* ((fn (if (eq (ffn-symb (fargn concl 1)) 'mv-nth)
         (ffn-symb (fargn concl 2))
         (ffn-symb (fargn concl 1)))) (fns (global-val 'tau-mv-nth-synonyms wrld)))
    (cond ((member-eq fn fns) wrld)
      (t (set-tau-runes nil
          rune
          (global-set 'tau-mv-nth-synonyms (cons fn fns) wrld))))))

(defun all-cars-nil
  (pairs)
  (cond ((endp pairs) t)
    (t (and (null (car (car pairs))) (all-cars-nil (cdr pairs))))))

(defun find-subject-bounder-link-term
  (pairs pairs0)
  (cond ((endp pairs) nil)
    ((and (null (car (car pairs)))
       (ffn-symb-p (cdr (car pairs)) 'in-tau-intervalp)
       (member-equal (cons nil (cons 'tau-intervalp (cddr (cdr (car pairs)))))
         pairs0)) (cdr (car pairs)))
    (t (find-subject-bounder-link-term (cdr pairs) pairs0))))

(defun tau-bounder-doms-extraction
  (term ivars ivar)
  (case-match term
    (('equal ('tau-interval-dom v) ('quote evg)) (cond ((and (if ivar
             (eq v ivar)
             (member-eq v ivars))
           (member-eq evg '(integerp rationalp acl2-numberp nil))) (mv v (list evg)))
        (t (mv nil nil))))
    (('if ('equal ('tau-interval-dom v) ('quote evg))
       ('equal ('tau-interval-dom v) ('quote evg))
       else-term) (cond ((and (if ivar
             (eq v ivar)
             (member-eq v ivars))
           (member-eq evg '(integerp rationalp acl2-numberp nil))) (mv-let (ivar doms)
            (tau-bounder-doms-extraction else-term ivars v)
            (cond (ivar (mv ivar (add-to-set-eq evg doms)))
              (t (mv nil nil)))))
        (t (mv nil nil))))
    (& (mv nil nil))))

(defun tau-bounder-hyp-extraction
  (hyps svars
    ivars
    missing-ivars1
    missing-ivars2
    ivar-to-doms-alist
    ivar-to-svar-pos-alist
    svar-to-ivar-alist)
  (cond ((endp hyps) (cond ((and (null missing-ivars1) (null missing-ivars2)) (mv t
            ivar-to-doms-alist
            ivar-to-svar-pos-alist
            svar-to-ivar-alist))
        (t (mv nil nil nil nil))))
    ((or (variablep (car hyps)) (fquotep (car hyps))) (mv nil nil nil nil))
    ((eq (ffn-symb (car hyps)) 'tau-intervalp) (let ((ivar (fargn (car hyps) 1)))
        (cond ((member-eq ivar missing-ivars1) (tau-bounder-hyp-extraction (cdr hyps)
              svars
              ivars
              (remove1-eq ivar missing-ivars1)
              missing-ivars2
              ivar-to-doms-alist
              ivar-to-svar-pos-alist
              svar-to-ivar-alist))
          (t (mv nil nil nil nil)))))
    ((eq (ffn-symb (car hyps)) 'in-tau-intervalp) (let ((svar (fargn (car hyps) 1)) (ivar (fargn (car hyps) 2)))
        (cond ((and (member-eq svar svars)
             (member-eq ivar missing-ivars2)
             (not (assoc-eq svar svar-to-ivar-alist))) (let ((n (- (len svars) (len (member-eq svar svars)))))
              (tau-bounder-hyp-extraction (cdr hyps)
                svars
                ivars
                missing-ivars1
                (remove1-eq ivar missing-ivars2)
                ivar-to-doms-alist
                (cons (cons ivar n) ivar-to-svar-pos-alist)
                (cons (cons svar ivar) svar-to-ivar-alist))))
          (t (mv nil nil nil nil)))))
    (t (mv-let (ivar doms)
        (tau-bounder-doms-extraction (car hyps) ivars nil)
        (cond ((and ivar (not (assoc-eq ivar ivar-to-doms-alist))) (tau-bounder-hyp-extraction (cdr hyps)
              svars
              ivars
              missing-ivars1
              missing-ivars2
              (cons (cons ivar doms) ivar-to-doms-alist)
              ivar-to-svar-pos-alist
              svar-to-ivar-alist))
          (t (mv nil nil nil nil)))))))

(defun acceptable-domains-for-bounder
  (svars svar-to-ivar-alist ivar-to-doms-alist)
  (cond ((endp svars) nil)
    (t (let ((temp (assoc-eq (car svars) svar-to-ivar-alist)))
        (cons (cond ((null temp) *all-interval-domains*)
            (t (let* ((ivar (cdr temp)) (temp (assoc-eq ivar ivar-to-doms-alist)))
                (cond ((null temp) *all-interval-domains*) (t (cdr temp))))))
          (acceptable-domains-for-bounder (cdr svars)
            svar-to-ivar-alist
            ivar-to-doms-alist))))))

(defun bounder-args
  (ivars ivar-to-svar-pos-alist)
  (cond ((endp ivars) nil)
    (t (cons (cdr (assoc-eq (car ivars) ivar-to-svar-pos-alist))
        (bounder-args (cdr ivars) ivar-to-svar-pos-alist)))))

(defun tau-bounder-formp
  (term wrld)
  (cond ((ffn-symb-p term 'implies) (let* ((hyp-pairs (unprettyify (fargn term 1))) (concl-pairs (unprettyify (fargn term 2)))
          (link-term (find-subject-bounder-link-term concl-pairs concl-pairs)))
        (cond ((and link-term
             (all-cars-nil hyp-pairs)
             (nvariablep (fargn link-term 1))
             (not (fquotep (fargn link-term 1)))
             (nvariablep (fargn link-term 2))
             (not (fquotep (fargn link-term 2)))
             (symbolp (ffn-symb (fargn link-term 2)))
             (symbol-listp (fargs (fargn link-term 2)))
             (no-duplicatesp-eq (fargs (fargn link-term 2)))) (cond ((or (eq (ffn-symb (fargn link-term 1)) 'mv-nth)
                 (member-eq (ffn-symb (fargn link-term 1))
                   (global-val 'tau-mv-nth-synonyms wrld))) (cond ((and (quotep (fargn (fargn link-term 1) 1))
                     (natp (cadr (fargn (fargn link-term 1) 1)))) (let ((j (cadr (fargn (fargn link-term 1) 1))) (subject-term (fargn (fargn link-term 1) 2))
                        (bounder-fn (ffn-symb (fargn link-term 2)))
                        (ivars (fargs (fargn link-term 2))))
                      (cond ((and (nvariablep subject-term)
                           (not (fquotep subject-term))
                           (symbolp (ffn-symb subject-term))
                           (symbol-listp (fargs subject-term))
                           (no-duplicatesp-eq (fargs subject-term))
                           (not (intersectp-eq (fargs subject-term) ivars))) (let ((fn (ffn-symb subject-term)) (svars (fargs subject-term))
                              (hyps (strip-cdrs hyp-pairs)))
                            (mv-let (flg ivar-to-doms-alist
                                ivar-to-svar-pos-alist
                                svar-to-ivar-alist)
                              (tau-bounder-hyp-extraction hyps
                                svars
                                ivars
                                ivars
                                ivars
                                nil
                                nil
                                nil)
                              (cond (flg (mv 2
                                    j
                                    (make bounder-correctness
                                      :subject-fn fn
                                      :acceptable-domains (acceptable-domains-for-bounder svars
                                        svar-to-ivar-alist
                                        ivar-to-doms-alist)
                                      :bounder-fn bounder-fn
                                      :bounder-args (bounder-args ivars ivar-to-svar-pos-alist))))
                                (t (mv nil nil nil))))))
                        (t (mv nil nil nil)))))
                  (t (mv nil nil nil))))
              (t (let ((j nil) (subject-term (fargn link-term 1))
                    (bounder-fn (ffn-symb (fargn link-term 2)))
                    (ivars (fargs (fargn link-term 2))))
                  (cond ((and (nvariablep subject-term)
                       (not (fquotep subject-term))
                       (symbolp (ffn-symb subject-term))
                       (symbol-listp (fargs subject-term))
                       (no-duplicatesp-eq (fargs subject-term))
                       (not (intersectp-eq (fargs subject-term) ivars))) (let ((fn (ffn-symb subject-term)) (svars (fargs subject-term))
                          (hyps (strip-cdrs hyp-pairs)))
                        (mv-let (flg ivar-to-doms-alist
                            ivar-to-svar-pos-alist
                            svar-to-ivar-alist)
                          (tau-bounder-hyp-extraction hyps
                            svars
                            ivars
                            ivars
                            ivars
                            nil
                            nil
                            nil)
                          (cond (flg (mv 1
                                j
                                (make bounder-correctness
                                  :subject-fn fn
                                  :acceptable-domains (acceptable-domains-for-bounder svars
                                    svar-to-ivar-alist
                                    ivar-to-doms-alist)
                                  :bounder-fn bounder-fn
                                  :bounder-args (bounder-args ivars ivar-to-svar-pos-alist))))
                            (t (mv nil nil nil))))))
                    (t (mv nil nil nil)))))))
          (t (mv nil nil nil)))))
    (t (mv nil nil nil))))

(defun pairwise-subsetp-eq
  (doms-lst1 doms-lst2)
  (cond ((endp doms-lst1) t)
    ((subsetp-eq (car doms-lst1) (car doms-lst2)) (pairwise-subsetp-eq (cdr doms-lst1) (cdr doms-lst2)))
    (t nil)))

(defun bounder-subsumedp
  (bc1 bc2)
  (and (eq (access bounder-correctness bc1 :bounder-fn)
      (access bounder-correctness bc2 :bounder-fn))
    (equal (access bounder-correctness bc1 :bounder-args)
      (access bounder-correctness bc2 :bounder-args))
    (pairwise-subsetp-eq (access bounder-correctness bc1 :acceptable-domains)
      (access bounder-correctness bc2 :acceptable-domains))
    (eq (access bounder-correctness bc1 :subject-fn)
      (access bounder-correctness bc2 :subject-fn))))

(defun bounder-subsumedp-by-some
  (bc bounders)
  (cond ((endp bounders) nil)
    ((bounder-subsumedp bc (car bounders)) t)
    (t (bounder-subsumedp-by-some bc (cdr bounders)))))

(defun delete-some-subsumed-bounders
  (bc bounders)
  (cond ((endp bounders) nil)
    ((bounder-subsumedp (car bounders) bc) (delete-some-subsumed-bounders bc (cdr bounders)))
    (t (cons (car bounders)
        (delete-some-subsumed-bounders bc (cdr bounders))))))

(defun add-bounder-to-bounders
  (bc bounders)
  (cond ((bounder-subsumedp-by-some bc bounders) bounders)
    (t (cons bc (delete-some-subsumed-bounders bc bounders)))))

(defun add-tau-bounder-rule
  (rune form j bc wrld)
  (let ((subject-fn (access bounder-correctness bc :subject-fn)))
    (cond ((equal form 1) (let* ((bounders0 (getpropc subject-fn 'tau-bounders-form-1 nil wrld)) (bounders1 (add-bounder-to-bounders bc bounders0)))
          (if (equal bounders0 bounders1)
            wrld
            (set-tau-runes nil
              rune
              (putprop subject-fn 'tau-bounders-form-1 bounders1 wrld)))))
      (t (let* ((slots (getpropc subject-fn 'tau-bounders-form-2 nil wrld)) (bounders0 (nth j slots))
            (bounders1 (add-bounder-to-bounders bc bounders0)))
          (if (equal bounders0 bounders1)
            wrld
            (set-tau-runes nil
              rune
              (putprop subject-fn
                'tau-bounders-form-2
                (update-nth j bounders1 slots)
                wrld))))))))

(defun strip-force-and-case-split-in-hyps-of-pairs
  (pairs)
  (cond ((endp pairs) nil)
    (t (cons (cons (strip-force-and-case-split (car (car pairs)))
          (cdr (car pairs)))
        (strip-force-and-case-split-in-hyps-of-pairs (cdr pairs))))))

(defun acceptable-tau-rulep
  (pair wrld)
  (let ((hyps (car pair)) (concl (cdr pair)))
    (cond ((tau-boolean-formp hyps concl wrld) 'boolean)
      ((tau-eval-formp hyps concl wrld) 'eval)
      ((tau-simple-formp hyps concl wrld) 'simple)
      ((tau-conjunctive-formp hyps concl wrld) 'conjunctive)
      (t (let ((n (tau-signature-formp hyps concl wrld)))
          (cond ((equal n 1) 'signature-form-1)
            ((equal n 2) 'signature-form-2)
            ((tau-big-switch-formp hyps concl wrld) 'big-switch)
            ((tau-mv-nth-synonym-formp hyps concl) 'mv-nth-synonym)
            (t nil)))))))

(defun acceptable-tau-rulesp
  (flg pairs wrld)
  (cond ((endp pairs) (eq flg :all))
    ((acceptable-tau-rulep (car pairs) wrld) (if (eq flg :all)
        (acceptable-tau-rulesp flg (cdr pairs) wrld)
        t))
    ((eq flg :all) nil)
    (t (acceptable-tau-rulesp flg (cdr pairs) wrld))))

(defun acceptable-tau-rules
  (pairs wrld)
  (cond ((endp pairs) nil)
    ((acceptable-tau-rulep (car pairs) wrld) (cons (car pairs) (acceptable-tau-rules (cdr pairs) wrld)))
    (t (acceptable-tau-rules (cdr pairs) wrld))))

(defun cross-prod1
  (lst lst-lst acc)
  (cond ((endp lst-lst) acc)
    (t (cross-prod1 lst
        (cdr lst-lst)
        (cons (append lst (car lst-lst)) acc)))))

(defun cross-prod2
  (lst1 lst2 acc)
  (cond ((endp lst1) (reverse acc))
    (t (cross-prod2 (cdr lst1)
        lst2
        (cross-prod1 (car lst1) lst2 acc)))))

(defun cross-prod (lst1 lst2) (cross-prod2 lst1 lst2 nil))

(defun cnf-dnf
  (sign term cnfp)
  (cond ((variablep term) (list (list (if sign
            term
            (list 'not term)))))
    ((fquotep term) (let ((val (if (eq (cadr term) nil)
             (not sign)
             sign)))
        (if val
          (if cnfp
            nil
            '(nil))
          (if cnfp
            '(nil)
            nil))))
    ((eq (ffn-symb term) 'not) (cnf-dnf (not sign) (fargn term 1) (not cnfp)))
    ((eq (ffn-symb term) 'if) (let ((x (fargn term 1)) (y (fargn term 2)) (z (fargn term 3)))
        (cond ((equal z *nil*) (if cnfp
              (append (cnf-dnf sign x cnfp) (cnf-dnf sign y cnfp))
              (cross-prod (cnf-dnf sign x cnfp) (cnf-dnf sign y cnfp))))
          ((equal y *nil*) (if cnfp
              (append (cnf-dnf (not sign) x cnfp) (cnf-dnf sign z cnfp))
              (cross-prod (cnf-dnf (not sign) x cnfp)
                (cnf-dnf sign z cnfp))))
          ((equal z *t*) (if cnfp
              (cross-prod (cnf-dnf (not sign) x cnfp)
                (cnf-dnf sign y cnfp))
              (append (cnf-dnf (not sign) x cnfp) (cnf-dnf sign y cnfp))))
          ((or (equal x y) (equal y *t*)) (if cnfp
              (cross-prod (cnf-dnf sign x cnfp) (cnf-dnf sign z cnfp))
              (append (cnf-dnf sign x cnfp) (cnf-dnf sign z cnfp))))
          (t (list (list (if sign
                  term
                  (list 'not term))))))))
    (t (list (list (if sign
            term
            (list 'not term)))))))

(defun split-on-conjoined-disjunctions
  (lst)
  (cond ((endp lst) nil)
    ((endp (cdr lst)) (cnf-dnf t (car lst) nil))
    (t (cross-prod (cnf-dnf t (car lst) nil)
        (split-on-conjoined-disjunctions (cdr lst))))))

(defun split-on-conjoined-disjunctions-in-hyps-of-pairs
  (pairs)
  (cond ((endp pairs) nil)
    (t (let ((hyps-lst (split-on-conjoined-disjunctions (car (car pairs)))))
        (cond ((endp hyps-lst) (cons (car pairs)
              (split-on-conjoined-disjunctions-in-hyps-of-pairs (cdr pairs))))
          (t (append (pairlis-x2 hyps-lst (cdr (car pairs)))
              (split-on-conjoined-disjunctions-in-hyps-of-pairs (cdr pairs)))))))))

(defun chk-acceptable-tau-rule
  (name term ctx wrld state)
  (let ((term1 (remove-guard-holders term wrld)))
    (mv-let (form j bc)
      (tau-bounder-formp term1 wrld)
      (declare (ignore j bc))
      (cond (form (value nil))
        (t (let ((pairs (split-on-conjoined-disjunctions-in-hyps-of-pairs (strip-force-and-case-split-in-hyps-of-pairs (unprettyify term1)))))
            (cond ((acceptable-tau-rulesp :all pairs wrld) (value nil))
              ((null (cdr pairs)) (er soft
                  ctx
                  "The formula of the theorem ~x0 fails to fit any of the forms ~
               for acceptable :TAU-SYSTEM rules.  See :DOC tau-system for the ~
               details of the acceptable forms."
                  name))
              (t (er soft
                  ctx
                  "The formula of the theorem ~x0 gives rise to ~n1 normalized ~
                 formulas (e.g., after stripping out conjuncts in the ~
                 conclusion, etc.).  In order to be a :TAU-SYSTEM rule, each ~
                 of these formulas must be acceptable as a tau rule and at ~
                 least one of them fails to be.  See :DOC tau for details of ~
                 the acceptable forms."
                  name
                  (length pairs))))))))))

(defun add-tau-rule1
  (lost-rune-action rune pairs ens wrld wrld0)
  (cond ((endp pairs) (mv nil wrld))
    (t (mv-let (msgp wrld)
        (let* ((hyps (car (car pairs))) (concl (cdr (car pairs)))
            (kind (acceptable-tau-rulep (cons hyps concl) wrld)))
          (case kind
            (boolean (mv nil (add-tau-boolean-rule rune hyps concl wrld)))
            (eval (mv nil (add-tau-eval-rule rune hyps concl wrld)))
            (simple (mv nil (add-tau-simple-rule rune hyps concl ens wrld)))
            (conjunctive (mv nil (add-tau-conjunctive-rule rune hyps concl ens wrld)))
            (signature-form-1 (mv nil (add-tau-signature-rule rune 1 hyps concl ens wrld)))
            (signature-form-2 (mv nil (add-tau-signature-rule rune 2 hyps concl ens wrld)))
            (big-switch (mv nil (add-tau-big-switch-rule rune hyps concl wrld)))
            (mv-nth-synonym (mv nil (add-tau-mv-nth-synonym-rule rune hyps concl wrld)))
            (otherwise (cond ((eq lost-rune-action 'report) (mv (msg "Unable to generate a :TAU-SYSTEM rule for the rune ~x0 ~
                    with formula ~x1.  A possible explanation is that we are ~
                    in the second pass of an ENCAPSULATE (e.g., we've just ~
                    printed ``End of Encapsulated Events.''). If so, then ~
                    evidently the formula in question was accepted during the ~
                    first pass but is no longer acceptable.  This can happen ~
                    if the ENCAPSULATE established too few constraints.  For ~
                    example, the local witness to some monadic function might ~
                    have been Boolean but that fact was not exported as ~
                    :TAU-SYSTEM (or, in tau automatic mode, ~
                    :TYPE-PRESCRIPTION) rule.  See :DOC tau for the details ~
                    of the acceptable forms of :TAU-SYSTEM rules."
                      rune
                      (reprettyify hyps concl wrld))
                    wrld0))
                ((eq lost-rune-action 'accumulate) (mv nil
                    (global-set 'tau-lost-runes
                      (cons rune (global-val 'tau-lost-runes wrld))
                      wrld)))
                (t (mv nil wrld))))))
        (cond (msgp (mv msgp wrld0))
          (t (add-tau-rule1 lost-rune-action
              rune
              (cdr pairs)
              ens
              wrld
              wrld0)))))))

(defun add-tau-rule
  (first-visitp rune term ens wrld0)
  (let ((term1 (remove-guard-holders term wrld0)))
    (mv-let (form j bc)
      (tau-bounder-formp term1 wrld0)
      (cond (form (mv nil (add-tau-bounder-rule rune form j bc wrld0)))
        (t (let* ((pairs (split-on-conjoined-disjunctions-in-hyps-of-pairs (strip-force-and-case-split-in-hyps-of-pairs (unprettyify term1)))) (lost-rune-action (if (eq (car rune) :tau-system)
                  (if first-visitp
                    'report
                    'accumulate)
                  'ignore)))
            (add-tau-rule1 lost-rune-action rune pairs ens wrld0 wrld0)))))))

(defun discover-tau-pred
  (fn ens wrld)
  (mv-let (monadic-booleanp ttree)
    (monadic-boolean-fnp fn ens wrld)
    (cond (monadic-booleanp (initialize-tau-pred fn
          (set-tau-runes 'list (tagged-objects 'lemma ttree) wrld)))
      (t wrld))))

(defun discover-tau-preds
  (fns ens wrld)
  (cond ((endp fns) wrld)
    (t (discover-tau-preds (cdr fns)
        ens
        (discover-tau-pred (car fns) ens wrld)))))

(defun tau-rules-from-type-prescriptions
  (tp-lst fn ens wrld wrld0)
  (cond ((endp tp-lst) (mv nil wrld))
    ((and (eq (cadr (access type-prescription (car tp-lst) :rune)) fn)
       (enabled-numep (access type-prescription (car tp-lst) :nume)
         ens)) (mv-let (term ttree)
        (convert-type-prescription-to-term (car tp-lst) ens wrld)
        (let ((pairs (acceptable-tau-rules (split-on-conjoined-disjunctions-in-hyps-of-pairs (strip-force-and-case-split-in-hyps-of-pairs (unprettyify (remove-guard-holders term wrld0))))
               wrld)))
          (cond ((null pairs) (tau-rules-from-type-prescriptions (cdr tp-lst)
                fn
                ens
                wrld
                wrld0))
            (t (mv-let (msgp wrld)
                (add-tau-rule1 'ignore
                  (access type-prescription (car tp-lst) :rune)
                  pairs
                  ens
                  wrld
                  wrld0)
                (cond (msgp (mv msgp wrld0))
                  (t (tau-rules-from-type-prescriptions (cdr tp-lst)
                      fn
                      ens
                      (set-tau-runes 'list (tagged-objects 'lemma ttree) wrld)
                      wrld0)))))))))
    (t (tau-rules-from-type-prescriptions (cdr tp-lst)
        fn
        ens
        wrld
        wrld0))))

(defun original-def-body1
  (fn def-bodies)
  (cond ((endp def-bodies) nil)
    ((eq (cadr (access def-body (car def-bodies) :rune)) fn) (car def-bodies))
    (t (original-def-body1 fn (cdr def-bodies)))))

(defun original-def-body
  (fn wrld)
  (original-def-body1 fn (getpropc fn 'def-bodies nil wrld)))

(defun tau-like-propositionp
  (var term wrld)
  (mv-let (sign recog e criteria)
    (tau-like-term term var wrld)
    (declare (ignore sign e criteria))
    (cond (recog t)
      ((variablep term) nil)
      ((fquotep term) (or (equal term *t*) (equal term *nil*)))
      ((eq (ffn-symb term) 'if) (and (tau-like-propositionp var (fargn term 1) wrld)
          (tau-like-propositionp var (fargn term 2) wrld)
          (tau-like-propositionp var (fargn term 3) wrld)))
      ((eq (ffn-symb term) 'return-last) (tau-like-propositionp var (fargn term 3) wrld))
      ((and (eq (ffn-symb term) 'not) (eq (ffn-symb term) 'null)) (tau-like-propositionp var (fargn term 1) wrld))
      ((or (eq (ffn-symb term) 'implies) (eq (ffn-symb term) 'iff)) (and (tau-like-propositionp var (fargn term 1) wrld)
          (tau-like-propositionp var (fargn term 2) wrld)))
      (t nil))))

(defun expand-tau-like-proposition
  (term)
  (cond ((variablep term) term)
    ((fquotep term) term)
    ((eq (ffn-symb term) 'if) (fcons-term* 'if
        (expand-tau-like-proposition (fargn term 1))
        (expand-tau-like-proposition (fargn term 2))
        (expand-tau-like-proposition (fargn term 3))))
    ((eq (ffn-symb term) 'return-last) (expand-tau-like-proposition (fargn term 3)))
    ((or (eq (ffn-symb term) 'not) (eq (ffn-symb term) 'null)) (fcons-term* 'not
        (expand-tau-like-proposition (fargn term 1))))
    ((eq (ffn-symb term) 'implies) (fcons-term* 'if
        (expand-tau-like-proposition (fargn term 1))
        (expand-tau-like-proposition (fargn term 2))
        *t*))
    ((eq (ffn-symb term) 'iff) (let ((arg2 (expand-tau-like-proposition (fargn term 2))))
        (fcons-term* 'if
          (expand-tau-like-proposition (fargn term 1))
          arg2
          (fcons-term* 'not arg2))))
    (t term)))

(defun add-only-simple-and-conjunctive-tau-rules
  (rune pairs ens wrld)
  (cond ((endp pairs) wrld)
    (t (add-only-simple-and-conjunctive-tau-rules rune
        (cdr pairs)
        ens
        (let ((hyps (car (car pairs))) (concl (cdr (car pairs))))
          (cond ((tau-conjunctive-formp hyps concl wrld) (cond ((null (cdr hyps)) (add-tau-simple-rule rune hyps concl ens wrld))
                (t (add-tau-conjunctive-rule rune hyps concl ens wrld))))
            (t wrld)))))))

(defun convert-normalized-term-to-pairs
  (rhyps term ans)
  (cond ((variablep term) (cons (cons (revappend rhyps nil) term) ans))
    ((fquotep term) (if (equal term *nil*)
        (cond ((consp rhyps) (cons (cons (revappend (cdr rhyps) nil)
                (dumb-negate-lit (car rhyps)))
              ans))
          (t (cons (cons nil *nil*) ans)))
        ans))
    ((eq (ffn-symb term) 'if) (cond ((equal (fargn term 3) *nil*) (convert-normalized-term-to-pairs rhyps
            (fargn term 2)
            (cons (cons (revappend rhyps nil) (fargn term 1)) ans)))
        ((equal (fargn term 2) *nil*) (convert-normalized-term-to-pairs rhyps
            (fargn term 3)
            (cons (cons (revappend rhyps nil)
                (dumb-negate-lit (fargn term 1)))
              ans)))
        (t (convert-normalized-term-to-pairs (cons (fargn term 1) rhyps)
            (fargn term 2)
            (convert-normalized-term-to-pairs (cons (dumb-negate-lit (fargn term 1)) rhyps)
              (fargn term 3)
              ans)))))
    (t (cons (cons (revappend rhyps nil) term) ans))))

(defun complementaryp
  (lit1 lit2)
  (declare (xargs :guard (and (pseudo-termp lit1) (pseudo-termp lit2))))
  (or (and (ffn-symb-p lit1 'not) (equal (fargn lit1 1) lit2))
    (and (ffn-symb-p lit2 'not) (equal (fargn lit2 1) lit1))))

(defun subsumes-but-for-one-negation
  (hyps1 hyps2 ancestor-lits)
  (cond ((endp hyps1) nil)
    ((endp hyps2) nil)
    ((equal (car hyps1) (car hyps2)) (subsumes-but-for-one-negation (cdr hyps1)
        (cdr hyps2)
        ancestor-lits))
    ((complementaryp (car hyps1) (car hyps2)) (if (subsetp-equal (cdr hyps1) (cdr hyps2))
        (cons (car hyps2) ancestor-lits)
        nil))
    ((member-equal (car hyps2) ancestor-lits) (subsumes-but-for-one-negation hyps1
        (cdr hyps2)
        ancestor-lits))
    (t nil)))

(defun remove-ancestor-literals-from-pairs1
  (pair1 pairs ancestor-lits)
  (cond ((endp pairs) nil)
    (t (let ((pair2 (car pairs)))
        (cond ((equal (cdr pair1) (cdr pair2)) (let ((new-ancestor-lits (subsumes-but-for-one-negation (car pair1)
                   (car pair2)
                   ancestor-lits)))
              (cond (new-ancestor-lits (let ((new-pair2 (cons (set-difference-equal (car pair2) new-ancestor-lits)
                         (cdr pair2))))
                    (cons new-pair2
                      (remove-ancestor-literals-from-pairs1 new-pair2
                        (cdr pairs)
                        new-ancestor-lits))))
                (t (cons pair2
                    (remove-ancestor-literals-from-pairs1 pair2 (cdr pairs) nil))))))
          (t (cons pair2
              (remove-ancestor-literals-from-pairs1 pair2 (cdr pairs) nil))))))))

(defun remove-ancestor-literals-from-pairs
  (pairs)
  (cond ((endp pairs) nil)
    ((endp (cdr pairs)) pairs)
    (t (cons (car pairs)
        (remove-ancestor-literals-from-pairs1 (car pairs)
          (cdr pairs)
          nil)))))

(defun convert-term-to-pairs
  (term ens wrld)
  (mv-let (nterm ttree)
    (normalize term
      t
      nil
      ens
      wrld
      nil
      (backchain-limit wrld :ts))
    (mv (remove-ancestor-literals-from-pairs (convert-normalized-term-to-pairs nil nterm nil))
      (all-runes-in-ttree ttree nil))))

(defun tau-subrs
  (rune fn formals rhs ens wrld)
  (let ((var (car formals)))
    (cond ((tau-like-propositionp var rhs wrld) (let* ((lhs (fcons-term fn formals)) (rhs1 (expand-tau-like-proposition rhs)))
          (mv-let (pairs1 runes1)
            (convert-term-to-pairs (fcons-term* 'if lhs rhs1 *t*)
              ens
              wrld)
            (mv-let (pairs2 runes2)
              (convert-term-to-pairs (fcons-term* 'if rhs1 lhs *t*)
                ens
                wrld)
              (let ((wrld (add-only-simple-and-conjunctive-tau-rules rune
                     pairs1
                     ens
                     (add-only-simple-and-conjunctive-tau-rules rune
                       pairs2
                       ens
                       wrld))))
                (set-tau-runes 'list (union-equal runes1 runes2) wrld))))))
      (t wrld))))

(defun tau-visit-defuns1
  (fns ens wrld wrld0)
  (cond ((endp fns) (mv nil wrld))
    (t (let* ((fn (car fns)) (db (original-def-body fn wrld))
          (formals (access def-body db :formals))
          (rhs (access def-body db :concl))
          (def-eqn (cond ((null db) nil)
              ((or (access def-body db :hyp)
                 (not (eq (access def-body db :equiv) 'equal))) nil)
              (t (fcons-term* 'equal (fcons-term fn formals) rhs))))
          (def-nume (access def-body db :nume))
          (def-rune (access def-body db :rune)))
        (let ((wrld (cond ((or (null def-eqn) (not (enabled-numep def-nume ens))) wrld)
               ((tau-big-switch-equationp def-eqn wrld) (add-tau-big-switch-rule def-rune nil def-eqn wrld))
               ((tau-mv-nth-synonym-formp nil def-eqn) (add-tau-mv-nth-synonym-rule def-rune nil def-eqn wrld))
               (t (tau-subrs def-rune fn formals rhs ens wrld)))))
          (mv-let (msgp wrld)
            (tau-rules-from-type-prescriptions (getpropc fn 'type-prescriptions nil wrld)
              fn
              ens
              wrld
              wrld0)
            (cond (msgp (mv msgp wrld0))
              (t (tau-visit-defuns1 (cdr fns) ens wrld wrld0)))))))))

(defun tau-visit-defuns
  (fns auto-modep ens wrld0)
  (let* ((wrld (discover-tau-preds fns ens wrld0)))
    (if auto-modep
      (tau-visit-defuns1 fns ens wrld wrld0)
      (mv nil wrld))))

(defun tau-visit-defun
  (fn auto-modep ens wrld0)
  (tau-visit-defuns (list fn) auto-modep ens wrld0))

(defun corollaries-and-runes-of-enabled-rules
  (tau-system-onlyp rule-classes
    runic-mapping-pairs
    ens
    theorem)
  (cond ((endp rule-classes) nil)
    (t (let* ((class-name (car (car rule-classes))) (formula (or (cadr (assoc-keyword :corollary (cdr (car rule-classes))))
              theorem))
          (nume (car (car runic-mapping-pairs)))
          (rune (cdr (car runic-mapping-pairs)))
          (rest (corollaries-and-runes-of-enabled-rules tau-system-onlyp
              (cdr rule-classes)
              (cdr runic-mapping-pairs)
              ens
              theorem)))
        (cond ((and (or (not tau-system-onlyp) (eq class-name :tau-system))
             (enabled-numep nume ens)) (cons (cons formula rune) rest))
          (t rest))))))

(defun tau-visit-defthm1
  (first-visitp terms-and-runes ens wrld wrld0)
  (cond ((endp terms-and-runes) (mv nil wrld))
    (t (let ((term (car (car terms-and-runes))) (rune (cdr (car terms-and-runes))))
        (mv-let (msgp wrld)
          (add-tau-rule first-visitp rune term ens wrld)
          (cond (msgp (mv msgp wrld0))
            (t (tau-visit-defthm1 first-visitp
                (cdr terms-and-runes)
                ens
                wrld
                wrld0))))))))

(defun tau-visit-defthm
  (first-visitp name auto-modep ens wrld0)
  (let* ((classes (getpropc name 'classes nil wrld0)) (terms-and-runes (corollaries-and-runes-of-enabled-rules (or (not auto-modep) (assoc-eq :tau-system classes))
          classes
          (getpropc name 'runic-mapping-pairs nil wrld0)
          ens
          (getpropc name 'theorem nil wrld0))))
    (tau-visit-defthm1 first-visitp
      terms-and-runes
      ens
      wrld0
      wrld0)))

(defun tau-visit-event
  (first-visitp ev-type namex auto-modep ens ctx wrld state)
  (mv-let (msgp wrld1)
    (case ev-type
      (defun (tau-visit-defun namex auto-modep ens wrld))
      (defuns (tau-visit-defuns namex auto-modep ens wrld))
      ((defthm defaxiom) (tau-visit-defthm first-visitp namex auto-modep ens wrld))
      (otherwise (mv nil wrld)))
    (cond (msgp (er soft ctx "~@0" msgp)) (t (value wrld1)))))

(defun apply-conjunctive-tau-rule
  (tau1 tau2 ens wrld)
  (mv-let (contradictionp sign recog)
    (tau-near-subsetp tau1 tau2 ens wrld)
    (cond (contradictionp (mv t nil nil))
      (t (mv nil (not sign) recog)))))

(defun apply-conjunctive-tau-rules2
  (conjunctive-rules tau ens wrld changedp)
  (cond ((endp conjunctive-rules) (mv changedp tau))
    (t (mv-let (contradictionp sign recog)
        (apply-conjunctive-tau-rule (car conjunctive-rules)
          tau
          ens
          wrld)
        (cond (contradictionp (mv t *tau-contradiction*))
          ((null recog) (apply-conjunctive-tau-rules2 (cdr conjunctive-rules)
              tau
              ens
              wrld
              changedp))
          (t (let ((new-tau (add-to-tau sign recog tau ens wrld)))
              (cond ((eq new-tau *tau-contradiction*) (mv t *tau-contradiction*))
                (t (apply-conjunctive-tau-rules2 (cdr conjunctive-rules)
                    new-tau
                    ens
                    wrld
                    (or changedp (not (equal tau new-tau)))))))))))))

(defun apply-conjunctive-tau-rules1
  (conjunctive-rules tau ens wrld max-loop)
  (if (and max-loop (equal max-loop 0))
    tau
    (mv-let (changedp tau)
      (apply-conjunctive-tau-rules2 conjunctive-rules
        tau
        ens
        wrld
        nil)
      (cond ((eq tau *tau-contradiction*) *tau-contradiction*)
        (changedp (apply-conjunctive-tau-rules1 conjunctive-rules
            tau
            ens
            wrld
            (if max-loop
              (- max-loop 1)
              nil)))
        (t tau)))))

(defun apply-conjunctive-tau-rules
  (tau ens wrld calist)
  (cond ((eq tau *tau-contradiction*) (mv *tau-contradiction* calist))
    (t (let ((temp (assoc-equal tau calist)))
        (cond (temp (mv (cdr temp) calist))
          (t (let ((val (apply-conjunctive-tau-rules1 (getpropc 'tau-conjunctive-rules 'global-value nil wrld)
                   tau
                   ens
                   wrld
                   nil)))
              (mv val (cons (cons tau val) calist)))))))))

(defun add-to-tau!
  (sign recog tau ens wrld calist)
  (let ((new-tau (if (eq recog :skip)
         tau
         (add-to-tau sign recog tau ens wrld))))
    (cond ((and (not (eq recog :skip)) (equal tau new-tau)) (mv tau calist))
      (t (apply-conjunctive-tau-rules new-tau ens wrld calist)))))

(defun all-tau-emptyp
  (lst)
  (cond ((endp lst) t)
    (t (and (equal (car lst) *tau-empty*)
        (all-tau-emptyp (cdr lst))))))

(defun all-unrestricted-signature-rulesp
  (sigrules)
  (cond ((endp sigrules) t)
    ((and (null (access signature-rule (car sigrules) :dependent-hyps))
       (all-tau-emptyp (access signature-rule (car sigrules) :input-tau-list))) (all-unrestricted-signature-rulesp (cdr sigrules)))
    (t nil)))

(defun disjoin-intervals
  (interval1 interval2)
  (let* ((dom1 (access tau-interval interval1 :domain)) (dom2 (access tau-interval interval2 :domain))
      (dom (cond ((eq dom1 dom2) dom1)
          ((eq dom1 'integerp) dom2)
          ((eq dom2 'integerp) dom1)
          ((eq dom1 'rationalp) dom2)
          ((eq dom2 'rationalp) dom1)
          ((eq dom1 'acl2-numberp) dom2)
          (t dom1)))
      (lo-rel1 (access tau-interval interval1 :lo-rel))
      (lo-rel2 (access tau-interval interval2 :lo-rel))
      (lo1 (access tau-interval interval1 :lo))
      (lo2 (access tau-interval interval2 :lo))
      (hi-rel1 (access tau-interval interval1 :hi-rel))
      (hi-rel2 (access tau-interval interval2 :hi-rel))
      (hi1 (access tau-interval interval1 :hi))
      (hi2 (access tau-interval interval2 :hi)))
    (mv-let (lo-rel lo)
      (if (lower-bound-> lo-rel1 lo1 lo-rel2 lo2)
        (mv lo-rel2 lo2)
        (mv lo-rel1 lo1))
      (mv-let (hi-rel hi)
        (if (upper-bound-< hi-rel1 hi1 hi-rel2 hi2)
          (mv hi-rel2 hi2)
          (mv hi-rel1 hi1))
        (if (and (null dom) (null lo) (null hi))
          nil
          (make tau-interval
            :domain dom
            :lo-rel lo-rel
            :lo lo
            :hi-rel hi-rel
            :hi hi))))))

(defun conjoin-intervals
  (interval1 interval2)
  (let* ((dom1 (access tau-interval interval1 :domain)) (dom2 (access tau-interval interval2 :domain))
      (dom (cond ((eq dom1 dom2) dom1)
          ((eq dom1 'integerp) dom1)
          ((eq dom2 'integerp) dom2)
          ((eq dom1 'rationalp) dom1)
          ((eq dom2 'rationalp) dom2)
          ((eq dom1 'acl2-numberp) dom1)
          (t dom2)))
      (lo-rel1 (access tau-interval interval1 :lo-rel))
      (lo-rel2 (access tau-interval interval2 :lo-rel))
      (lo1 (access tau-interval interval1 :lo))
      (lo2 (access tau-interval interval2 :lo))
      (hi-rel1 (access tau-interval interval1 :hi-rel))
      (hi-rel2 (access tau-interval interval2 :hi-rel))
      (hi1 (access tau-interval interval1 :hi))
      (hi2 (access tau-interval interval2 :hi)))
    (mv-let (lo-rel1 lo1 hi-rel1 hi1)
      (if (and (eq dom 'integerp) (not (eq dom1 'integerp)))
        (mv nil
          (squeeze-k nil lo-rel1 lo1)
          nil
          (squeeze-k t hi-rel1 hi1))
        (mv lo-rel1 lo1 hi-rel1 hi1))
      (mv-let (lo-rel2 lo2 hi-rel2 hi2)
        (if (and (eq dom 'integerp) (not (eq dom2 'integerp)))
          (mv nil
            (squeeze-k nil lo-rel2 lo2)
            nil
            (squeeze-k t hi-rel2 hi2))
          (mv lo-rel2 lo2 hi-rel2 hi2))
        (mv-let (lo-rel lo)
          (if (lower-bound-> lo-rel1 lo1 lo-rel2 lo2)
            (mv lo-rel1 lo1)
            (mv lo-rel2 lo2))
          (mv-let (hi-rel hi)
            (if (upper-bound-< hi-rel1 hi1 hi-rel2 hi2)
              (mv hi-rel1 hi1)
              (mv hi-rel2 hi2))
            (cond ((and (null dom) (null lo) (null hi)) nil)
              ((and lo
                 hi
                 (if (or lo-rel hi-rel)
                   (>= lo hi)
                   (> lo hi))) *tau-empty-interval*)
              (t (make tau-interval
                  :domain dom
                  :lo-rel lo-rel
                  :lo lo
                  :hi-rel hi-rel
                  :hi hi)))))))))

(defun combine-pos/neg-pairs-from-tau1
  (sign pos-evg1 pairs1 pos-evg2 pairs2 ens wrld)
  (cond ((endp pairs1) (cond ((endp pairs2) nil)
        ((and pos-evg1
           (eq (ev-fncall-w-tau-recog (cdr (car pairs2)) pos-evg1 ens wrld)
             sign)) (cons (car pairs2)
            (combine-pos/neg-pairs-from-tau1 sign
              pos-evg1
              nil
              pos-evg2
              (cdr pairs2)
              ens
              wrld)))
        (t (combine-pos/neg-pairs-from-tau1 sign
            pos-evg1
            nil
            pos-evg2
            (cdr pairs2)
            ens
            wrld))))
    ((endp pairs2) (cond ((and pos-evg2
           (eq (ev-fncall-w-tau-recog (cdr (car pairs1)) pos-evg2 ens wrld)
             sign)) (cons (car pairs1)
            (combine-pos/neg-pairs-from-tau1 sign
              pos-evg1
              (cdr pairs1)
              pos-evg2
              nil
              ens
              wrld)))
        (t (combine-pos/neg-pairs-from-tau1 sign
            pos-evg1
            (cdr pairs1)
            pos-evg2
            nil
            ens
            wrld))))
    ((equal (car pairs1) (car pairs2)) (cons (car pairs1)
        (combine-pos/neg-pairs-from-tau1 sign
          pos-evg1
          (cdr pairs1)
          pos-evg2
          (cdr pairs2)
          ens
          wrld)))
    ((and pos-evg1
       (eq (ev-fncall-w-tau-recog (cdr (car pairs2)) pos-evg1 ens wrld)
         sign)) (cons (car pairs2)
        (combine-pos/neg-pairs-from-tau1 sign
          pos-evg1
          pairs1
          pos-evg2
          (cdr pairs2)
          ens
          wrld)))
    ((and pos-evg2
       (eq (ev-fncall-w-tau-recog (cdr (car pairs1)) pos-evg2 ens wrld)
         sign)) (cons (car pairs1)
        (combine-pos/neg-pairs-from-tau1 sign
          pos-evg1
          (cdr pairs1)
          pos-evg2
          pairs2
          ens
          wrld)))
    ((> (car (car pairs1)) (car (car pairs2))) (combine-pos/neg-pairs-from-tau1 sign
        pos-evg1
        (cdr pairs1)
        pos-evg2
        pairs2
        ens
        wrld))
    (t (combine-pos/neg-pairs-from-tau1 sign
        pos-evg1
        pairs1
        pos-evg2
        (cdr pairs2)
        ens
        wrld))))

(defun augment-pos/neg-pairs-with-implicit-numeric-recogs
  (pos-evg sign pairs wrld)
  (if pos-evg
    (let* ((pred (if (acl2-numberp (car pos-evg))
           (cond ((integerp (car pos-evg)) 'integerp)
             ((rationalp (car pos-evg)) 'rationalp)
             (t 'acl2-numberp))
           nil)) (implicit-pairs (if pred
            (if sign
              (access tau (tau-simple-implicants t pred wrld) :pos-pairs)
              (access tau (tau-simple-implicants t pred wrld) :neg-pairs))
            nil)))
      (merge-car-> pairs implicit-pairs))
    pairs))

(defun combine-pos/neg-pairs-from-tau
  (sign tau1 tau2 ens wrld)
  (let* ((pos-evg1 (access tau tau1 :pos-evg)) (pos-evg2 (access tau tau2 :pos-evg))
      (pairs1 (augment-pos/neg-pairs-with-implicit-numeric-recogs pos-evg1
          sign
          (if sign
            (access tau tau1 :pos-pairs)
            (access tau tau1 :neg-pairs))
          wrld))
      (pairs2 (augment-pos/neg-pairs-with-implicit-numeric-recogs pos-evg2
          sign
          (if sign
            (access tau tau2 :pos-pairs)
            (access tau tau2 :neg-pairs))
          wrld)))
    (combine-pos/neg-pairs-from-tau1 sign
      pos-evg1
      pairs1
      pos-evg2
      pairs2
      ens
      wrld)))

(defun combine-tau
  (tau1 tau2 ens wrld)
  (cond ((eq tau1 *tau-contradiction*) tau2)
    ((eq tau2 *tau-contradiction*) tau1)
    (t (let ((pos-evg (if (equal (access tau tau1 :pos-evg)
               (access tau tau2 :pos-evg))
             (access tau tau1 :pos-evg)
             nil)) (neg-evgs (intersection-equal (access tau tau1 :neg-evgs)
              (access tau tau2 :neg-evgs)))
          (pos-pairs (combine-pos/neg-pairs-from-tau t tau1 tau2 ens wrld))
          (neg-pairs (combine-pos/neg-pairs-from-tau nil tau1 tau2 ens wrld))
          (interval (disjoin-intervals (access tau tau1 :interval)
              (access tau tau2 :interval))))
        (let ((dom (access tau-interval interval :domain)) (lo-rel (access tau-interval interval :lo-rel))
            (lo (access tau-interval interval :lo))
            (hi-rel (access tau-interval interval :hi-rel))
            (hi (access tau-interval interval :hi)))
          (cond ((and (not (singleton-tau-intervalp lo-rel lo hi-rel hi))
               dom
               (not (tau-pair-member (case dom
                     (integerp *tau-integerp-pair*)
                     (rationalp *tau-rationalp-pair*)
                     (otherwise *tau-acl2-numberp-pair*))
                   pos-pairs))) (er hard
                'combine-tau
                "We have just constructed an interval, ~x0, whose domain is not ~
               in the :pos-pairs of the tau we planned to put it into!  The ~
               offending interval was constructed by disjoin-intervals from ~
               the intervals in these two tau ~x1 and ~x2."
                interval
                tau1
                tau2))
            ((or pos-evg neg-evgs pos-pairs neg-pairs interval) (make tau
                :pos-evg pos-evg
                :neg-evgs neg-evgs
                :pos-pairs pos-pairs
                :neg-pairs neg-pairs
                :interval interval))
            (t *tau-empty*)))))))

(defun push-mv-nth-down
  (i term)
  (cond ((variablep term) (fcons-term* 'mv-nth i term))
    ((fquotep term) (kwote (mv-nth (cadr i) (cadr term))))
    ((eq (ffn-symb term) 'if) (fcons-term* 'if
        (fargn term 1)
        (push-mv-nth-down i (fargn term 2))
        (push-mv-nth-down i (fargn term 3))))
    (t (fcons-term* 'mv-nth i term))))

(defun tau-expand-big-switch
  (body switch-var switch-tau var-alist ens wrld)
  (cond ((not (ffn-symb-p body 'if)) (cond ((occur switch-var body) (mv nil nil))
        (t (mv t (sublis-var var-alist body)))))
    (t (mv-let (sign recog e criterion)
        (tau-like-term (fargn body 1) :various-any wrld)
        (declare (ignore criterion))
        (cond ((and recog (eq e switch-var)) (let ((temp (reduce-sign/recog switch-tau sign recog ens wrld)))
              (cond ((eq temp t) (tau-expand-big-switch (fargn body 2)
                    switch-var
                    switch-tau
                    var-alist
                    ens
                    wrld))
                ((eq temp nil) (tau-expand-big-switch (fargn body 3)
                    switch-var
                    switch-tau
                    var-alist
                    ens
                    wrld))
                (t (mv nil nil)))))
          (t (mv nil nil)))))))

(defun deconstruct-conjunction
  (sign a b c)
  (if sign
    (if (equal c *nil*)
      (mv t t a t b)
      (if (equal b *nil*)
        (mv t nil a t c)
        (mv nil nil nil nil nil)))
    (if (or (equal a b) (equal b *t*))
      (mv t nil a nil c)
      (if (equal c *t*)
        (mv t t a nil b)
        (mv nil nil nil nil nil)))))

(defun ok-to-fire-signature-rulep1
  (formal-tau-lst actual-tau-lst ens wrld)
  (cond ((endp formal-tau-lst) t)
    ((tau-implies (car actual-tau-lst)
       (car formal-tau-lst)
       ens
       wrld) (ok-to-fire-signature-rulep1 (cdr formal-tau-lst)
        (cdr actual-tau-lst)
        ens
        wrld))
    (t nil)))

(defun smart-member-equal-+-
  (lit clause)
  (cond ((null clause) nil)
    ((equal lit (car clause)) '+)
    ((let ((lit1 lit) (lit2 (car clause)))
       (or (and (ffn-symb-p lit1 'not) (equal (fargn lit1 1) lit2))
         (and (ffn-symb-p lit2 'not) (equal (fargn lit2 1) lit1)))) '-)
    (t (smart-member-equal-+- lit (cdr clause)))))

(defun find-first-acceptable-domain
  (actual-dom acceptable-domains)
  (cond ((endp acceptable-domains) (mv nil nil))
    ((eq actual-dom (car acceptable-domains)) (mv t actual-dom))
    (t (let* ((more-specific-acceptable-domains (cdr (assoc-eq (car acceptable-domains)
               '((rationalp integerp) (acl2-numberp rationalp integerp)
                 (nil acl2-numberp rationalp integerp))))) (winner (member-eq actual-dom more-specific-acceptable-domains)))
        (cond (winner (mv t (car acceptable-domains)))
          (t (find-first-acceptable-domain actual-dom
              (cdr acceptable-domains))))))))

(defun tau-lst-with-acceptable-domainsp
  (actual-tau-lst doms-lst)
  (cond ((endp doms-lst) t)
    ((eq (car doms-lst) t) (tau-lst-with-acceptable-domainsp (cdr actual-tau-lst)
        (cdr doms-lst)))
    (t (mv-let (flg dom)
        (find-first-acceptable-domain (access tau-interval
            (access tau (car actual-tau-lst) :interval)
            :domain)
          (car doms-lst))
        (declare (ignore dom))
        (and flg
          (tau-lst-with-acceptable-domainsp (cdr actual-tau-lst)
            (cdr doms-lst)))))))

(defun collect-bounder-args
  (actual-tau-lst doms-lst bounder-args)
  (cond ((endp bounder-args) nil)
    (t (let ((actual-int (access tau
             (nth (car bounder-args) actual-tau-lst)
             :interval)) (acceptable-doms (nth (car bounder-args) doms-lst)))
        (mv-let (flg dom)
          (find-first-acceptable-domain (access tau-interval actual-int :domain)
            acceptable-doms)
          (declare (ignore flg))
          (cons (change tau-interval actual-int :domain dom)
            (collect-bounder-args actual-tau-lst
              doms-lst
              (cdr bounder-args))))))))

(defun bounding-interval
  (bc actual-tau-lst wrld)
  (let ((doms-lst (access bounder-correctness bc :acceptable-domains)))
    (cond ((tau-lst-with-acceptable-domainsp actual-tau-lst doms-lst) (let ((bounder-fn (access bounder-correctness bc :bounder-fn)) (bounder-args (collect-bounder-args actual-tau-lst
                doms-lst
                (access bounder-correctness bc :bounder-args))))
          (mv-let (erp val)
            (ev-fncall-w bounder-fn bounder-args wrld nil nil t t nil)
            (cond (erp nil) (t val)))))
      (t nil))))

(defun conjoin-bounding-intervals
  (bounders actual-tau-lst wrld)
  (cond ((endp bounders) nil)
    (t (conjoin-intervals (bounding-interval (car bounders) actual-tau-lst wrld)
        (conjoin-bounding-intervals (cdr bounders)
          actual-tau-lst
          wrld)))))

(defun apply-tau-bounders
  (bounders actual-tau-lst ens wrld calist)
  (let ((int (conjoin-bounding-intervals bounders actual-tau-lst wrld)))
    (cond ((null int) (mv *tau-empty* calist))
      ((tau-empty-intervalp int) (mv *tau-contradiction* calist))
      (t (let ((dom (access tau-interval int :domain)) (lo-rel (access tau-interval int :lo-rel))
            (lo (access tau-interval int :lo))
            (hi-rel (access tau-interval int :hi-rel))
            (hi (access tau-interval int :hi)))
          (cond ((and (null dom) (null lo) (null hi)) (mv *tau-empty* calist))
            (t (let* ((dom-pair (case dom
                     (integerp *tau-integerp-pair*)
                     (rationalp *tau-rationalp-pair*)
                     (acl2-numberp *tau-acl2-numberp-pair*)
                     (otherwise nil))) (tau1 (if (null dom-pair)
                      *tau-empty*
                      (add-to-tau t dom-pair *tau-empty* ens wrld))))
                (mv-let (sign k token)
                  (tau-interval-endpoint-to-sign-k-token nil lo-rel lo)
                  (let ((tau2 (if (null k)
                         tau1
                         (add-to-tau sign (cons k token) tau1 ens wrld))))
                    (mv-let (sign k token)
                      (tau-interval-endpoint-to-sign-k-token t hi-rel hi)
                      (add-to-tau! sign
                        (if (null k)
                          :skip (cons k token))
                        tau2
                        ens
                        wrld
                        calist))))))))))))

(defun tau-interval-equal-decider
  (int1 int2)
  (cond ((and (identity-intervalp int1)
       (identity-intervalp int2)
       (equal (access tau-interval int1 :lo)
         (access tau-interval int2 :lo))) t)
    ((equal (conjoin-intervals int1 int2) *tau-empty-interval*) nil)
    (t '?)))

(defun tau-interval-<-decider
  (int1 int2)
  (let ((lo-rel1 (access tau-interval int1 :lo-rel)) (lo1 (access tau-interval int1 :lo))
      (hi-rel1 (access tau-interval int1 :hi-rel))
      (hi1 (access tau-interval int1 :hi))
      (lo-rel2 (access tau-interval int2 :lo-rel))
      (lo2 (access tau-interval int2 :lo))
      (hi-rel2 (access tau-interval int2 :hi-rel))
      (hi2 (access tau-interval int2 :hi)))
    (cond ((and hi1 lo2 (<? (not (or hi-rel1 lo-rel2)) hi1 lo2)) t)
      ((and hi2 lo1 (<? (not (or hi-rel2 lo-rel1)) hi2 lo1)) nil)
      (t '?))))

(defun annotate-clause-with-key-numbers
  (clause max i wrld)
  (cond ((endp clause) nil)
    (t (let ((lit (car clause)))
        (mv-let (rsign recog e criterion)
          (tau-like-term lit :various-any wrld)
          (declare (ignore rsign criterion))
          (cons (list (if (and recog (variablep e))
                (if (cdr recog)
                  (+ i (* 2 max))
                  i)
                (+ i (* 3 max)))
              i
              lit)
            (annotate-clause-with-key-numbers (cdr clause)
              max
              (+ 1 i)
              wrld)))))))

(defun tau-clause1p
  (triples tau-alist type-alist pot-lst ens wrld calist)
  (cond ((endp triples) (mv nil calist))
    (t (mv-let (contradictionp mbt mbf tau-alist calist)
        (tau-assume nil
          (caddr (car triples))
          tau-alist
          type-alist
          pot-lst
          ens
          wrld
          calist)
        (declare (ignore mbt))
        (cond (contradictionp (mv t calist))
          (mbf (mv t calist))
          (t (tau-clause1p (cdr triples)
              tau-alist
              type-alist
              pot-lst
              ens
              wrld
              calist)))))))

(defun tau-get-all-preds
  (wrld ans)
  (cond ((endp wrld) ans)
    ((eq (cadr (car wrld)) 'tau-pair) (tau-get-all-preds (cdr wrld)
        (add-to-set-eq (car (car wrld)) ans)))
    (t (tau-get-all-preds (cdr wrld) ans))))

(defun tau-get-stats-new-max-block
  (pred prop val-len block)
  (case-match block
    (((':max max-pred max-prop max-len) (':next & & next-len)) (cond ((> val-len max-len) `((:max ,PRED ,PROP ,VAL-LEN) (:next ,MAX-PRED ,MAX-PROP ,MAX-LEN)))
        ((> val-len next-len) `((:max ,MAX-PRED ,MAX-PROP ,MAX-LEN) (:next ,PRED ,PROP ,VAL-LEN)))
        (t block)))
    (& block)))

(defun tau-size
  (tau)
  (+ (if (access tau tau :pos-evg)
      1
      0)
    (length (access tau tau :neg-evgs))
    (length (access tau tau :pos-pairs))
    (length (access tau tau :neg-pairs))))

(defun tau-get-stats-on-implicant-sizes
  (preds wrld ans max-block)
  (cond ((endp preds) (list (merge-sort-lexorder ans) max-block))
    (t (let ((pos-size (tau-size (getpropc (car preds) 'pos-implicants nil wrld))) (neg-size (tau-size (getpropc (car preds) 'neg-implicants nil wrld))))
        (tau-get-stats-on-implicant-sizes (cdr preds)
          wrld
          (cons pos-size (cons neg-size ans))
          (tau-get-stats-new-max-block (car preds)
            'neg-implicants
            neg-size
            (tau-get-stats-new-max-block (car preds)
              'pos-implicants
              pos-size
              max-block)))))))

(defun decode-recog
  (sign recog e)
  (let* ((discriminator (cdr recog)) (atm (cond ((null discriminator) `(equal ,E ',@RECOG))
          ((eq discriminator :lessp-k-x) `(< ',(CAR DISCRIMINATOR) ,E))
          ((eq discriminator :lessp-x-k) `(< ,E ',(CAR DISCRIMINATOR)))
          (t `(,DISCRIMINATOR ,E)))))
    (if sign
      atm
      `(not ,ATM))))

(defun decode-recog-lst
  (sign lst e)
  (cond ((endp lst) nil)
    (t (cons (decode-recog sign (car lst) e)
        (decode-recog-lst sign (cdr lst) e)))))

(defun decode-tau1
  (tau e)
  (append (decode-recog-lst t
      (if (access tau tau :pos-evg)
        (list (access tau tau :pos-evg))
        nil)
      e)
    (decode-recog-lst t
      (revappend (access tau tau :pos-pairs) nil)
      e)
    (decode-tau-interval (access tau tau :interval) e t)
    (decode-recog-lst nil (access tau tau :neg-evgs) e)
    (decode-recog-lst nil
      (revappend (access tau tau :neg-pairs) nil)
      e)))

(defun decode-tau
  (tau e)
  (cond ((eq tau *tau-contradiction*) nil)
    (t (let ((terms (decode-tau1 tau e)))
        (cond ((endp terms) t)
          ((endp (cdr terms)) (car terms))
          (t `(and ,@TERMS)))))))

(defun decode-tau-conjunctive-rule
  (tau)
  (cond ((eq tau *tau-contradiction*) nil)
    (t (let* ((terms (decode-tau1 tau 'v)))
        (cond ((null (cdr terms)) (dumb-negate-lit (car terms)))
          (t (let ((concl (dumb-negate-lit (car (last terms)))) (hyps (all-but-last terms)))
              (cond ((null hyps) (dumb-negate-lit concl))
                ((null (cdr hyps)) `(implies ,(CAR HYPS) ,CONCL))
                (t `(implies (and ,@HYPS) ,CONCL))))))))))

(defun decode-tau-conjunctive-rules
  (lst)
  (cond ((endp lst) nil)
    (t (cons (decode-tau-conjunctive-rule (car lst))
        (decode-tau-conjunctive-rules (cdr lst))))))

(defun decode-tau-lst
  (lst e-lst)
  (cond ((endp lst) nil)
    (t (let ((hyp (decode-tau (car lst) (car e-lst))))
        (cond ((eq hyp t) (decode-tau-lst (cdr lst) (cdr e-lst)))
          (t (cons hyp (decode-tau-lst (cdr lst) (cdr e-lst)))))))))

(defun decode-tau-alist
  (alist seen)
  (cond ((endp alist) nil)
    ((member-equal (car (car alist)) seen) (decode-tau-alist (cdr alist) seen))
    (t (cons (decode-tau (cdr (car alist)) (car (car alist)))
        (decode-tau-alist (cdr alist) (cons (car (car alist)) seen))))))

(defun decode-tau-signature-rule
  (flg fn sr wrld)
  (cond ((and (symbolp fn) (arity fn wrld)) (let* ((vars (access signature-rule sr :vars)) (input-tau-list (access signature-rule sr :input-tau-list))
          (dependent-hyps (access signature-rule sr :dependent-hyps))
          (output-recog (access signature-rule sr :output-recog))
          (output-sign (access signature-rule sr :output-sign))
          (discriminator (cdr output-recog))
          (eterm (if (null flg)
              `(,FN ,@VARS)
              `(mv-nth ,FLG (,FN ,@VARS))))
          (hyps (append (decode-tau-lst input-tau-list vars) dependent-hyps))
          (concl-atm (cond ((null discriminator) `(equal ,ETERM
                  ,(KWOTE (CAR (ACCESS SIGNATURE-RULE SR :OUTPUT-RECOG)))))
              ((eq discriminator :lessp-k-x) `(< ,(KWOTE (CAR OUTPUT-RECOG)) ,ETERM))
              ((eq discriminator :lessp-x-k) `(< ,ETERM ,(KWOTE (CAR OUTPUT-RECOG))))
              (t `(,DISCRIMINATOR ,ETERM))))
          (concl (if output-sign
              concl-atm
              (fcons-term* 'not concl-atm))))
        (reprettyify hyps concl wrld)))
    (t nil)))

(defun decode-tau-signature-rules1
  (flg fn sr-lst wrld)
  (cond ((endp sr-lst) nil)
    (t (cons (decode-tau-signature-rule flg fn (car sr-lst) wrld)
        (decode-tau-signature-rules1 flg fn (cdr sr-lst) wrld)))))

(defun decode-tau-signature-rules2
  (i fn mv-lst wrld)
  (cond ((endp mv-lst) nil)
    (t (append (decode-tau-signature-rules1 i fn (car mv-lst) wrld)
        (decode-tau-signature-rules2 (+ 1 i) fn (cdr mv-lst) wrld)))))

(defun decode-tau-signature-rules
  (flg fn sr-lst wrld)
  (let ((temp (cond ((null flg) (decode-tau-signature-rules1 nil fn sr-lst wrld))
         (t (decode-tau-signature-rules2 0 fn sr-lst wrld)))))
    (cond ((null temp) t)
      ((null (cdr temp)) (car temp))
      (t `(and ,@TEMP)))))

(defun tau-get-all-sig-fns
  (wrld fns-seen)
  (cond ((endp wrld) fns-seen)
    ((and (or (eq (cadr (car wrld)) 'signature-rules-form-1)
         (eq (cadr (car wrld)) 'signature-rules-form-2))
       (not (member-eq (car (car wrld)) fns-seen))) (tau-get-all-sig-fns (cdr wrld)
        (cons (car (car wrld)) fns-seen)))
    (t (tau-get-all-sig-fns (cdr wrld) fns-seen))))

(defun some-slot-has-multiple-tau-sigs
  (slots)
  (cond ((endp slots) nil)
    ((> (length (car slots)) 1) t)
    (t (some-slot-has-multiple-tau-sigs (cdr slots)))))

(defun count-tau-sigs-by-slot
  (slots)
  (cond ((endp slots) nil)
    (t (cons (length (car slots))
        (count-tau-sigs-by-slot (cdr slots))))))

(defun collect-rules-with-dependent-hyps
  (fn i rules wrld ans)
  (cond ((endp rules) ans)
    (t (collect-rules-with-dependent-hyps fn
        i
        (cdr rules)
        wrld
        (if (access signature-rule (car rules) :dependent-hyps)
          (cons (decode-tau-signature-rule i fn (car rules) wrld) ans)
          ans)))))

(defun collect-rules-with-dependent-hyps-across-mv
  (fn i mv-lst wrld ans)
  (cond ((endp mv-lst) ans)
    (t (collect-rules-with-dependent-hyps-across-mv fn
        (+ i 1)
        (cdr mv-lst)
        wrld
        (collect-rules-with-dependent-hyps fn
          i
          (car mv-lst)
          wrld
          ans)))))

(defun tau-get-stats-on-signatures1
  (fn wrld
    fn-cnt-1
    fn-cnt-2
    fn-cnt-1-and-2
    multi-sig-cnt-1
    multi-sig-cnt-2
    multi-sig-cnt-alist
    rules-with-dependent-hyps)
  (let ((sigs1 (getpropc fn 'signature-rules-form-1 nil wrld)) (sigs2 (getpropc fn 'signature-rules-form-2 nil wrld)))
    (mv-let (fn-cnt-1 fn-cnt-2 fn-cnt-1-and-2)
      (cond ((and sigs1 sigs2) (mv fn-cnt-1 fn-cnt-2 (+ 1 fn-cnt-1-and-2)))
        (sigs1 (mv (+ 1 fn-cnt-1) fn-cnt-2 fn-cnt-1-and-2))
        (t (mv fn-cnt-1 (+ 1 fn-cnt-2) fn-cnt-1-and-2)))
      (let* ((multi-sig-cnt-1 (if (> (length sigs1) 1)
             (+ 1 multi-sig-cnt-1)
             multi-sig-cnt-1)) (multi-sig-cnt-2 (if (some-slot-has-multiple-tau-sigs sigs2)
              (+ 1 multi-sig-cnt-2)
              multi-sig-cnt-2))
          (multi-sig-cnt-alist (cond ((or (> (length sigs1) 1)
                 (some-slot-has-multiple-tau-sigs sigs2)) (cons `(,FN ,(LENGTH SIGS1) (mv ,@(COUNT-TAU-SIGS-BY-SLOT SIGS2)))
                  multi-sig-cnt-alist))
              (t multi-sig-cnt-alist)))
          (rules-with-dependent-hyps (collect-rules-with-dependent-hyps-across-mv fn
              0
              sigs2
              wrld
              (collect-rules-with-dependent-hyps fn
                nil
                sigs1
                wrld
                rules-with-dependent-hyps))))
        (mv fn-cnt-1
          fn-cnt-2
          fn-cnt-1-and-2
          multi-sig-cnt-1
          multi-sig-cnt-2
          multi-sig-cnt-alist
          rules-with-dependent-hyps)))))

(defun tau-get-stats-on-signatures
  (fns wrld
    fn-cnt-1
    fn-cnt-2
    fn-cnt-1-and-2
    multi-sig-cnt-1
    multi-sig-cnt-2
    multi-sig-cnt-alist
    rules-with-dependent-hyps)
  (cond ((endp fns) `((:fns-with-signatures (:form-1-only ,FN-CNT-1)
         (:form-2-only ,FN-CNT-2)
         (:both-forms ,FN-CNT-1-AND-2)) (:fns-with-multiple-sigs (:form-1 ,MULTI-SIG-CNT-1)
          (:form-2 ,MULTI-SIG-CNT-2))
        (:fn-with-multiple-sigs-details (fn form-1-cnt (mv slot-1-cnt dot-dot-dot slot-k-cnt))
          ,@MULTI-SIG-CNT-ALIST)
        (:rules-with-dependent-hyps ,(LENGTH RULES-WITH-DEPENDENT-HYPS)
          ,(REVAPPEND RULES-WITH-DEPENDENT-HYPS NIL))))
    (t (mv-let (fn-cnt-1 fn-cnt-2
          fn-cnt-1-and-2
          multi-sig-cnt-1
          multi-sig-cnt-2
          multi-sig-cnt-alist
          rules-with-dependent-hyps)
        (tau-get-stats-on-signatures1 (car fns)
          wrld
          fn-cnt-1
          fn-cnt-2
          fn-cnt-1-and-2
          multi-sig-cnt-1
          multi-sig-cnt-2
          multi-sig-cnt-alist
          rules-with-dependent-hyps)
        (tau-get-stats-on-signatures (cdr fns)
          wrld
          fn-cnt-1
          fn-cnt-2
          fn-cnt-1-and-2
          multi-sig-cnt-1
          multi-sig-cnt-2
          multi-sig-cnt-alist
          rules-with-dependent-hyps)))))

(defun collect-tau-big-switches
  (wrld ans)
  (cond ((endp wrld) ans)
    ((eq (cadr (car wrld)) 'big-switch) (collect-tau-big-switches (cdr wrld)
        (add-to-set-eq (car (car wrld)) ans)))
    (t (collect-tau-big-switches (cdr wrld) ans))))

(defun tau-sum-lst
  (x)
  (cond ((endp x) 0) (t (+ (car x) (tau-sum-lst (cdr x))))))

(defun tau-get-stats
  (wrld)
  (let* ((preds (tau-get-all-preds wrld nil)) (fns (tau-get-all-sig-fns wrld nil))
      (implicant-sizes (tau-get-stats-on-implicant-sizes preds
          wrld
          nil
          `((:max nil nil 0) (:next nil nil 0))))
      (implicants (car implicant-sizes))
      (sum-size (tau-sum-lst implicants)))
    `((:preds ,(LENGTH PREDS)) (:implicant-sizes ,IMPLICANT-SIZES)
      (:average-implicant-size ,(FLOOR SUM-SIZE (LENGTH IMPLICANTS))
        --
        ,(CEILING SUM-SIZE (LENGTH IMPLICANTS)))
      (:median-implicant-size ,(IF (EVENP (LENGTH IMPLICANTS))
     `(,(NTH (- (FLOOR (LENGTH IMPLICANTS) 2) 1) IMPLICANTS) --
       ,(NTH (FLOOR (LENGTH IMPLICANTS) 2) IMPLICANTS))
     (NTH (FLOOR (LENGTH IMPLICANTS) 2) IMPLICANTS)))
      (:conjunctive-rules ,(LENGTH (GETPROPC 'TAU-CONJUNCTIVE-RULES 'GLOBAL-VALUE NIL WRLD)))
      ,@(TAU-GET-STATS-ON-SIGNATURES FNS WRLD 0 0 0 0 0 NIL NIL)
      (:big-switches ,(COLLECT-TAU-BIG-SWITCHES WRLD NIL))
      (:mv-nth-synonyms ,(GLOBAL-VAL 'TAU-MV-NTH-SYNONYMS WRLD))
      (:tau-runes ,(LEN (GET-TAU-RUNES WRLD)))
      (:tau-lost-runes ,(LEN (GLOBAL-VAL 'TAU-LOST-RUNES WRLD))))))

(defun tau-data-fn
  (fn wrld)
  (let ((fn (deref-macro-name fn (macro-aliases wrld))))
    (cond ((and (symbolp fn) (arity fn wrld)) (let ((tau-pair (getpropc fn 'tau-pair nil wrld)) (sigs1 (getpropc fn 'signature-rules-form-1 nil wrld))
            (sigs2 (getpropc fn 'signature-rules-form-2 nil wrld))
            (big-switch (getpropc fn 'big-switch nil wrld))
            (mv-nth-synonym (member-eq fn (global-val 'tau-mv-nth-synonyms wrld))))
          (cond ((or tau-pair sigs1 sigs2 big-switch mv-nth-synonym) `(,FN (recognizer-index ,(CAR TAU-PAIR))
                (pos-implicants ,(DECODE-TAU (GETPROPC FN 'POS-IMPLICANTS *TAU-EMPTY* WRLD) 'V))
                (neg-implicants ,(DECODE-TAU (GETPROPC FN 'NEG-IMPLICANTS *TAU-EMPTY* WRLD) 'V))
                (signatures ,(LET ((SIGS1 (DECODE-TAU-SIGNATURE-RULES NIL FN SIGS1 WRLD))
       (SIGS2 (DECODE-TAU-SIGNATURE-RULES T FN SIGS2 WRLD)))
   (IF (EQ SIGS1 T)
       (IF (EQ SIGS2 T)
           T
           SIGS2)
       (IF (EQ SIGS2 T)
           SIGS1
           `(AND ,SIGS1 ,SIGS2)))))
                (big-switch? ,(IF BIG-SWITCH
     :YES
     :NO))
                (mv-nth-synonym? ,(IF MV-NTH-SYNONYM
     :YES
     :NO))))
            (t nil))))
      (t nil))))

(defun all-fnnames-world1
  (trips logicp wrld ans)
  (cond ((endp trips) ans)
    ((and (eq (cadr (car trips)) 'formals)
       (if (eq logicp t)
         (not (eq (symbol-class (car (car trips)) wrld) :program))
         (if logicp
           t
           (eq (symbol-class (car (car trips)) wrld) :program)))
       (not (member-eq (car (car trips)) ans))) (all-fnnames-world1 (cdr trips)
        logicp
        wrld
        (cons (car (car trips)) ans)))
    (t (all-fnnames-world1 (cdr trips) logicp wrld ans))))

(defun all-fnnames-world
  (mode wrld)
  (all-fnnames-world1 wrld
    (if (eq mode :logic)
      t
      (if (eq mode :program)
        nil
        :either))
    wrld
    nil))

(defun tau-data-fns
  (fns wrld ans)
  (cond ((endp fns) ans)
    (t (tau-data-fns (cdr fns)
        wrld
        (let ((temp (tau-data-fn (car fns) wrld)))
          (if temp
            (cons temp ans)
            ans))))))

(defun tau-database
  (wrld)
  (tau-data-fns (merge-sort-lexorder (all-fnnames-world :logic wrld))
    wrld
    `((tau-next-index ,(GLOBAL-VAL 'TAU-NEXT-INDEX WRLD)) (tau-conjunctive-rules ,(DECODE-TAU-CONJUNCTIVE-RULES
  (MERGE-SORT-LEXORDER (GLOBAL-VAL 'TAU-CONJUNCTIVE-RULES WRLD))))
      (tau-mv-nth-synonyms ,(MERGE-SORT-LEXORDER (GLOBAL-VAL 'TAU-MV-NTH-SYNONYMS WRLD)))
      (tau-runes ,(GET-TAU-RUNES WRLD))
      (tau-lost-runes ,(MERGE-SORT-LEXORDER (GLOBAL-VAL 'TAU-LOST-RUNES WRLD))))))

(defun initialize-tau-globals
  (wrld)
  (putprop-if-different 'tau-runes
    'global-value
    nil
    (putprop-if-different 'tau-conjunctive-rules
      'global-value
      nil
      (putprop-if-different 'tau-mv-nth-synonyms
        'global-value
        nil
        (putprop-if-different 'tau-lost-runes
          'global-value
          nil
          wrld)))))

(defun collect-tau-relevant-triples
  (wrld ans)
  (cond ((endp wrld) ans)
    ((or (and (eq (cadr (car wrld)) 'formals)
         (not (eq (cddr (car wrld)) *acl2-property-unbound*)))
       (and (eq (car (car wrld)) 'event-landmark)
         (eq (cadr (car wrld)) 'global-value))) (collect-tau-relevant-triples (cdr wrld)
        (cons (car wrld) ans)))
    (t (collect-tau-relevant-triples (cdr wrld) ans))))