type-set-b - ACL2 Book

other

(in-package "ACL2")

*number-of-numeric-type-set-bits*constant

(defconst *number-of-numeric-type-set-bits* 7)

*type-set-binary-+-table-list*constant

(defconst *type-set-binary-+-table-list*
  (let ((len (expt 2 *number-of-numeric-type-set-bits*)))
    (cons (list :header :dimensions (list len len)
        :maximum-length (1+ (* len len))
        :default *ts-acl2-number*
        :name '*type-set-binary-+-table*)
      (type-set-binary-+-alist (1- len) (1- len) nil))))

*type-set-binary-+-table*constant

(defconst *type-set-binary-+-table*
  (compress2 'type-set-binary-+-table
    *type-set-binary-+-table-list*))

*type-set-binary-*-table-list*constant

(defconst *type-set-binary-*-table-list*
  (let ((len (expt 2 *number-of-numeric-type-set-bits*)))
    (cons (list :header :dimensions (list len len)
        :maximum-length (1+ (* len len))
        :default *ts-acl2-number*
        :name '*type-set-binary-*-table*)
      (type-set-binary-*-alist (1- len) (1- len) nil))))

*type-set-binary-*-table*constant

(defconst *type-set-binary-*-table*
  (compress2 'type-set-binary-*-table
    *type-set-binary-*-table-list*))

*type-set-<-table-list*constant

(defconst *type-set-<-table-list*
  (cons (list :header :dimensions '(64 64)
      :maximum-length (1+ (* 64 64))
      :name '*type-set-<-table*)
    (type-set-<-alist 63 63 nil)))

*type-set-<-table*constant

(defconst *type-set-<-table*
  (compress2 'type-set-<-table *type-set-<-table-list*))

assoc-equal-cdrfunction

(defun assoc-equal-cdr
  (x alist)
  (declare (xargs :mode :logic :guard (alistp alist)))
  (cond ((endp alist) nil)
    ((equal x (cdar alist)) (car alist))
    (t (assoc-equal-cdr x (cdr alist)))))

runepfunction

(defun runep
  (x wrld)
  (declare (xargs :guard (if (and (consp x) (consp (cdr x)) (symbolp (cadr x)))
        (and (plist-worldp wrld)
          (alistp (getpropc (cadr x) 'runic-mapping-pairs nil wrld)))
        t)))
  (cond ((and (consp x) (consp (cdr x)) (symbolp (cadr x))) (car (assoc-equal-cdr x
          (getpropc (cadr x) 'runic-mapping-pairs nil wrld))))
    (t nil)))

base-symbolmacro

(defmacro base-symbol (rune) `(cadr ,RUNE))

strip-base-symbolsmacro

(defmacro strip-base-symbols (runes) `(strip-cadrs ,RUNES))

fnumefunction

(defun fnume
  (rune wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
        (consp rune)
        (consp (cdr rune))
        (symbolp (base-symbol rune))
        (alistp (getpropc (base-symbol rune) 'runic-mapping-pairs nil wrld)))))
  (car (assoc-equal-cdr rune
      (getpropc (base-symbol rune) 'runic-mapping-pairs nil wrld))))

frunic-mapping-pairfunction

(defun frunic-mapping-pair
  (rune wrld)
  (assoc-equal-cdr rune
    (getpropc (base-symbol rune) 'runic-mapping-pairs nil wrld)))

fn-rune-numefunction

(defun fn-rune-nume
  (fn nflg xflg wrld)
  (let* ((runic-mapping-pairs (getpropc fn 'runic-mapping-pairs nil wrld)) (pair (if xflg
          (cadr runic-mapping-pairs)
          (car runic-mapping-pairs))))
    (if nflg
      (car pair)
      (cdr pair))))

definition-runesfunction

(defun definition-runes
  (fns xflg wrld)
  (cond ((null fns) nil)
    (t (cons (fn-rune-nume (car fns) nil xflg wrld)
        (definition-runes (cdr fns) xflg wrld)))))

get-next-numefunction

(defun get-next-nume
  (lst)
  (cond ((null lst) 0)
    ((and (eq (cadr (car lst)) 'runic-mapping-pairs)
       (consp (cddr (car lst)))) (+ (car (car (cddr (car lst)))) (length (cddr (car lst)))))
    (t (get-next-nume (cdr lst)))))

deref-macro-name-lstfunction

(defun deref-macro-name-lst
  (macro-name-lst macro-aliases)
  (cond ((atom macro-name-lst) nil)
    (t (cons (deref-macro-name (car macro-name-lst) macro-aliases)
        (deref-macro-name-lst (cdr macro-name-lst) macro-aliases)))))

*abbrev-rune-alist*constant

(defconst *abbrev-rune-alist*
  '((:d . :definition) (:e . :executable-counterpart)
    (:i . :induction)
    (:r . :rewrite)
    (:t . :type-prescription)))

translate-abbrev-runefunction

(defun translate-abbrev-rune
  (x macro-aliases)
  (declare (xargs :guard (alistp macro-aliases)))
  (let ((kwd (and (consp x)
         (consp (cdr x))
         (symbolp (cadr x))
         (cdr (assoc-eq (car x) *abbrev-rune-alist*)))))
    (cond (kwd (list* kwd
          (deref-macro-name (cadr x) macro-aliases)
          (cddr x)))
      (t x))))

rule-name-designatorpfunction

(defun rule-name-designatorp
  (x macro-aliases wrld)
  (cond ((symbolp x) (let ((x (deref-macro-name x macro-aliases)))
        (cond ((getpropc x 'runic-mapping-pairs nil wrld) x)
          (t (and (not (eq (getpropc x 'theory t wrld) t)) x)))))
    ((and (consp x) (null (cdr x)) (symbolp (car x))) (let* ((fn (deref-macro-name (car x) macro-aliases)))
        (and (function-symbolp fn wrld)
          (runep (list :executable-counterpart fn) wrld)
          fn)))
    (t (let ((x (translate-abbrev-rune x macro-aliases)))
        (and (runep x wrld) (base-symbol x))))))

theoryp1function

(defun theoryp1
  (lst macro-aliases wrld)
  (cond ((atom lst) (null lst))
    ((rule-name-designatorp (car lst) macro-aliases wrld) (theoryp1 (cdr lst) macro-aliases wrld))
    (t nil)))

theorypfunction

(defun theoryp
  (lst wrld)
  (theoryp1 lst (macro-aliases wrld) wrld))

runic-theoryp1function

(defun runic-theoryp1
  (prev-nume lst wrld)
  (cond ((atom lst) (null lst))
    (t (let ((nume (runep (car lst) wrld)))
        (cond ((and nume (or (null prev-nume) (> prev-nume nume))) (runic-theoryp1 nume (cdr lst) wrld))
          (t nil))))))

runic-theorypfunction

(defun runic-theoryp
  (lst wrld)
  (runic-theoryp1 nil lst wrld))

find-mapping-pairs-tail1function

(defun find-mapping-pairs-tail1
  (rune mapping-pairs)
  (cond ((null mapping-pairs) nil)
    ((equal rune (cdr (car mapping-pairs))) mapping-pairs)
    (t (find-mapping-pairs-tail1 rune (cdr mapping-pairs)))))

find-mapping-pairs-tailfunction

(defun find-mapping-pairs-tail
  (rune mapping-pairs wrld)
  (cond ((and mapping-pairs
       (eq (base-symbol rune) (cadr (cdr (car mapping-pairs))))) (find-mapping-pairs-tail1 rune mapping-pairs))
    (t (find-mapping-pairs-tail1 rune
        (getpropc (base-symbol rune) 'runic-mapping-pairs nil wrld)))))

augment-runic-theory1function

(defun augment-runic-theory1
  (lst mapping-pairs wrld ans)
  (cond ((null lst) ans)
    (t (let ((mapping-pairs (find-mapping-pairs-tail (car lst) mapping-pairs wrld)))
        (cond (mapping-pairs (augment-runic-theory1 (cdr lst)
              (cdr mapping-pairs)
              wrld
              (cons (car mapping-pairs) ans)))
          (t (augment-runic-theory1 (cdr lst) mapping-pairs wrld ans)))))))

augment-runic-theoryfunction

(defun augment-runic-theory
  (lst wrld)
  (augment-runic-theory1 (reverse lst) nil wrld nil))

*bad-runic-designator-string*constant

(defconst *bad-runic-designator-string*
  "This symbol was expected to be suitable for theory expressions; see :DOC ~
   theories, in particular the discussion of runic designators.  One possible ~
   source of this problem is an attempt to include an uncertified book with a ~
   deftheory event that attempts to use the above symbol in a deftheory event.")

convert-theory-to-unordered-mapping-pairs1function

(defun convert-theory-to-unordered-mapping-pairs1
  (lst macro-aliases wrld ans)
  (cond ((null lst) ans)
    ((symbolp (car lst)) (let ((temp (getpropc (deref-macro-name (car lst) macro-aliases)
             'runic-mapping-pairs
             nil
             wrld)))
        (cond ((and temp
             (eq (car (cdr (car temp))) :definition)
             (eq (car (cdr (cadr temp))) :executable-counterpart)) (convert-theory-to-unordered-mapping-pairs1 (cdr lst)
              macro-aliases
              wrld
              (if (equal (length temp) 4)
                (cons (car temp) (cons (cadddr temp) ans))
                (cons (car temp) ans))))
          (temp (convert-theory-to-unordered-mapping-pairs1 (cdr lst)
              macro-aliases
              wrld
              (revappend temp ans)))
          (t (convert-theory-to-unordered-mapping-pairs1 (cdr lst)
              macro-aliases
              wrld
              (augment-runic-theory1 (reverse (getpropc (car lst)
                    'theory
                    `(:error ,*BAD-RUNIC-DESIGNATOR-STRING*)
                    wrld))
                nil
                wrld
                ans))))))
    ((null (cdr (car lst))) (convert-theory-to-unordered-mapping-pairs1 (cdr lst)
        macro-aliases
        wrld
        (cons (cadr (getpropc (deref-macro-name (car (car lst)) macro-aliases)
              'runic-mapping-pairs
              `(:error ,*BAD-RUNIC-DESIGNATOR-STRING*)
              wrld))
          ans)))
    (t (convert-theory-to-unordered-mapping-pairs1 (cdr lst)
        macro-aliases
        wrld
        (cons (frunic-mapping-pair (translate-abbrev-rune (car lst) macro-aliases)
            wrld)
          ans)))))

convert-theory-to-unordered-mapping-pairsfunction

(defun convert-theory-to-unordered-mapping-pairs
  (lst wrld)
  (convert-theory-to-unordered-mapping-pairs1 lst
    (macro-aliases wrld)
    wrld
    nil))

duplicitous-cons-carfunction

(defun duplicitous-cons-car
  (x y)
  (cond ((equal (car x) (caar y)) y) (t (cons x y))))

duplicitous-revappend-carfunction

(defun duplicitous-revappend-car
  (lst ans)
  (cond ((null lst) ans)
    (t (duplicitous-revappend-car (cdr lst)
        (duplicitous-cons-car (car lst) ans)))))

duplicitous-merge-carfunction

(defun duplicitous-merge-car
  (parity lst1 lst2 ans)
  (cond ((null lst1) (duplicitous-revappend-car lst2 ans))
    ((null lst2) (duplicitous-revappend-car lst1 ans))
    ((if parity
       (> (car (car lst1)) (car (car lst2)))
       (< (car (car lst1)) (car (car lst2)))) (duplicitous-merge-car parity
        (cdr lst1)
        lst2
        (duplicitous-cons-car (car lst1) ans)))
    (t (duplicitous-merge-car parity
        lst1
        (cdr lst2)
        (duplicitous-cons-car (car lst2) ans)))))

duplicitous-sort-carfunction

(defun duplicitous-sort-car
  (parity lst)
  (cond ((null (cdr lst)) lst)
    (t (duplicitous-merge-car parity
        (duplicitous-sort-car (not parity) (evens lst))
        (duplicitous-sort-car (not parity) (odds lst))
        nil))))

augment-theoryfunction

(defun augment-theory
  (lst wrld)
  (declare (xargs :guard (theoryp lst wrld)))
  (cond ((runic-theoryp lst wrld) (augment-runic-theory lst wrld))
    (t (duplicitous-sort-car nil
        (convert-theory-to-unordered-mapping-pairs lst wrld)))))

assert$-runic-theorypmacro

(defmacro assert$-runic-theoryp
  (runic-theory-expr wrld)
  (declare (ignore wrld))
  runic-theory-expr)

runic-theoryfunction

(defun runic-theory
  (lst wrld)
  (cond ((runic-theoryp lst wrld) lst)
    (t (assert$-runic-theoryp (strip-cdrs (duplicitous-sort-car nil
            (convert-theory-to-unordered-mapping-pairs lst wrld)))
        wrld))))

other

(defrec enabled-structure
  ((index-of-last-enabling . theory-array) (array-name . array-length)
    array-name-root . array-name-suffix)
  t)

enabled-structure-pfunction

(defun enabled-structure-p
  (ens)
  (declare (xargs :guard t))
  (and (weak-enabled-structure-p ens)
    (array1p (access enabled-structure ens :array-name)
      (access enabled-structure ens :theory-array))
    (symbolp (access enabled-structure ens :array-name))
    (signed-byte-p *fixnum-bits*
      (access enabled-structure ens :array-length))
    (signed-byte-p *fixnum-bits*
      (access enabled-structure ens :index-of-last-enabling))
    (< (access enabled-structure ens :index-of-last-enabling)
      (access enabled-structure ens :array-length))
    (character-listp (access enabled-structure ens :array-name-root))
    (natp (access enabled-structure ens :array-name-suffix))
    (equal (access enabled-structure ens :array-length)
      (car (dimensions (access enabled-structure ens :array-name)
          (access enabled-structure ens :theory-array))))))

enabled-numepfunction

(defun enabled-numep
  (nume ens)
  (declare (type (or null (unsigned-byte 60)) nume)
    (xargs :guard (enabled-structure-p ens)))
  (cond ((null nume) t)
    ((> nume
       (the-fixnum (access enabled-structure ens :index-of-last-enabling))) t)
    (t (aref1 (access enabled-structure ens :array-name)
        (access enabled-structure ens :theory-array)
        (the-fixnat nume)))))

enabled-arith-numepfunction

(defun enabled-arith-numep
  (nume ens)
  (cond ((null nume) t)
    ((> (the-fixnat nume)
       (the-fixnum (access enabled-structure ens :index-of-last-enabling))) nil)
    (t (aref1 (access enabled-structure ens :array-name)
        (access enabled-structure ens :theory-array)
        (the-fixnat nume)))))

enabled-runepfunction

(defun enabled-runep
  (rune ens wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
        (consp rune)
        (consp (cdr rune))
        (symbolp (base-symbol rune))
        (enabled-structure-p ens)
        (fixnat-alistp (getpropc (base-symbol rune) 'runic-mapping-pairs nil wrld)))
      :guard-hints (("Goal" :do-not-induct t))))
  (enabled-numep (fnume rune wrld) ens))

active-runepmacro

(defmacro active-runep
  (rune)
  `(let* ((rune ,RUNE) (nume (and (consp rune)
          (consp (cdr rune))
          (symbolp (cadr rune))
          (fnume rune (w state)))))
    (and nume (enabled-numep nume ens))))

active-or-non-runepmacro

(defmacro active-or-non-runep
  (rune)
  `(let* ((rune ,RUNE) (nume (and (consp rune)
          (consp (cdr rune))
          (symbolp (cadr rune))
          (fnume rune (w state)))))
    (or (not nume) (enabled-numep nume ens))))

enabled-xfnpfunction

(defun enabled-xfnp
  (fn ens wrld)
  (cond ((flambdap fn) t)
    (t (enabled-numep (fn-rune-nume fn t t wrld) ens))))

sublis-var!mutual-recursion

(mutual-recursion (defun sublis-var!
    (alist term ens wrld ttree)
    (cond ((variablep term) (let ((a (assoc-eq term alist)))
          (cond (a (mv (cdr a) (quotep (cdr a)) ttree))
            (t (mv term nil ttree)))))
      ((fquotep term) (mv term t ttree))
      ((flambda-applicationp term) (mv-let (args flg ttree)
          (sublis-var!-lst alist (fargs term) ens wrld ttree)
          (cond (flg (sublis-var! (pairlis$ (lambda-formals (ffn-symb term)) args)
                (lambda-body (ffn-symb term))
                ens
                wrld
                ttree))
            (t (mv (cons-term (ffn-symb term) args) nil ttree)))))
      ((eq (ffn-symb term) 'if) (mv-let (arg1 flg1 ttree)
          (sublis-var! alist (fargn term 1) ens wrld ttree)
          (cond (flg1 (if (cadr arg1)
                (sublis-var! alist (fargn term 2) ens wrld ttree)
                (sublis-var! alist (fargn term 3) ens wrld ttree)))
            (t (mv-let (arg2 flg2 ttree)
                (sublis-var! alist (fargn term 2) ens wrld ttree)
                (mv-let (arg3 flg3 ttree)
                  (sublis-var! alist (fargn term 3) ens wrld ttree)
                  (declare (ignore flg3))
                  (cond ((equal arg2 arg3) (mv arg2 flg2 ttree))
                    (t (mv (fcons-term* 'if arg1 arg2 arg3) nil ttree)))))))))
      (t (mv-let (args flg ttree)
          (sublis-var!-lst alist (fargs term) ens wrld ttree)
          (cond ((and flg
               (logicp (ffn-symb term) wrld)
               (enabled-xfnp (ffn-symb term) ens wrld)
               (not (getpropc (ffn-symb term) 'constrainedp nil wrld))) (mv-let (erp val)
                (pstk (ev-fncall-w (ffn-symb term)
                    (strip-cadrs args)
                    wrld
                    nil
                    nil
                    t
                    t
                    nil))
                (cond (erp (mv (cons-term (ffn-symb term) args) nil ttree))
                  (t (mv (kwote val)
                      t
                      (push-lemma (fn-rune-nume (ffn-symb term) nil t wrld) ttree))))))
            (t (mv (cons-term (ffn-symb term) args) nil ttree)))))))
  (defun sublis-var!-lst
    (alist lst ens wrld ttree)
    (cond ((null lst) (mv nil t ttree))
      (t (mv-let (x flg1 ttree)
          (sublis-var! alist (car lst) ens wrld ttree)
          (mv-let (y flg2 ttree)
            (sublis-var!-lst alist (cdr lst) ens wrld ttree)
            (mv (cons x y) (and flg1 flg2) ttree)))))))

theory-warning-fns-auxfunction

(defun theory-warning-fns-aux
  (runes1 runes2 max-nume nume prev-rune1 prev-rune2 w acc)
  (declare (type (unsigned-byte 60) nume))
  (cond ((eql nume max-nume) (reverse acc))
    (t (let* ((found1 (eql (caar runes1) nume)) (found2 (eql (caar runes2) nume))
          (curr-rune1 (and found1 (cdar runes1)))
          (curr-rune2 (and found2 (cdar runes2)))
          (rest-runes1 (if found1
              (cdr runes1)
              runes1))
          (rest-runes2 (if found2
              (cdr runes2)
              runes2)))
        (theory-warning-fns-aux rest-runes1
          rest-runes2
          max-nume
          (1+f nume)
          curr-rune1
          curr-rune2
          w
          (if (and (eq (car curr-rune2) :executable-counterpart)
              (null prev-rune2)
              (not (and curr-rune1 (null prev-rune1)))
              (null (formals (cadr curr-rune2) w)))
            (cons (cadr curr-rune2) acc)
            acc))))))

theory-warning-fnsfunction

(defun theory-warning-fns
  (ens1 ens2 w)
  (theory-warning-fns-aux (cdr (access enabled-structure ens1 :theory-array))
    (cdr (access enabled-structure ens2 :theory-array))
    (1+ (access enabled-structure ens2 :index-of-last-enabling))
    0
    nil
    nil
    w
    nil))

other

(defun@par maybe-warn-about-theory
  (ens1 force-xnume-en1 imm-xnume-en1 ens2 ctx wrld state)
  (cond ((warning-disabled-p "Disable") (state-mac@par))
    (t (pprogn@par (let ((fns (theory-warning-fns ens1 ens2 wrld)))
          (if fns
            (warning$@par ctx
              ("Disable")
              "The following 0-ary function~#0~[~/s~] will now have ~#0~[its ~
                :definition rune~/their :definition runes~] disabled but ~
                ~#0~[its :executable-counterpart rune~/their ~
                :executable-counterpart runes~] enabled, which will allow ~
                ~#0~[its definition~/their definitions~] to open up after ~
                all:  ~&0.~|See :DOC theories."
              fns)
            (state-mac@par)))
        (cond ((and force-xnume-en1
             (not (enabled-numep *force-xnume* ens2))) (warning$@par ctx
              ("Disable")
              "Forcing has transitioned from enabled to disabled.~|See :DOC ~
            force."))
          ((and (not force-xnume-en1)
             (enabled-numep *force-xnume* ens2)) (warning$@par ctx
              ("Disable")
              "Forcing has transitioned from disabled to enabled.~|See :DOC ~
            force."))
          (t (state-mac@par)))
        (cond ((and imm-xnume-en1
             (not (enabled-numep *immediate-force-modep-xnume* ens2))) (warning$@par ctx
              ("Disable")
              "IMMEDIATE-FORCE-MODEP has transitioned from enabled to ~
            disabled.~|See :DOC force."))
          ((and (not imm-xnume-en1)
             (enabled-numep *immediate-force-modep-xnume* ens2)) (warning$@par ctx
              ("Disable")
              "IMMEDIATE-FORCE-MODEP has transitioned from disabled to ~
            enabled.~|See :DOC immediate-force-modep."))
          (t (state-mac@par)))))))

other

(defrec theory-invariant-record
  ((tterm . error) untrans-term . book)
  t)

enabled-disabled-runepsfunction

(defun enabled-disabled-runeps
  (exprs enableds disableds)
  (cond ((endp exprs) (mv nil (reverse enableds) (reverse disableds)))
    (t (let ((e (car exprs)))
        (case-match e
          (('active-runep ('quote rune)) (enabled-disabled-runeps (cdr exprs)
              (cons rune enableds)
              disableds))
          (('not ('active-runep ('quote rune))) (enabled-disabled-runeps (cdr exprs)
              enableds
              (cons rune disableds)))
          (& (mv t nil nil)))))))

theory-invariant-msg-implicationfunction

(defun theory-invariant-msg-implication
  (runeps1 runeps2)
  (mv-let (flg enableds1 disableds1)
    (enabled-disabled-runeps (if (eq (car runeps1) 'and)
        (cdr runeps1)
        (list runeps1))
      nil
      nil)
    (and (null flg)
      (mv-let (flg enableds2 disableds2)
        (enabled-disabled-runeps (if (eq (car runeps2) 'and)
            (cdr runeps2)
            (list runeps2))
          nil
          nil)
        (and (null flg)
          (or enableds1 disableds1)
          (or enableds2 disableds2)
          (let* ((en "the rune~#0~[ ~&0 is~/s ~&0 are~] enabled") (dis "the rune~#0~[ ~&0 is~/s ~&0 are~] not enabled")
              (msg0 (and enableds1 (msg en enableds1)))
              (msg1 (and enableds1 disableds1 " and "))
              (msg2 (and disableds1 (msg dis disableds1)))
              (msg3 (and enableds2 (msg en enableds2)))
              (msg4 (and enableds2 disableds2 " and "))
              (msg5 (and disableds2 (msg dis disableds2))))
            (msg "~|which asserts that if ~@0~@1~@2, then ~@3~@4~@5"
              (or msg0 "")
              (or msg1 "")
              (or msg2 "")
              (or msg3 "")
              (or msg4 "")
              (or msg5 ""))))))))

combine-andsfunction

(defun combine-ands
  (x y)
  (case-match x
    (('and . a) (case-match y (('and . b) `(and ,@A ,@B)) (& `(and ,@A y))))
    (& (case-match y (('and . a) `(and ,X ,@A)) (& `(and ,X ,Y))))))

theory-invariant-msg-active-runep-lstfunction

(defun theory-invariant-msg-active-runep-lst
  (lst acc)
  (cond ((atom lst) (and (cdr acc)
        (msg "~|which asserts that the runes ~&0 are not ~
                    ~#1~[both~/all~] enabled at the same time"
          (reverse acc)
          (cdr acc))))
    (t (let ((form (car lst)))
        (case-match form
          (('active-runep ('quote rune)) (theory-invariant-msg-active-runep-lst (cdr lst)
              (cons rune acc)))
          (t ""))))))

theory-invariant-msgfunction

(defun theory-invariant-msg
  (form)
  (case-match form
    (('not ('and . active-runep-lst)) (and (consp active-runep-lst)
        (consp (cdr active-runep-lst))
        (theory-invariant-msg-active-runep-lst active-runep-lst nil)))
    (('not ('active-runep ('quote rune))) (msg "~|which asserts that the rune ~x0 is not enabled"
        rune))
    (('incompatible rune1 rune2 . &) (msg "~|which asserts that the runes ~x0 and ~x1 are not both enabled at ~
           the same time"
        rune1
        rune2))
    (('incompatible! rune1 rune2 . &) (msg "~|which asserts that the runes ~x0 and ~x1 are not both enabled at ~
           the same time"
        rune1
        rune2))
    (('or ('not active-runeps1) active-runeps2) (theory-invariant-msg `(if ,ACTIVE-RUNEPS1
          ,ACTIVE-RUNEPS2
          t)))
    (('if active-runeps1 ('if active-runeps2 concl 't) 't) (theory-invariant-msg `(if ,(COMBINE-ANDS ACTIVE-RUNEPS1 ACTIVE-RUNEPS2)
          ,CONCL
          t)))
    (('if active-runeps1 ('or ('not active-runeps2) concl) 't) (theory-invariant-msg `(if ,(COMBINE-ANDS ACTIVE-RUNEPS1 ACTIVE-RUNEPS2)
          ,CONCL
          t)))
    (('if active-runeps1 active-runeps2 't) (theory-invariant-msg-implication active-runeps1
        active-runeps2))
    (& nil)))

other

(defrec certify-book-info
  (cert-op full-book-name . event-data-channel)
  nil)

other

(defrec useless-runes (tag data . full-book-string) nil)

active-useless-runesfunction

(defun active-useless-runes
  (state)
  (let ((useless-runes (f-get-global 'useless-runes state)))
    (and useless-runes
      (and (eq (access useless-runes useless-runes :tag) 'theory)
        (access useless-runes useless-runes :data)))))

*dot-sys-dir*constant

(defconst *dot-sys-dir* ".sys")

dot-sys-filenamefunction

(defun dot-sys-filename
  (full-book-string suffix)
  (let ((len (length full-book-string)) (posn (search *directory-separator-string*
          full-book-string
          :from-end t)))
    (assert$ (and (equal (subseq full-book-string (- len 5) len) ".lisp")
        posn)
      (concatenate 'string
        (subseq full-book-string 0 (1+ posn))
        *dot-sys-dir*
        (subseq full-book-string posn (- len 5))
        suffix))))

useless-runes-filenamefunction

(defun useless-runes-filename
  (full-book-string)
  (dot-sys-filename full-book-string "@useless-runes.lsp"))

event-data-filenamefunction

(defun event-data-filename
  (file tmp-p)
  (let ((len (length file)))
    (assert$ (equal (subseq file (- len 5) len) ".lisp")
      (concatenate 'string
        (subseq file 0 (- len 5))
        (if tmp-p
          "@event-data.lsp.temp"
          "@event-data.lsp")))))

active-useless-runes-filenamefunction

(defun active-useless-runes-filename
  (state)
  (let ((useless-runes (f-get-global 'useless-runes state)))
    (and useless-runes
      (useless-runes-filename (access useless-runes useless-runes :full-book-string)))))

other

(defun@par chk-theory-invariant1
  (theory-expr ens invariant-alist errp-acc ctx state)
  (cond ((null invariant-alist) (mv@par errp-acc nil state))
    (t (let* ((table-entry (car invariant-alist)) (inv-name (car table-entry))
          (inv-rec (cdr table-entry))
          (theory-inv (access theory-invariant-record inv-rec :tterm)))
        (mv-let (erp okp latches)
          (ev theory-inv
            (list (cons 'ens ens)
              (cons 'state (coerce-state-to-object state)))
            state
            nil
            nil
            t)
          (declare (ignore latches))
          (cond (erp (let* ((produced-by-msg (cond ((eq theory-expr :from-hint) "an :in-theory hint")
                     ((eq theory-expr :install) "the current event")
                     (t (msg "~x0" theory-expr)))) (theory-invariant-term (access theory-invariant-record inv-rec :untrans-term))
                  (msg (msg "Theory invariant ~x0 could not be evaluated on ~
                              the theory produced by ~@1~@2.  Theory invariant ~
                              ~P43 produced the error message:~%~@5~@6  See ~
                              :DOC theory-invariant."
                      inv-name
                      produced-by-msg
                      (if (active-useless-runes state)
                        (msg ", modified by subtracting the theory ~
                                       for the current event stored in file ~
                                       ~s0"
                          (active-useless-runes-filename state))
                        "")
                      (term-evisc-tuple nil state)
                      theory-invariant-term
                      okp
                      (if (access theory-invariant-record inv-rec :error)
                        "~|This theory invariant violation causes an ~
                                  error."
                        ""))))
                (mv-let@par (errp-acc state)
                  (cond ((access theory-invariant-record inv-rec :error) (mv-let@par (erp val state)
                        (er-soft@par ctx "Theory" "~@0" msg)
                        (declare (ignore erp val))
                        (mv@par t state)))
                    (t (pprogn@par (warning$@par ctx
                          "Theory"
                          `("~@0" (:error-msg ,OKP)
                            (:produced-by-msg ,PRODUCED-BY-MSG)
                            (:theory-invariant-name ,INV-NAME)
                            (:theory-invariant-term ,THEORY-INVARIANT-TERM))
                          msg)
                        (mv@par errp-acc state))))
                  (chk-theory-invariant1@par theory-expr
                    ens
                    (cdr invariant-alist)
                    errp-acc
                    ctx
                    state))))
            (okp (chk-theory-invariant1@par theory-expr
                ens
                (cdr invariant-alist)
                errp-acc
                ctx
                state))
            (t (let* ((produced-by-msg (cond ((eq theory-expr :from-hint) "an :in-theory hint")
                     ((eq theory-expr :install) "the current event")
                     (t (msg "~x0" theory-expr)))) (theory-invariant-term (access theory-invariant-record inv-rec :untrans-term))
                  (theory-invariant-book (access theory-invariant-record inv-rec :book))
                  (thy-inv-msg (theory-invariant-msg theory-invariant-term))
                  (msg (msg "Theory invariant ~x0, defined ~@1, failed on the ~
                            theory produced by ~@2~@3.  Theory invariant ~x0 ~
                            is ~@4~@5  See :DOC theory-invariant."
                      inv-name
                      (if (null theory-invariant-book)
                        "at the top-level"
                        (msg "in book ~x0"
                          (book-name-to-filename theory-invariant-book (w state) ctx)))
                      produced-by-msg
                      (if (active-useless-runes state)
                        (msg ", modified by subtracting the theory for ~
                                     the current event stored in file ~s0"
                          (active-useless-runes-filename state))
                        "")
                      (if thy-inv-msg
                        (msg "~P10~@2."
                          (term-evisc-tuple nil state)
                          theory-invariant-term
                          thy-inv-msg)
                        (msg "~P10."
                          (term-evisc-tuple nil state)
                          theory-invariant-term))
                      (if (access theory-invariant-record inv-rec :error)
                        "~|This theory invariant violation causes an ~
                                error."
                        ""))))
                (mv-let@par (errp-acc state)
                  (cond ((access theory-invariant-record inv-rec :error) (mv-let@par (erp val state)
                        (er-soft@par ctx "Theory" "~@0" msg)
                        (declare (ignore erp val))
                        (mv@par t state)))
                    (t (pprogn@par (warning$@par ctx
                          "Theory"
                          `("~@0" (:produced-by-msg ,PRODUCED-BY-MSG)
                            (:theory-invariant-name ,INV-NAME)
                            (:theory-invariant-term ,THEORY-INVARIANT-TERM))
                          msg)
                        (mv@par errp-acc state))))
                  (chk-theory-invariant1@par theory-expr
                    ens
                    (cdr invariant-alist)
                    errp-acc
                    ctx
                    state))))))))))

other

(defun@par chk-theory-invariant
  (theory-expr ens ctx state)
  (chk-theory-invariant1@par theory-expr
    ens
    (table-alist 'theory-invariant-table (w state))
    nil
    ctx
    state))

other

(defrec clause-id
  ((forcing-round . pool-lst) case-lst . primes)
  t)

pos-listpfunction

(defun pos-listp
  (l)
  (declare (xargs :guard t))
  (cond ((atom l) (eq l nil))
    (t (and (posp (car l)) (pos-listp (cdr l))))))

all-digits-pfunction

(defun all-digits-p
  (lst radix)
  (declare (xargs :guard (and (character-listp lst)
        (integerp radix)
        (<= 2 radix)
        (<= radix 36))))
  (cond ((endp lst) t)
    (t (and (digit-char-p (car lst) radix)
        (all-digits-p (cdr lst) radix)))))

d-pos-listpfunction

(defun d-pos-listp
  (lst)
  (declare (xargs :guard t))
  (cond ((atom lst) (null lst))
    ((natp (car lst)) (d-pos-listp (cdr lst)))
    (t (and (symbolp (car lst))
        (let ((name (symbol-name (car lst))))
          (and (not (equal name ""))
            (eql (char name 0) #\D)
            (all-digits-p (cdr (coerce name 'list)) 10)))
        (d-pos-listp (cdr lst))))))

clause-id-pfunction

(defun clause-id-p
  (cl-id)
  (declare (xargs :guard t))
  (case-match cl-id
    (((forcing-round . pool-lst) case-lst . primes) (and (natp forcing-round)
        (pos-listp pool-lst)
        (d-pos-listp case-lst)
        (natp primes)))
    (& nil)))

*initial-clause-id*constant

(defconst *initial-clause-id*
  (make clause-id
    :forcing-round 0
    :pool-lst nil
    :case-lst nil
    :primes 0))

chars-for-tilde-@-clause-id-phrase/periodsfunction

(defun chars-for-tilde-@-clause-id-phrase/periods
  (lst)
  (declare (xargs :guard (d-pos-listp lst)))
  (cond ((null lst) nil)
    ((null (cdr lst)) (explode-atom (car lst) 10))
    (t (append (explode-atom (car lst) 10)
        (cons #\.
          (chars-for-tilde-@-clause-id-phrase/periods (cdr lst)))))))

chars-for-tilde-@-clause-id-phrase/primesfunction

(defun chars-for-tilde-@-clause-id-phrase/primes
  (n)
  (declare (xargs :guard (and (integerp n) (>= n 0))))
  (cond ((= n 0) nil)
    ((= n 1) '(#\'))
    ((= n 2) '(#\' #\'))
    ((= n 3) '(#\' #\' #\'))
    (t (cons #\' (append (explode-atom n 10) '(#\'))))))

chars-for-tilde-@-clause-id-phrasefunction

(defun chars-for-tilde-@-clause-id-phrase
  (id)
  (declare (xargs :guard (clause-id-p id)))
  (append (if (= (access clause-id id :forcing-round) 0)
      nil
      `(#\[ ,@(EXPLODE-ATOM (ACCESS CLAUSE-ID ID :FORCING-ROUND) 10)
        #\]))
    (cond ((null (access clause-id id :pool-lst)) (cond ((null (access clause-id id :case-lst)) (append '(#\G #\o #\a #\l)
              (chars-for-tilde-@-clause-id-phrase/primes (access clause-id id :primes))))
          (t (append '(#\S #\u #\b #\g #\o #\a #\l #\ )
              (chars-for-tilde-@-clause-id-phrase/periods (access clause-id id :case-lst))
              (chars-for-tilde-@-clause-id-phrase/primes (access clause-id id :primes))))))
      (t (append '(#\S #\u #\b #\g #\o #\a #\l #\  #\*)
          (chars-for-tilde-@-clause-id-phrase/periods (access clause-id id :pool-lst))
          (cons #\/
            (append (chars-for-tilde-@-clause-id-phrase/periods (access clause-id id :case-lst))
              (chars-for-tilde-@-clause-id-phrase/primes (access clause-id id :primes)))))))))

string-for-tilde-@-clause-id-phrasefunction

(defun string-for-tilde-@-clause-id-phrase
  (id)
  (declare (xargs :guard (clause-id-p id)))
  (coerce (chars-for-tilde-@-clause-id-phrase id) 'string))

update-enabled-structure-arrayfunction

(defun update-enabled-structure-array
  (name header alist k old d new-n)
  (declare (xargs :guard (and (array1p name (cons header alist))
        (null (array-order header))
        (or (eq k nil) (and (natp k) (<= k (length alist))))
        (natp d)
        (<= new-n d)))
    (ignore k old d new-n))
  (compress1 name (cons header alist)))

increment-array-namefunction

(defun increment-array-name
  (ens incrmt-array-name-info)
  (let* ((root (access enabled-structure ens :array-name-root)) (suffix (cond ((eq incrmt-array-name-info t) (1+ (access enabled-structure ens :array-name-suffix)))
          (t (access enabled-structure ens :array-name-suffix))))
      (name (cond ((eq incrmt-array-name-info t) (intern (coerce (append root (explode-nonnegative-integer suffix 10 nil))
                'string)
              "ACL2"))
          ((keywordp incrmt-array-name-info) incrmt-array-name-info)
          (incrmt-array-name-info (intern (coerce (append root
                  (chars-for-tilde-@-clause-id-phrase incrmt-array-name-info))
                'string)
              "ACL2"))
          (t (access enabled-structure ens :array-name)))))
    (mv root suffix name)))

update-enabled-structurefunction

(defun update-enabled-structure
  (ens n d new-d alist augmented-p incrmt-array-name-info)
  (declare (ignore d augmented-p))
  (mv-let (root suffix name)
    (increment-array-name ens incrmt-array-name-info)
    (make enabled-structure
      :index-of-last-enabling n
      :theory-array (compress1 name
        (cons (list :header :dimensions (list new-d)
            :maximum-length (1+ new-d)
            :default nil
            :name name
            :order nil)
          alist))
      :array-name name
      :array-length new-d
      :array-name-root root
      :array-name-suffix suffix)))

load-theory-into-enabled-structure-1function

(defun load-theory-into-enabled-structure-1
  (theory augmented-p
    ens
    incrmt-array-name-info
    index-of-last-enabling
    wrld)
  (let* ((n (or index-of-last-enabling
         (max 0 (1- (get-next-nume wrld))))) (d (access enabled-structure ens :array-length))
      (new-d (cond ((and (eq augmented-p 'ext-p)
             (consp theory)
             (>= (caar theory) d)) (* 2 (1+ (caar theory))))
          ((< n d) d)
          (t (max (* 2 d) (+ d (* 500 (1+ (floor (- n d) 500))))))))
      (alist (if augmented-p
          theory
          (augment-runic-theory theory wrld))))
    (update-enabled-structure ens
      n
      d
      new-d
      alist
      augmented-p
      incrmt-array-name-info)))

other

(defun@par load-theory-into-enabled-structure
  (theory-expr theory
    augmented-p
    ens
    incrmt-array-name-info
    index-of-last-enabling
    wrld
    ctx
    state)
  (let ((ens (load-theory-into-enabled-structure-1 theory
         augmented-p
         ens
         incrmt-array-name-info
         index-of-last-enabling
         wrld)))
    (er-progn@par (if (or (eq theory-expr :no-check)
          (eq (ld-skip-proofsp state) 'include-book)
          (eq (ld-skip-proofsp state) 'include-book-with-locals))
        (value@par nil)
        (chk-theory-invariant@par theory-expr ens ctx state))
      (value@par ens))))

initial-global-enabled-structurefunction

(defun initial-global-enabled-structure
  (root-string)
  (let* ((root (coerce root-string 'list)) (name (intern (coerce (append root '(#\0)) 'string) "ACL2"))
      (d 1000))
    (make enabled-structure
      :index-of-last-enabling -1
      :theory-array (compress1 name
        (cons (list :header :dimensions (list d)
            :maximum-length (1+ d)
            :default nil
            :name name)
          nil))
      :array-name name
      :array-length d
      :array-name-root root
      :array-name-suffix 0)))

recompress-global-enabled-structurefunction

(defun recompress-global-enabled-structure
  (varname wrld)
  (let ((ges1 (getpropc varname 'global-value nil wrld)))
    (cond (ges1 (prog2$ (maybe-flush-and-compress1 (access enabled-structure ges1 :array-name)
            (access enabled-structure ges1 :theory-array))
          t))
      (t t))))

recompress-stobj-accessor-arraysfunction

(defun recompress-stobj-accessor-arrays
  (stobj-names wrld)
  (if (endp stobj-names)
    t
    (let* ((st (car stobj-names)) (ar (getpropc st 'accessor-names nil wrld)))
      (prog2$ (or (null ar) (maybe-flush-and-compress1 st ar))
        (recompress-stobj-accessor-arrays (cdr stobj-names) wrld)))))

*fake-rune-for-type-set*constant

(defconst *fake-rune-for-type-set*
  '(:fake-rune-for-type-set nil))

puffertfunction

(defun puffert
  (ttree)
  (push-lemma *fake-rune-for-type-set* ttree))

immediate-forcepfunction

(defun immediate-forcep
  (fn ens)
  (cond ((eq fn 'case-split) 'case-split)
    ((enabled-numep *immediate-force-modep-xnume* ens) t)
    (t nil)))

numeric-type-setmacro

(defmacro numeric-type-set
  (ts)
  `(let ((numeric-ts-use-nowhere-else (ts-intersection (check-vars-not-free (numeric-ts-use-nowhere-else) ,TS)
         *ts-acl2-number*)))
    (if (ts= numeric-ts-use-nowhere-else ,TS)
      ,TS
      (ts-union numeric-ts-use-nowhere-else *ts-zero*))))

rational-type-setmacro

(defmacro rational-type-set
  (ts)
  `(let ((numeric-ts-use-nowhere-else (ts-intersection (check-vars-not-free (numeric-ts-use-nowhere-else) ,TS)
         *ts-rational*)))
    (if (ts= numeric-ts-use-nowhere-else ,TS)
      ,TS
      (ts-union numeric-ts-use-nowhere-else *ts-zero*))))

type-set-binary-+function

(defun type-set-binary-+
  (term ts1 ts2 ttree ttree0)
  (let ((arg1 (fargn term 1)) (arg2 (fargn term 2)))
    (cond ((or (ts= ts1 *ts-empty*) (ts= ts2 *ts-empty*)) (mv *ts-empty* ttree))
      ((and (equal arg2 ''-1)
         (ts-subsetp ts1 *ts-positive-integer*)) (mv *ts-non-negative-integer* (puffert ttree)))
      ((and (equal arg1 ''-1)
         (ts-subsetp ts2 *ts-positive-integer*)) (mv *ts-non-negative-integer* (puffert ttree)))
      (t (let ((ans (aref2 'type-set-binary-+-table
               *type-set-binary-+-table*
               (numeric-type-set ts1)
               (numeric-type-set ts2))))
          (mv ans
            (puffert (if (ts= ans *ts-acl2-number*)
                ttree0
                ttree))))))))

type-set-binary-*function

(defun type-set-binary-*
  (ts1 ts2 ttree ttree0)
  (cond ((or (ts= ts1 *ts-empty*) (ts= ts2 *ts-empty*)) (mv *ts-empty* ttree))
    (t (let ((ans (aref2 'type-set-binary-*-table
             *type-set-binary-*-table*
             (numeric-type-set ts1)
             (numeric-type-set ts2))))
        (mv ans
          (puffert (if (ts= ans *ts-acl2-number*)
              ttree0
              ttree)))))))

type-set-notfunction

(defun type-set-not
  (ts ttree ttree0)
  (cond ((ts= ts *ts-nil*) (mv *ts-t* (puffert ttree)))
    ((ts-subsetp *ts-nil* ts) (mv *ts-boolean* ttree0))
    (t (mv *ts-nil* (puffert ttree)))))

type-set-<-1function

(defun type-set-<-1
  (r arg2 commutedp type-alist)
  (cond ((endp type-alist) (mv *ts-boolean* nil))
    (t (let ((type-alist-entry (car type-alist)))
        (case-match type-alist-entry
          ((typed-term type . ttree) (mv-let (c leftp x)
              (case-match typed-term
                (('< ('quote c) x) (if (rationalp c)
                    (mv c t x)
                    (mv nil nil x)))
                (('< x ('quote c)) (if (rationalp c)
                    (mv c nil x)
                    (mv nil nil nil)))
                (& (mv nil nil nil)))
              (cond ((null c) (type-set-<-1 r arg2 commutedp (cdr type-alist)))
                (leftp (cond ((and (<= r c) (ts= type *ts-t*) (equal x arg2)) (mv (if commutedp
                          *ts-nil*
                          *ts-t*)
                        (puffert ttree)))
                    ((and (if commutedp
                         (< c r)
                         (<= c r))
                       (ts= type *ts-nil*)
                       (equal x arg2)) (mv (if commutedp
                          *ts-t*
                          *ts-nil*)
                        (puffert ttree)))
                    (t (type-set-<-1 r arg2 commutedp (cdr type-alist)))))
                (t (cond ((and (if commutedp
                         (<= r c)
                         (< r c))
                       (ts= type *ts-nil*)
                       (equal x arg2)) (mv (if commutedp
                          *ts-nil*
                          *ts-t*)
                        (puffert ttree)))
                    ((and (<= c r) (ts= type *ts-t*) (equal x arg2)) (mv (if commutedp
                          *ts-t*
                          *ts-nil*)
                        (puffert ttree)))
                    (t (type-set-<-1 r arg2 commutedp (cdr type-alist))))))))
          (& (type-set-<-1 r arg2 commutedp (cdr type-alist))))))))

type-set-<function

(defun type-set-<
  (arg1 arg2 ts1 ts2 type-alist ttree ttree0 pot-lst pt)
  (let* ((nts1 (numeric-type-set ts1)) (nts2 (numeric-type-set ts2)))
    (cond ((and (equal arg2 *1*) (ts-subsetp nts1 *ts-integer*)) (mv-let (ts ttree)
          (type-set-< *0*
            arg1
            *ts-zero*
            ts1
            type-alist
            (puffert ttree)
            ttree
            pot-lst
            pt)
          (type-set-not ts ttree ttree0)))
      ((and (equal arg1 *-1*) (ts-subsetp nts2 *ts-integer*)) (mv-let (ts ttree)
          (type-set-< arg2
            *0*
            ts2
            *ts-zero*
            type-alist
            (puffert ttree)
            ttree
            pot-lst
            pt)
          (type-set-not ts ttree ttree0)))
      (t (mv-let (returned-ts returned-ttree)
          (cond ((and (quotep arg1) (rationalp (cadr arg1))) (type-set-<-1 (cadr arg1) arg2 nil type-alist))
            ((and (quotep arg2) (rationalp (cadr arg2))) (type-set-<-1 (cadr arg2) arg1 t type-alist))
            (t (mv *ts-boolean* nil)))
          (if (not (ts= returned-ts *ts-boolean*))
            (mv returned-ts (cons-tag-trees returned-ttree ttree0))
            (let ((temp-ts (if (or (ts-intersectp ts1 *ts-complex-rational*)
                     (ts-intersectp ts2 *ts-complex-rational*))
                   *ts-boolean*
                   (aref2 'type-set-<-table *type-set-<-table* nts1 nts2))))
              (cond ((or (ts= temp-ts *ts-t*) (ts= temp-ts *ts-nil*)) (mv temp-ts (puffert ttree)))
                ((null pot-lst) (mv *ts-boolean* ttree0))
                (t (mv-let (contradictionp new-pot-lst)
                    (add-polys0 (list (normalize-poly (add-linear-terms :lhs arg2
                            :rhs arg1
                            (base-poly ttree0 '<= nil nil))))
                      pot-lst
                      pt
                      nil
                      2)
                    (declare (ignore new-pot-lst))
                    (if contradictionp
                      (mv *ts-t* (access poly contradictionp :ttree))
                      (mv-let (contradictionp new-pot-lst)
                        (add-polys0 (list (normalize-poly (add-linear-terms :lhs arg1
                                :rhs arg2
                                (base-poly ttree0 '< nil nil))))
                          pot-lst
                          pt
                          nil
                          2)
                        (declare (ignore new-pot-lst))
                        (if contradictionp
                          (mv *ts-nil* (access poly contradictionp :ttree))
                          (mv *ts-boolean* ttree0))))))))))))))

type-set-unary--function

(defun type-set-unary--
  (ts ttree ttree0)
  (let ((ts1 (numeric-type-set ts)))
    (cond ((ts= ts1 *ts-acl2-number*) (mv *ts-acl2-number* ttree0))
      (t (mv (ts-builder ts1
            (*ts-zero* *ts-zero*)
            (*ts-one* *ts-negative-integer*)
            (*ts-integer>1* *ts-negative-integer*)
            (*ts-positive-ratio* *ts-negative-ratio*)
            (*ts-negative-integer* *ts-positive-integer*)
            (*ts-negative-ratio* *ts-positive-ratio*)
            (*ts-complex-rational* *ts-complex-rational*))
          (puffert ttree))))))

type-set-unary-/function

(defun type-set-unary-/
  (ts ttree ttree0)
  (let* ((ts1 (numeric-type-set ts)) (ans (ts-builder ts1
          (*ts-zero* *ts-zero*)
          (*ts-one* *ts-one*)
          (*ts-integer>1* (ts-intersection0 *ts-positive-ratio*
              (ts-complement0 *ts-zero*)
              (ts-complement0 *ts-one*)))
          (*ts-positive-ratio* *ts-positive-rational*)
          (*ts-negative-rational* *ts-negative-rational*)
          (*ts-complex-rational* *ts-complex-rational*))))
    (cond ((ts= ans *ts-acl2-number*) (mv *ts-acl2-number* (puffert ttree0)))
      (t (mv ans (puffert ttree))))))

type-set-numeratorfunction

(defun type-set-numerator
  (ts ttree ttree0)
  (let* ((ts1 (rational-type-set ts)) (ans (ts-builder ts1
          (*ts-zero* *ts-zero*)
          (*ts-one* *ts-one*)
          (*ts-integer>1* *ts-integer>1*)
          (*ts-positive-ratio* *ts-positive-integer*)
          (*ts-negative-rational* *ts-negative-integer*))))
    (cond ((ts= ans *ts-integer*) (mv *ts-integer* (puffert ttree0)))
      (t (mv ans (puffert ttree))))))

type-set-denominatorfunction

(defun type-set-denominator
  (ts ttree ttree0)
  (let* ((ts1 (rational-type-set ts)) (ans (ts-builder ts1
          (*ts-integer* *ts-one*)
          (*ts-ratio* *ts-integer>1*))))
    (cond ((ts= ans *ts-positive-integer*) (mv *ts-positive-integer* (puffert ttree0)))
      (t (mv ans (puffert ttree))))))

type-set-realpartfunction

(defun type-set-realpart
  (ts ttree ttree0)
  (cond ((ts-intersectp ts *ts-complex-rational*) (mv *ts-rational* (puffert ttree0)))
    (t (mv (numeric-type-set ts) (puffert ttree)))))

type-set-imagpartfunction

(defun type-set-imagpart
  (ts ttree ttree0)
  (cond ((ts-subsetp ts *ts-complex-rational*) (mv (ts-union *ts-positive-rational* *ts-negative-rational*)
        (puffert ttree)))
    ((ts-intersectp ts *ts-complex-rational*) (mv *ts-rational* (puffert ttree0)))
    (t (mv *ts-zero* (puffert ttree)))))

type-set-complexfunction

(defun type-set-complex
  (ts1 ts2 ttree ttree0)
  (let ((ts1 (rational-type-set ts1)) (ts2 (rational-type-set ts2)))
    (cond ((ts= ts2 *ts-zero*) (mv ts1 (puffert ttree)))
      ((ts= (ts-intersection ts2 *ts-zero*) *ts-empty*) (mv *ts-complex-rational* (puffert ttree)))
      ((ts= ts1 *ts-rational*) (mv *ts-acl2-number* (puffert ttree0)))
      (t (mv (ts-union ts1 *ts-complex-rational*) (puffert ttree))))))

other

(defrec recognizer-tuple
  (fn (nume . true-ts) (false-ts . strongp) . rune)
  t)

*initial-recognizer-alist*constant

(defconst *initial-recognizer-alist*
  (list (make recognizer-tuple
      :fn 'integerp
      :true-ts *ts-integer*
      :false-ts (ts-complement *ts-integer*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'rationalp
      :true-ts *ts-rational*
      :false-ts (ts-complement *ts-rational*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'complex-rationalp
      :true-ts *ts-complex-rational*
      :false-ts (ts-complement *ts-complex-rational*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'acl2-numberp
      :true-ts *ts-acl2-number*
      :false-ts (ts-complement *ts-acl2-number*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'consp
      :true-ts *ts-cons*
      :false-ts (ts-complement *ts-cons*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'atom
      :true-ts (ts-complement *ts-cons*)
      :false-ts *ts-cons*
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'listp
      :true-ts (ts-union *ts-cons* *ts-nil*)
      :false-ts (ts-complement (ts-union *ts-cons* *ts-nil*))
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'true-listp
      :true-ts *ts-true-list*
      :false-ts (ts-complement *ts-true-list*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'characterp
      :true-ts *ts-character*
      :false-ts (ts-complement *ts-character*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'stringp
      :true-ts *ts-string*
      :false-ts (ts-complement *ts-string*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'null
      :true-ts *ts-nil*
      :false-ts (ts-complement *ts-nil*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)
    (make recognizer-tuple
      :fn 'symbolp
      :true-ts *ts-symbol*
      :false-ts (ts-complement *ts-symbol*)
      :strongp t
      :nume nil
      :rune *fake-rune-for-anonymous-enabled-rule*)))

most-recent-enabled-recog-tuple1function

(defun most-recent-enabled-recog-tuple1
  (lst ens)
  (cond ((endp lst) nil)
    ((enabled-numep (access recognizer-tuple (car lst) :nume)
       ens) (car lst))
    (t (most-recent-enabled-recog-tuple1 (cdr lst) ens))))

most-recent-enabled-recog-tuplefunction

(defun most-recent-enabled-recog-tuple
  (fn wrld ens)
  (let ((lst (getpropc fn 'recognizer-alist nil wrld)))
    (and lst (most-recent-enabled-recog-tuple1 lst ens))))

type-set-recognizerfunction

(defun type-set-recognizer
  (recog-tuple arg-ts ttree ttree0)
  (let ((ts (ts-builder arg-ts
         ((access recognizer-tuple recog-tuple :true-ts) *ts-t*)
         ((access recognizer-tuple recog-tuple :false-ts) *ts-nil*))))
    (cond ((ts= ts *ts-boolean*) (mv *ts-boolean*
          (push-lemma (access recognizer-tuple recog-tuple :rune)
            ttree0)))
      (t (mv ts
          (push-lemma (access recognizer-tuple recog-tuple :rune)
            ttree))))))

type-set-carfunction

(defun type-set-car
  (ts ttree ttree0)
  (cond ((ts-intersectp ts *ts-cons*) (mv *ts-unknown* ttree0))
    (t (mv *ts-nil* ttree))))

type-set-cdrfunction

(defun type-set-cdr
  (ts ttree ttree0)
  (let ((cdr-ts (ts-builder ts
         (*ts-proper-cons* *ts-true-list*)
         (*ts-improper-cons* (ts-complement *ts-true-list*))
         (otherwise *ts-nil*))))
    (mv cdr-ts
      (if (ts= cdr-ts *ts-unknown*)
        ttree0
        (puffert ttree)))))

type-set-coercefunction

(defun type-set-coerce
  (term ts1 ts2 ttree1 ttree2 ttree0)
  (cond ((equal (fargn term 2) ''list) (cond ((ts-intersectp *ts-string* ts1) (mv *ts-true-list* (puffert ttree0)))
        (t (mv *ts-nil* (puffert ttree1)))))
    ((quotep (fargn term 2)) (mv *ts-string* (puffert ttree0)))
    ((ts-disjointp *ts-non-t-non-nil-symbol* ts2) (mv *ts-string* (puffert ttree2)))
    (t (mv (ts-union *ts-true-list* *ts-string*) (puffert ttree0)))))

type-set-intern-in-package-of-symbolfunction

(defun type-set-intern-in-package-of-symbol
  (ts1 ts2 ttree1 ttree2 ttree0)
  (cond ((ts-disjointp ts1 *ts-string*) (mv *ts-nil* (puffert ttree1)))
    ((ts-disjointp ts2 *ts-symbol*) (mv *ts-nil* (puffert ttree2)))
    (t (mv *ts-symbol* (puffert ttree0)))))

type-set-lengthfunction

(defun type-set-length
  (ts ttree ttree0)
  (let ((ans (ts-builder ts
         (*ts-string* *ts-non-negative-integer*)
         (*ts-cons* *ts-positive-integer*)
         (otherwise *ts-zero*))))
    (cond ((ts= ans *ts-integer*) (mv *ts-integer* (puffert ttree0)))
      (t (mv ans (puffert ttree))))))

type-set-consfunction

(defun type-set-cons
  (ts2 ttree ttree0)
  (let ((ts (ts-builder ts2
         (*ts-true-list* *ts-proper-cons*)
         (otherwise *ts-improper-cons*))))
    (cond ((ts= ts *ts-cons*) (mv ts (puffert ttree0)))
      (t (mv ts (puffert ttree))))))

*singleton-type-sets*constant

(defconst *singleton-type-sets*
  (list *ts-t* *ts-nil* *ts-zero* *ts-one*))

type-set-equalfunction

(defun type-set-equal
  (ts1 ts2 ttree ttree0)
  (cond ((member ts1 *singleton-type-sets*) (cond ((ts= ts1 ts2) (mv *ts-t* (puffert ttree)))
        ((ts-intersectp ts1 ts2) (mv *ts-boolean* (puffert ttree0)))
        (t (mv *ts-nil* (puffert ttree)))))
    ((ts-intersectp ts1 ts2) (mv *ts-boolean* (puffert ttree0)))
    (t (mv *ts-nil* (puffert ttree)))))

type-set-quotefunction

(defun type-set-quote
  (evg)
  (cond ((atom evg) (cond ((rationalp evg) (cond ((integerp evg) (cond ((int= evg 0) *ts-zero*)
                ((int= evg 1) *ts-one*)
                ((> evg 0) *ts-integer>1*)
                (t *ts-negative-integer*)))
            ((> evg 0) *ts-positive-ratio*)
            (t *ts-negative-ratio*)))
        ((complex-rationalp evg) *ts-complex-rational*)
        ((symbolp evg) (cond ((eq evg t) *ts-t*)
            ((eq evg nil) *ts-nil*)
            (t *ts-non-t-non-nil-symbol*)))
        ((stringp evg) *ts-string*)
        (t *ts-character*)))
    ((true-listp evg) *ts-proper-cons*)
    (t *ts-improper-cons*)))

type-set-char-codefunction

(defun type-set-char-code
  (ts ttree ttree0)
  (cond ((ts-disjointp ts *ts-character*) (mv *ts-zero* (puffert ttree)))
    (t (mv *ts-non-negative-integer* (puffert ttree0)))))

fn-count-1function

(defun fn-count-1
  (flg x fn-count-acc p-fn-count-acc)
  (declare (xargs :guard (and (if flg
          (pseudo-term-listp x)
          (pseudo-termp x))
        (integerp fn-count-acc)
        (integerp p-fn-count-acc))
      :verify-guards nil))
  (cond (flg (cond ((atom x) (mv fn-count-acc p-fn-count-acc))
        (t (mv-let (fn-cnt p-fn-cnt)
            (fn-count-1 nil (car x) fn-count-acc p-fn-count-acc)
            (fn-count-1 t (cdr x) fn-cnt p-fn-cnt)))))
    ((variablep x) (mv fn-count-acc p-fn-count-acc))
    ((fquotep x) (mv fn-count-acc (+ p-fn-count-acc (fn-count-evg (cadr x)))))
    (t (fn-count-1 t (fargs x) (1+ fn-count-acc) p-fn-count-acc))))

fn-countmacro

(defmacro fn-count (term) `(fn-count-1 nil ,TERM 0 0))

term-orderfunction

(defun term-order
  (term1 term2)
  (declare (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))))
  (term-order1 term1 term2 nil))

other

(defrec type-prescription
  (basic-ts (nume . term)
    (hyps . backchain-limit-lst)
    (vars . rune) . corollary)
  t)

find-runed-type-prescriptionfunction

(defun find-runed-type-prescription
  (rune lst)
  (cond ((null lst) nil)
    ((equal rune (access type-prescription (car lst) :rune)) (car lst))
    (t (find-runed-type-prescription rune (cdr lst)))))

mv-atffunction

(defun mv-atf
  (not-flg mbt mbf tta fta ttree1 ttree2)
  (if not-flg
    (mv mbf
      mbt
      fta
      tta
      (if (or mbt mbf)
        (cons-tag-trees ttree1 ttree2)
        nil))
    (mv mbt
      mbf
      tta
      fta
      (if (or mbt mbf)
        (cons-tag-trees ttree1 ttree2)
        nil))))

assume-true-false-errorfunction

(defun assume-true-false-error
  (type-alist x temp-temp)
  (er hard
    'assume-true-false-error
    "It was thought impossible for an equivalence relation, e.g., ~x0, ~
    to have anything besides a non-empty proper subset of ~
    *ts-boolean* on the type-alist!  But in the type-alist ~x1 the ~
    term ~x2 has type set ~x3."
    (ffn-symb x)
    type-alist
    x
    temp-temp))

non-cons-cdrfunction

(defun non-cons-cdr
  (term)
  (cond ((variablep term) term)
    ((fquotep term) term)
    ((eq (ffn-symb term) 'cons) (non-cons-cdr (fargn term 2)))
    (t term)))

canonical-representativefunction

(defun canonical-representative
  (equiv term type-alist)
  (declare (xargs :guard (symbolp equiv)))
  (cond ((null type-alist) (mv nil t term nil))
    (t (let ((first-term (caar type-alist)) (ts (cadar type-alist)))
        (cond ((or (variablep first-term)
             (not (eq (ffn-symb first-term) equiv))) (canonical-representative equiv term (cdr type-alist)))
          ((equal term (fargn first-term 1)) (cond ((ts= ts *ts-t*) (mv t nil (fargn first-term 2) (cddar type-alist)))
              (t (mv t t term nil))))
          ((equal term (fargn first-term 2)) (mv t t term nil))
          (t (canonical-representative equiv term (cdr type-alist))))))))

subst-type-alist1-checkfunction

(defun subst-type-alist1-check
  (old equiv type-alist)
  (cond ((null type-alist) nil)
    (t (or (let ((term (caar type-alist)))
          (and (ffn-symb-p term equiv)
            (or (equal old (fargn term 1)) (equal old (fargn term 2)))))
        (subst-type-alist1-check old equiv (cdr type-alist))))))

nil-fnfunction

(defun nil-fn
  nil
  (declare (xargs :guard t :mode :logic))
  nil)

*nil-fn-ts-entry*constant

(defconst *nil-fn-ts-entry*
  (list* (cons-term 'nil-fn nil)
    *ts-nil*
    (push-lemma '(:definition nil-fn) nil)))

subst-type-alist1function

(defun subst-type-alist1
  (new old equiv ttree type-alist acc)
  (cond ((null type-alist) (reverse acc))
    (t (subst-type-alist1 new
        old
        equiv
        ttree
        (cdr type-alist)
        (let ((term (caar type-alist)))
          (cond ((and (ffn-symb-p term equiv)
               (or (equal old (fargn term 1)) (equal old (fargn term 2)))) (let ((equiv-call (if (equal old (fargn term 1))
                     (cons-term* equiv new (fargn term 2))
                     (cons-term* equiv (fargn term 1) new))))
                (cond ((quotep equiv-call) (cons *nil-fn-ts-entry* acc))
                  (t (cons (list* equiv-call
                        (cadar type-alist)
                        (puffert (cons-tag-trees (cddar type-alist) ttree)))
                      acc)))))
            (t (cons (car type-alist) acc))))))))

subst-type-alistfunction

(defun subst-type-alist
  (new old equiv ttree type-alist)
  (cond ((subst-type-alist1-check old equiv type-alist) (subst-type-alist1 new old equiv ttree type-alist nil))
    (t type-alist)))

infect-type-alist-entryfunction

(defun infect-type-alist-entry
  (entry ttree)
  (cons (car entry)
    (cons (cadr entry) (cons-tag-trees (cddr entry) ttree))))

infect-new-type-alist-entries2function

(defun infect-new-type-alist-entries2
  (new-type-alist old-type-alist ttree)
  (cond ((null new-type-alist) nil)
    ((equal (caar new-type-alist) (caar old-type-alist)) (cons (car new-type-alist)
        (infect-new-type-alist-entries2 (cdr new-type-alist)
          (cdr old-type-alist)
          ttree)))
    (t (cons (infect-type-alist-entry (car new-type-alist) ttree)
        (infect-new-type-alist-entries2 (cdr new-type-alist)
          (cdr old-type-alist)
          ttree)))))

infect-new-type-alist-entries1function

(defun infect-new-type-alist-entries1
  (new-type-alist old-type-alist ttree n)
  (if (zp n)
    (infect-new-type-alist-entries2 new-type-alist
      old-type-alist
      ttree)
    (cons (infect-type-alist-entry (car new-type-alist) ttree)
      (infect-new-type-alist-entries1 (cdr new-type-alist)
        old-type-alist
        ttree
        (1- n)))))

infect-new-type-alist-entriesfunction

(defun infect-new-type-alist-entries
  (new-type-alist old-type-alist ttree)
  (if (null ttree)
    new-type-alist
    (infect-new-type-alist-entries1 new-type-alist
      old-type-alist
      ttree
      (- (length new-type-alist) (length old-type-alist)))))

extend-type-alist-simplefunction

(defun extend-type-alist-simple
  (term ts ttree type-alist)
  (cond ((ts= ts *ts-unknown*) type-alist)
    ((variablep term) (cons (list* term ts ttree) type-alist))
    ((fquotep term) type-alist)
    (t (cons (list* term ts ttree) type-alist))))

extend-type-alist1function

(defun extend-type-alist1
  (equiv occursp1
    occursp2
    both-canonicalp
    arg1-canon
    arg2-canon
    swap-flg
    term
    ts
    ttree
    type-alist)
  (cons (cond ((and (not swap-flg) both-canonicalp) (list* term ts ttree))
      (swap-flg (list* (cons-term* equiv arg2-canon arg1-canon)
          ts
          (puffert ttree)))
      (t (list* (cons-term* equiv arg1-canon arg2-canon)
          ts
          (puffert ttree))))
    (cond ((ts= ts *ts-nil*) type-alist)
      (swap-flg (cond (occursp2 (subst-type-alist arg1-canon
              arg2-canon
              equiv
              ttree
              type-alist))
          (t type-alist)))
      (t (cond (occursp1 (subst-type-alist arg2-canon
              arg1-canon
              equiv
              ttree
              type-alist))
          (t type-alist))))))

extend-type-alistfunction

(defun extend-type-alist
  (term ts ttree type-alist wrld)
  (declare (xargs :guard (and (pseudo-termp term) (not (quotep term)))))
  (cond ((and (nvariablep term)
       (not (fquotep term))
       (equivalence-relationp (ffn-symb term) wrld)) (cond ((equal (fargn term 1) (fargn term 2)) type-alist)
        ((not (or (ts= ts *ts-t*) (ts= ts *ts-nil*))) (cond ((ts-intersectp ts *ts-nil*) type-alist)
            (t (extend-type-alist term
                *ts-t*
                (puffert ttree)
                type-alist
                wrld))))
        (t (let ((equiv (ffn-symb term)) (arg1 (fargn term 1))
              (arg2 (fargn term 2)))
            (mv-let (occursp1 canonicalp1 arg1-canon ttree1)
              (canonical-representative equiv arg1 type-alist)
              (mv-let (occursp2 canonicalp2 arg2-canon ttree2)
                (canonical-representative equiv arg2 type-alist)
                (cond ((equal arg1-canon arg2-canon) type-alist)
                  (t (let ((swap-flg (term-order arg1-canon arg2-canon)))
                      (extend-type-alist1 equiv
                        occursp1
                        occursp2
                        (and canonicalp1 canonicalp2)
                        arg1-canon
                        arg2-canon
                        swap-flg
                        term
                        ts
                        (cons-tag-trees ttree1 (cons-tag-trees ttree2 ttree))
                        type-alist))))))))))
    (t (extend-type-alist-simple term ts ttree type-alist))))

zip-variable-type-alistfunction

(defun zip-variable-type-alist
  (vars pairs)
  (cond ((null vars) nil)
    ((ts= (caar pairs) *ts-unknown*) (zip-variable-type-alist (cdr vars) (cdr pairs)))
    (t (cons (cons (car vars) (car pairs))
        (zip-variable-type-alist (cdr vars) (cdr pairs))))))

assoc-equivfunction

(defun assoc-equiv
  (fn arg1 arg2 alist)
  (cond ((eq alist nil) nil)
    ((and (ffn-symb-p (caar alist) fn)
       (if (equal (fargn (caar alist) 2) arg2)
         (equal (fargn (caar alist) 1) arg1)
         (and (equal (fargn (caar alist) 1) arg2)
           (equal (fargn (caar alist) 2) arg1)))) (car alist))
    (t (assoc-equiv fn arg1 arg2 (cdr alist)))))

assoc-equiv+function

(defun assoc-equiv+
  (equiv arg1 arg2 type-alist)
  (cond ((equal arg1 arg2) (mv *ts-t* (puffert nil)))
    ((and (eq equiv 'equal) (quotep arg1) (quotep arg2)) (mv *ts-nil*
        (push-lemma '(:executable-counterpart equal) nil)))
    (t (mv-let (occursp1 canonicalp1 arg1-canon ttree1)
        (canonical-representative equiv arg1 type-alist)
        (declare (ignore canonicalp1))
        (cond ((and occursp1 (equal arg1-canon arg2)) (mv *ts-t* (puffert ttree1)))
          ((and occursp1
             (eq equiv 'equal)
             (quotep arg1-canon)
             (quotep arg2)) (mv *ts-nil*
              (push-lemma '(:executable-counterpart equal) ttree1)))
          (t (mv-let (occursp2 canonicalp2 arg2-canon ttree2)
              (canonical-representative equiv arg2 type-alist)
              (declare (ignore canonicalp2))
              (cond ((and occursp2 (equal arg1-canon arg2-canon)) (mv *ts-t* (puffert (cons-tag-trees ttree1 ttree2))))
                ((and (eq equiv 'equal)
                   occursp2
                   (quotep arg1-canon)
                   (quotep arg2-canon)) (mv *ts-nil*
                    (push-lemma '(:executable-counterpart equal)
                      (cons-tag-trees ttree1 ttree2))))
                (t (let ((temp-temp (assoc-equiv equiv arg1-canon arg2-canon type-alist)))
                    (cond (temp-temp (cond ((ts= (cadr temp-temp) *ts-t*) (mv (er hard
                                'assoc-equiv+
                                "Please send the authors of ACL2 a replayable ~
                              transcript of this problem if possible, so that ~
                              they can see what went wrong in the function ~
                              assoc-equiv+.  The offending call was ~x0.  The ~
                              surprising type-set arose from a call of ~x1."
                                (list 'assoc-equiv+
                                  (kwote equiv)
                                  (kwote arg1)
                                  (kwote arg2)
                                  type-alist)
                                (list 'assoc-equiv
                                  (kwote equiv)
                                  (kwote arg1-canon)
                                  (kwote arg2-canon)
                                  '<same_type-alist>))
                              nil))
                          ((ts= (cadr temp-temp) *ts-nil*) (mv *ts-nil*
                              (cons-tag-trees (cddr temp-temp)
                                (cons-tag-trees ttree1 ttree2))))
                          (t (let ((erp (assume-true-false-error type-alist
                                   (mcons-term* equiv arg1-canon arg2-canon)
                                   (cadr temp-temp))))
                              (mv erp nil)))))
                      (t (mv nil nil)))))))))))))

assoc-type-alistfunction

(defun assoc-type-alist
  (term type-alist wrld)
  (cond ((variablep term) (let ((temp (assoc-eq term type-alist)))
        (if temp
          (mv (cadr temp) (cddr temp))
          (mv nil nil))))
    ((fquotep term) (mv nil nil))
    ((equivalence-relationp (ffn-symb term) wrld) (assoc-equiv+ (ffn-symb term)
        (fargn term 1)
        (fargn term 2)
        type-alist))
    (t (let ((temp (assoc-equal term type-alist)))
        (if temp
          (mv (cadr temp) (cddr temp))
          (mv nil nil))))))

look-in-type-alistfunction

(defun look-in-type-alist
  (term type-alist wrld)
  (mv-let (ts ttree)
    (assoc-type-alist term type-alist wrld)
    (mv (if ts
        ts
        *ts-unknown*)
      ttree)))

member-char-stringpfunction

(defun member-char-stringp
  (chr str i)
  (declare (xargs :guard (and (stringp str) (integerp i) (< i (length str)))
      :measure (nfix (+ 1 i))))
  (cond ((not (mbt (integerp i))) nil)
    ((< i 0) nil)
    (t (or (eql chr (char str i))
        (member-char-stringp chr str (1- i))))))

terminal-substringp1function

(defun terminal-substringp1
  (str1 str2 max1 max2)
  (declare (xargs :guard (and (stringp str1)
        (stringp str2)
        (integerp max1)
        (integerp max2)
        (< max1 (length str1))
        (< max2 (length str2))
        (<= max1 max2))
      :measure (nfix (+ 1 max1))))
  (cond ((not (mbt (integerp max1))) nil)
    ((< max1 0) t)
    ((eql (char str1 max1) (char str2 max2)) (terminal-substringp1 str1 str2 (1- max1) (1- max2)))
    (t nil)))

terminal-substringpfunction

(defun terminal-substringp
  (str1 str2 max1 max2)
  (declare (xargs :guard (and (stringp str1)
        (stringp str2)
        (integerp max1)
        (integerp max2)
        (< max1 (length str1))
        (< max2 (length str2)))))
  (cond ((< max2 max1) nil)
    (t (terminal-substringp1 str1 str2 max1 max2))))

evg-occurfunction

(defun evg-occur
  (x y)
  (declare (xargs :guard t))
  (cond ((atom y) (cond ((characterp y) (and (characterp x) (eql x y)))
        ((stringp y) (cond ((characterp x) (member-char-stringp x y (1- (length y))))
            ((stringp x) (terminal-substringp x y (1- (length x)) (1- (length y))))
            (t nil)))
        ((symbolp y) (cond ((characterp x) (let ((sny (symbol-name y)))
                (member-char-stringp x sny (1- (length sny)))))
            ((stringp x) (let ((sny (symbol-name y)))
                (terminal-substringp x
                  sny
                  (1- (length x))
                  (1- (length sny)))))
            ((symbolp x) (eq x y))
            (t nil)))
        ((integerp y) (and (integerp x)
            (or (int= x y)
              (and (<= 0 x)
                (<= x
                  (if (< y 0)
                    (- y)
                    y))))))
        ((rationalp y) (cond ((integerp x) (or (evg-occur x (numerator y))
                (evg-occur x (denominator y))))
            ((rationalp x) (= x y))
            (t nil)))
        ((complex-rationalp y) (cond ((rationalp x) (or (evg-occur x (realpart y)) (evg-occur x (imagpart y))))
            ((complex-rationalp x) (= x y))
            (t nil)))
        (t (er hard?
            'evg-occur
            "Surprising case:  ~x0"
            `(evg-occur ,X ,Y)))))
    (t (or (evg-occur x (car y)) (evg-occur x (cdr y))))))

occurmutual-recursion

(mutual-recursion (defun occur
    (term1 term2)
    (declare (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))))
    (cond ((variablep term2) (eq term1 term2))
      ((fquotep term2) (cond ((quotep term1) (evg-occur (cadr term1) (cadr term2)))
          (t nil)))
      ((equal term1 term2) t)
      (t (occur-lst term1 (fargs term2)))))
  (defun occur-lst
    (term1 args2)
    (declare (xargs :guard (and (pseudo-termp term1) (pseudo-term-listp args2))))
    (cond ((endp args2) nil)
      (t (or (occur term1 (car args2)) (occur-lst term1 (cdr args2)))))))

pseudo-variantpmutual-recursion

(mutual-recursion (defun pseudo-variantp
    (term1 term2)
    (declare (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))))
    (cond ((variablep term1) (not (quotep term2)))
      ((fquotep term1) (equal term1 term2))
      ((or (variablep term2) (fquotep term2)) nil)
      (t (and (equal (ffn-symb term1) (ffn-symb term2))
          (pseudo-variantp-list (fargs term1) (fargs term2))))))
  (defun pseudo-variantp-list
    (args1 args2)
    (declare (xargs :guard (and (pseudo-term-listp args1) (pseudo-term-listp args2))))
    (cond ((endp args1) t)
      (t (and (pseudo-variantp (car args1) (car args2))
          (pseudo-variantp-list (cdr args1) (cdr args2)))))))

decrement-worse-than-clkmacro

(defmacro decrement-worse-than-clk
  (clk)
  (declare (xargs :guard (symbolp clk)))
  `(if (< ,CLK 2)
    ,CLK
    (1-f ,CLK)))

with-decrement-worse-than-clkmacro

(defmacro with-decrement-worse-than-clk
  (clk form)
  (declare (xargs :guard (symbolp clk)))
  `(let ((,CLK (decrement-worse-than-clk ,CLK)))
    (declare (type (unsigned-byte 60) ,CLK))
    ,FORM))

worse-than-builtin-clocked-bodymacro

(defmacro worse-than-builtin-clocked-body
  (clk)
  (declare (xargs :guard (atom clk)))
  `(cond ((basic-worse-than term1 term2 ,CLK) t)
    ((pseudo-variantp term1 term2) nil)
    ((variablep term1) nil)
    ((fquotep term1) nil)
    (t (worse-than-lst (fargs term1) term2 ,CLK))))

worse-than-builtin-clockedmutual-recursion

(mutual-recursion (defun worse-than-builtin-clocked
    (term1 term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count term1) (acl2-count term2)) 2)
        :well-founded-relation o<))
    (cond ((zpf clk) nil)
      (t (let ((clk (1-f clk)))
          (declare (type (unsigned-byte 60) clk))
          (worse-than-builtin-clocked-body clk)))))
  (defun worse-than-or-equal-builtin-clocked
    (term1 term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count term1) (acl2-count term2)) 3)
        :well-founded-relation o<))
    (if (pseudo-variantp term1 term2)
      (equal term1 term2)
      (worse-than-builtin-clocked term1
        term2
        (decrement-worse-than-clk clk))))
  (defun basic-worse-than-lst1
    (args1 args2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-term-listp args1) (pseudo-term-listp args2))
        :measure (make-ord 1 (+ 1 (acl2-count args1) (acl2-count args2)) 0)
        :well-founded-relation o<))
    (cond ((endp args1) nil)
      ((or (and (or (variablep (car args1)) (fquotep (car args1)))
           (not (or (variablep (car args2)) (fquotep (car args2)))))
         (worse-than-builtin-clocked (car args2) (car args1) clk)) t)
      (t (basic-worse-than-lst1 (cdr args1) (cdr args2) clk))))
  (defun basic-worse-than-lst2
    (args1 args2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-term-listp args1) (pseudo-term-listp args2))
        :measure (make-ord 1 (+ 1 (acl2-count args1) (acl2-count args2)) 0)
        :well-founded-relation o<))
    (cond ((endp args1) nil)
      ((worse-than-builtin-clocked (car args1) (car args2) clk) t)
      (t (basic-worse-than-lst2 (cdr args1) (cdr args2) clk))))
  (defun basic-worse-than
    (term1 term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count term1) (acl2-count term2)) 0)
        :well-founded-relation o<))
    (cond ((variablep term2) (cond ((eq term1 term2) nil) (t (occur term2 term1))))
      ((fquotep term2) (cond ((variablep term1) t)
          ((fquotep term1) (> (fn-count-evg (cadr term1)) (fn-count-evg (cadr term2))))
          (t t)))
      ((variablep term1) nil)
      ((fquotep term1) nil)
      ((cond ((flambda-applicationp term1) (equal (ffn-symb term1) (ffn-symb term2)))
         (t (eq (ffn-symb term1) (ffn-symb term2)))) (cond ((pseudo-variantp term1 term2) nil)
          (t (with-decrement-worse-than-clk clk
              (cond ((basic-worse-than-lst1 (fargs term1) (fargs term2) clk) nil)
                (t (basic-worse-than-lst2 (fargs term1) (fargs term2) clk)))))))
      (t nil)))
  (defun some-subterm-worse-than-or-equal
    (term1 term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count term1) (acl2-count term2)) 1)
        :well-founded-relation o<))
    (cond ((variablep term1) (eq term1 term2))
      (t (with-decrement-worse-than-clk clk
          (cond ((if (pseudo-variantp term1 term2)
               (equal term1 term2)
               (basic-worse-than term1 term2 clk)) t)
            ((fquotep term1) nil)
            (t (some-subterm-worse-than-or-equal-lst (fargs term1)
                term2
                clk)))))))
  (defun some-subterm-worse-than-or-equal-lst
    (args term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-term-listp args) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count args) (acl2-count term2)) 0)
        :well-founded-relation o<))
    (cond ((endp args) nil)
      (t (or (some-subterm-worse-than-or-equal (car args) term2 clk)
          (some-subterm-worse-than-or-equal-lst (cdr args) term2 clk)))))
  (defun worse-than-lst
    (args term2 clk)
    (declare (type (unsigned-byte 60) clk)
      (xargs :guard (and (pseudo-term-listp args) (pseudo-termp term2))
        :measure (make-ord 1 (+ 1 (acl2-count args) (acl2-count term2)) 0)
        :well-founded-relation o<))
    (cond ((endp args) nil)
      (t (or (some-subterm-worse-than-or-equal (car args) term2 clk)
          (worse-than-lst (cdr args) term2 clk))))))

encapsulate

(encapsulate ((worse-than (term1 term2)
     t
     :guard (and (pseudo-termp term1) (pseudo-termp term2))))
  (logic)
  (local (defun worse-than
      (term1 term2)
      (declare (ignore term1 term2))
      nil)))

encapsulate

(encapsulate ((worse-than-or-equal (term1 term2)
     t
     :guard (and (pseudo-termp term1) (pseudo-termp term2))))
  (logic)
  (local (defun worse-than-or-equal
      (term1 term2)
      (declare (ignore term1 term2))
      nil)))

worse-than-clkmacro

(defmacro worse-than-clk nil 15)

worse-than-builtinfunction

(defun worse-than-builtin
  (term1 term2)
  (declare (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))))
  (worse-than-builtin-clocked term1 term2 (worse-than-clk)))

worse-than-or-equal-builtinfunction

(defun worse-than-or-equal-builtin
  (term1 term2)
  (declare (xargs :guard (and (pseudo-termp term1) (pseudo-termp term2))))
  (worse-than-or-equal-builtin-clocked term1
    term2
    (worse-than-clk)))

other

(defattach (worse-than worse-than-builtin) :skip-checks t)

other

(defattach (worse-than-or-equal worse-than-or-equal-builtin)
  :skip-checks t)

other

(defrec ancestor
  (lit atm var-cnt fn-cnt p-fn-cnt tokens . bkptr)
  t)

make-ancestor-binding-hypmacro

(defmacro make-ancestor-binding-hyp
  (hyp unify-subst)
  `(make ancestor
    :lit :binding-hyp :atm ,HYP
    :var-cnt ,UNIFY-SUBST
    :tokens nil
    :bkptr nil))

ancestor-binding-hyp-pmacro

(defmacro ancestor-binding-hyp-p
  (anc)
  `(eq (access ancestor ,ANC :lit) :binding-hyp))

ancestor-binding-hyp/hypmacro

(defmacro ancestor-binding-hyp/hyp
  (anc)
  `(access ancestor ,ANC :atm))

ancestor-binding-hyp/unify-substmacro

(defmacro ancestor-binding-hyp/unify-subst
  (anc)
  `(access ancestor ,ANC :var-cnt))

push-ancestorfunction

(defun push-ancestor
  (lit tokens ancestors bkptr)
  (let* ((alit lit) (alit-atm (mv-let (not-flg atm)
          (strip-not alit)
          (declare (ignore not-flg))
          atm)))
    (mv-let (var-cnt-alit-atm fn-cnt-alit-atm p-fn-cnt-alit-atm)
      (var-fn-count alit-atm nil)
      (cons (make ancestor
          :lit alit
          :atm alit-atm
          :var-cnt var-cnt-alit-atm
          :fn-cnt fn-cnt-alit-atm
          :p-fn-cnt p-fn-cnt-alit-atm
          :tokens tokens
          :bkptr bkptr)
        ancestors))))

ancestor-listpfunction

(defun ancestor-listp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
    ((not (weak-ancestor-p (car x))) nil)
    ((ancestor-binding-hyp-p (car x)) (and (null (access ancestor (car x) :tokens))
        (ancestor-listp (cdr x))))
    (t (let* ((anc (car x)) (alit (access ancestor anc :lit))
          (alit-atm (access ancestor anc :atm))
          (var-cnt-alit-atm (access ancestor anc :var-cnt))
          (fn-cnt-alit-atm (access ancestor anc :fn-cnt))
          (p-fn-cnt-alit-atm (access ancestor anc :p-fn-cnt))
          (atokens (access ancestor anc :tokens)))
        (and (pseudo-termp alit)
          (pseudo-termp alit-atm)
          (integerp var-cnt-alit-atm)
          (integerp fn-cnt-alit-atm)
          (integerp p-fn-cnt-alit-atm)
          (true-listp atokens)
          (ancestor-listp (cdr x)))))))

earlier-ancestor-biggerpfunction

(defun earlier-ancestor-biggerp
  (var-cnt fn-cnt p-fn-cnt tokens ancestors)
  (declare (xargs :guard (and (integerp var-cnt)
        (integerp fn-cnt)
        (integerp p-fn-cnt)
        (true-listp tokens)
        (ancestor-listp ancestors))))
  (cond ((endp ancestors) nil)
    (t (let* ((anc (car ancestors)) (var-cnt-alit-atm (access ancestor anc :var-cnt))
          (fn-cnt-alit-atm (access ancestor anc :fn-cnt))
          (p-fn-cnt-alit-atm (access ancestor anc :p-fn-cnt))
          (atokens (access ancestor anc :tokens)))
        (cond ((and (intersectp-equal tokens atokens)
             (var-or-fn-count-< var-cnt
               var-cnt-alit-atm
               fn-cnt
               fn-cnt-alit-atm
               p-fn-cnt
               p-fn-cnt-alit-atm)) t)
          (t (earlier-ancestor-biggerp var-cnt
              fn-cnt
              p-fn-cnt
              tokens
              (cdr ancestors))))))))

equal-mod-commutingfunction

(defun equal-mod-commuting
  (x y wrld)
  (declare (xargs :guard (and (pseudo-termp x) (pseudo-termp y) (plist-worldp wrld))))
  (cond ((variablep x) (eq x y))
    ((variablep y) nil)
    ((or (fquotep x) (fquotep y)) nil)
    ((equal x y) t)
    ((flambdap (ffn-symb x)) nil)
    (t (let ((fnx (ffn-symb x)))
        (and (eq fnx (ffn-symb y))
          (if (member-eq fnx '(equal iff))
            t
            (and wrld (equivalence-relationp fnx wrld)))
          (equal (fargn x 1) (fargn y 2))
          (equal (fargn x 2) (fargn y 1)))))))

ancestors-check1function

(defun ancestors-check1
  (lit-atm lit var-cnt fn-cnt p-fn-cnt ancestors tokens)
  (declare (xargs :guard (and (pseudo-termp lit-atm)
        (pseudo-termp lit)
        (integerp var-cnt)
        (integerp fn-cnt)
        (integerp p-fn-cnt)
        (ancestor-listp ancestors)
        (true-listp tokens))))
  (cond ((endp ancestors) (mv nil nil))
    ((ancestor-binding-hyp-p (car ancestors)) (ancestors-check1 lit-atm
        lit
        var-cnt
        fn-cnt
        p-fn-cnt
        (cdr ancestors)
        tokens))
    (t (let ((alit (access ancestor (car ancestors) :lit)) (alit-atm (access ancestor (car ancestors) :atm))
          (var-cnt-alit-atm (access ancestor (car ancestors) :var-cnt))
          (fn-cnt-alit-atm (access ancestor (car ancestors) :fn-cnt))
          (p-fn-cnt-alit-atm (access ancestor (car ancestors) :p-fn-cnt))
          (atokens (access ancestor (car ancestors) :tokens)))
        (cond ((equal-mod-commuting alit lit nil) (mv t t))
          ((equal-mod-commuting lit-atm alit-atm nil) (mv t nil))
          ((intersectp-equal tokens atokens) (cond ((and (nvariablep alit-atm)
                 (not (fquotep alit-atm))
                 (nvariablep lit-atm)
                 (not (fquotep lit-atm))
                 (equal (ffn-symb lit-atm) (ffn-symb alit-atm))
                 (not (var-or-fn-count-< var-cnt
                     var-cnt-alit-atm
                     fn-cnt
                     fn-cnt-alit-atm
                     p-fn-cnt
                     p-fn-cnt-alit-atm))) (mv t nil))
              (t (ancestors-check1 lit-atm
                  lit
                  var-cnt
                  fn-cnt
                  p-fn-cnt
                  (cdr ancestors)
                  tokens))))
          ((and (not (var-or-fn-count-< var-cnt
                 var-cnt-alit-atm
                 fn-cnt
                 fn-cnt-alit-atm
                 p-fn-cnt
                 p-fn-cnt-alit-atm))
             (worse-than-or-equal lit-atm alit-atm)) (cond ((earlier-ancestor-biggerp var-cnt
                 fn-cnt
                 p-fn-cnt
                 atokens
                 (cdr ancestors)) (ancestors-check1 lit-atm
                  lit
                  var-cnt
                  fn-cnt
                  p-fn-cnt
                  (cdr ancestors)
                  tokens))
              (t (mv t nil))))
          (t (ancestors-check1 lit-atm
              lit
              var-cnt
              fn-cnt
              p-fn-cnt
              (cdr ancestors)
              tokens)))))))

ancestors-check-builtinfunction

(defun ancestors-check-builtin
  (lit ancestors tokens)
  (declare (xargs :guard (and (pseudo-termp lit)
        (ancestor-listp ancestors)
        (true-listp tokens))))
  (cond ((endp ancestors) (mv nil nil))
    (t (mv-let (not-flg lit-atm)
        (strip-not lit)
        (declare (ignore not-flg))
        (mv-let (var-cnt fn-cnt p-fn-cnt)
          (var-fn-count lit-atm nil)
          (ancestors-check1 lit-atm
            lit
            var-cnt
            fn-cnt
            p-fn-cnt
            ancestors
            tokens))))))

other

(defproxy ancestors-check (* * *) => (mv * *))

other

(defattach (ancestors-check ancestors-check-builtin)
  :skip-checks t)

map-multiply-carfunction

(defun map-multiply-car
  (multiplicative-constant x)
  (cond ((endp x) nil)
    (t (cons (cons (* multiplicative-constant (car (car x)))
          (cdr (car x)))
        (map-multiply-car multiplicative-constant (cdr x))))))

normalize-addendfunction

(defun normalize-addend
  (addend)
  (cond ((variablep addend) (cons 1 addend))
    ((fquotep addend) (cons 1 addend))
    ((flambda-applicationp addend) (cons 1 addend))
    ((eq (ffn-symb addend) 'unary--) (cons -1 (fargn addend 1)))
    ((eq (ffn-symb addend) 'binary-*) (cond ((and (quotep (fargn addend 1))
           (rationalp (unquote (fargn addend 1)))) (cons (unquote (fargn addend 1)) (fargn addend 2)))
        (t (cons 1 addend))))
    (t (cons 1 addend))))

insert-cdr-term-orderfunction

(defun insert-cdr-term-order
  (item list)
  (cond ((endp list) (list item))
    ((term-order (cdr (car list)) (cdr item)) (cons (car list) (insert-cdr-term-order item (cdr list))))
    (t (cons item list))))

normalize-linear-sum-2function

(defun normalize-linear-sum-2
  (term)
  (cond ((eq (fn-symb term) 'binary-+) (insert-cdr-term-order (normalize-addend (fargn term 1))
        (normalize-linear-sum-2 (fargn term 2))))
    (t (list (normalize-addend term)))))

normalize-linear-sum-1function

(defun normalize-linear-sum-1
  (additive-constant term)
  (cond ((variablep term) (mv additive-constant 1 term))
    ((fquotep term) (cond ((rationalp (unquote term)) (mv (+ additive-constant (unquote term)) 1 *0*))
        (t (mv additive-constant 1 term))))
    ((flambda-applicationp term) (mv additive-constant 1 term))
    ((eq (ffn-symb term) 'unary--) (mv additive-constant -1 (fargn term 1)))
    ((eq (ffn-symb term) 'binary-*) (cond ((and (quotep (fargn term 1))
           (rationalp (unquote (fargn term 1)))) (mv additive-constant
            (unquote (fargn term 1))
            (fargn term 2)))
        (t (mv additive-constant 1 term))))
    ((eq (ffn-symb term) 'binary-+) (let* ((temp-1 (normalize-linear-sum-2 term)) (multiplicative-constant (car (car temp-1))))
        (cond ((or (eql multiplicative-constant 0)
             (eql multiplicative-constant 1)) (mv additive-constant 1 temp-1))
          (t (let ((temp-2 (map-multiply-car (/ multiplicative-constant) temp-1)))
              (mv additive-constant multiplicative-constant temp-2))))))
    (t (mv additive-constant 1 term))))

normalize-linear-sumfunction

(defun normalize-linear-sum
  (term)
  (cond ((variablep term) (mv 0 1 term))
    ((fquotep term) (mv 0 1 term))
    ((flambda-applicationp term) (mv 0 1 term))
    ((eq (ffn-symb term) 'unary--) (mv 0 -1 (fargn term 1)))
    ((eq (ffn-symb term) 'binary-*) (cond ((and (quotep (fargn term 1))
           (rationalp (unquote (fargn term 1)))) (mv 0 (unquote (fargn term 1)) (fargn term 2)))
        (t (mv 0 1 term))))
    ((eq (ffn-symb term) 'binary-+) (cond ((and (quotep (fargn term 1))
           (rationalp (unquote (fargn term 1)))) (normalize-linear-sum-1 (unquote (fargn term 1))
            (fargn term 2)))
        (t (normalize-linear-sum-1 0 term))))
    (t (mv 0 1 term))))

normalize-linear-sum-p1function

(defun normalize-linear-sum-p1
  (stripped-term term-to-match)
  (cond ((null stripped-term) nil)
    ((ffn-symb-p term-to-match 'binary-+) (normalize-linear-sum-p1 (cdr stripped-term)
        (fargn term-to-match 2)))
    (t (null (cdr stripped-term)))))

normalize-linear-sum-pfunction

(defun normalize-linear-sum-p
  (stripped-term term-to-match)
  (let ((term (cond ((and (ffn-symb-p term-to-match 'binary-+)
            (quotep (fargn term-to-match 1))) (fargn term-to-match 2))
         (t term-to-match))))
    (cond ((and (consp stripped-term)
         (consp (car stripped-term))
         (acl2-numberp (caar stripped-term))) (normalize-linear-sum-p1 stripped-term term))
      (t (not (ffn-symb-p term 'binary-+))))))

type-set-finish-1function

(defun type-set-finish-1
  (additive-const multiplicative-const
    stripped-term
    ts
    ttree
    type-alist)
  (cond ((null type-alist) (mv ts ttree))
    ((and (or (ts-subsetp (cadr (car type-alist)) *ts-integer*)
         (ts-subsetp (cadr (car type-alist)) *ts-ratio*))
       (normalize-linear-sum-p stripped-term
         (car (car type-alist)))) (let ((term-to-match (car (car type-alist))) (type-to-match (cadr (car type-alist)))
          (ttree-to-match (cddr (car type-alist))))
        (mv-let (typed-additive-const typed-multiplicative-const
            stripped-term-to-match)
          (normalize-linear-sum term-to-match)
          (cond ((and (equal stripped-term stripped-term-to-match)
               (not (eql typed-multiplicative-const 0))) (let* ((merged-multiplicative-const (* multiplicative-const (/ typed-multiplicative-const))) (merged-additive-const (- additive-const
                      (* merged-multiplicative-const typed-additive-const))))
                (cond ((and (not (eql merged-additive-const 0))
                     (not (eql merged-multiplicative-const 1))) (let* ((merged-multiplicative-const-ts (type-set-quote merged-multiplicative-const)) (merged-additive-const-ts (type-set-quote merged-additive-const))
                        (new-ts1 (aref2 'type-set-binary-*-table
                            *type-set-binary-*-table*
                            merged-multiplicative-const-ts
                            type-to-match))
                        (new-ts2 (aref2 'type-set-binary-+-table
                            *type-set-binary-+-table*
                            merged-additive-const-ts
                            new-ts1))
                        (new-ts3 (ts-intersection ts new-ts2)))
                      (if (or (ts-subsetp new-ts3 *ts-integer*)
                          (ts-subsetp new-ts3 *ts-ratio*))
                        (mv new-ts3 (puffert (cons-tag-trees ttree ttree-to-match)))
                        (type-set-finish-1 additive-const
                          multiplicative-const
                          stripped-term
                          ts
                          ttree
                          (cdr type-alist)))))
                  ((not (eql merged-additive-const 0)) (let* ((merged-additive-const-ts (type-set-quote merged-additive-const)) (new-ts1 (aref2 'type-set-binary-+-table
                            *type-set-binary-+-table*
                            merged-additive-const-ts
                            type-to-match))
                        (new-ts2 (ts-intersection ts new-ts1)))
                      (if (or (ts-subsetp new-ts2 *ts-integer*)
                          (ts-subsetp new-ts2 *ts-ratio*))
                        (mv new-ts2 (puffert (cons-tag-trees ttree ttree-to-match)))
                        (type-set-finish-1 additive-const
                          multiplicative-const
                          stripped-term
                          ts
                          ttree
                          (cdr type-alist)))))
                  ((not (eql merged-multiplicative-const 1)) (let* ((merged-multiplicative-const-ts (type-set-quote merged-multiplicative-const)) (new-ts1 (aref2 'type-set-binary-*-table
                            *type-set-binary-*-table*
                            merged-multiplicative-const-ts
                            type-to-match))
                        (new-ts2 (ts-intersection ts new-ts1)))
                      (if (or (ts-subsetp new-ts2 *ts-integer*)
                          (ts-subsetp new-ts2 *ts-ratio*))
                        (mv new-ts2 (puffert (cons-tag-trees ttree ttree-to-match)))
                        (type-set-finish-1 additive-const
                          multiplicative-const
                          stripped-term
                          ts
                          ttree
                          (cdr type-alist)))))
                  (t (type-set-finish-1 additive-const
                      multiplicative-const
                      stripped-term
                      ts
                      ttree
                      (cdr type-alist))))))
            (t (type-set-finish-1 additive-const
                multiplicative-const
                stripped-term
                ts
                ttree
                (cdr type-alist)))))))
    (t (type-set-finish-1 additive-const
        multiplicative-const
        stripped-term
        ts
        ttree
        (cdr type-alist)))))

type-set-finishfunction

(defun type-set-finish
  (x ts0 ttree0 ts1 ttree1 type-alist)
  (mv-let (ts ttree)
    (cond ((null ts0) (mv ts1 ttree1))
      ((ts-subsetp ts1 ts0) (mv ts1 ttree1))
      (t (mv (ts-intersection ts0 ts1)
          (cons-tag-trees ttree0 ttree1))))
    (cond ((and (ts-subsetp ts *ts-rational*)
         (ts-intersectp ts *ts-integer*)
         (ts-intersectp ts *ts-ratio*)) (mv-let (additive-const multiplicative-const stripped-term)
          (normalize-linear-sum x)
          (type-set-finish-1 additive-const
            multiplicative-const
            stripped-term
            ts
            ttree
            type-alist)))
      (t (mv ts ttree)))))

search-type-alist-recfunction

(defun search-type-alist-rec
  (term alt-term typ type-alist unify-subst ttree)
  (cond ((null type-alist) (mv nil unify-subst ttree nil))
    ((ts-subsetp (cadr (car type-alist)) typ) (mv-let (ans unify-subst)
        (one-way-unify1 term (car (car type-alist)) unify-subst)
        (cond (ans (mv t
              unify-subst
              (cons-tag-trees (cddr (car type-alist)) ttree)
              (cdr type-alist)))
          (alt-term (mv-let (ans unify-subst)
              (one-way-unify1 alt-term (car (car type-alist)) unify-subst)
              (cond (ans (mv t
                    unify-subst
                    (cons-tag-trees (cddr (car type-alist)) ttree)
                    (cdr type-alist)))
                (t (search-type-alist-rec term
                    alt-term
                    typ
                    (cdr type-alist)
                    unify-subst
                    ttree)))))
          (t (search-type-alist-rec term
              alt-term
              typ
              (cdr type-alist)
              unify-subst
              ttree)))))
    (t (search-type-alist-rec term
        alt-term
        typ
        (cdr type-alist)
        unify-subst
        ttree))))

free-varspmutual-recursion

(mutual-recursion (defun free-varsp
    (term alist)
    (cond ((variablep term) (not (assoc-eq term alist)))
      ((fquotep term) nil)
      (t (free-varsp-lst (fargs term) alist))))
  (defun free-varsp-lst
    (args alist)
    (cond ((null args) nil)
      (t (or (free-varsp (car args) alist)
          (free-varsp-lst (cdr args) alist))))))

search-type-alist-with-restfunction

(defun search-type-alist-with-rest
  (term typ type-alist unify-subst ttree wrld)
  (mv-let (term alt-term)
    (cond ((or (variablep term)
         (fquotep term)
         (not (equivalence-relationp (ffn-symb term) wrld))) (mv term nil))
      ((free-varsp term unify-subst) (mv term
          (fcons-term* (ffn-symb term) (fargn term 2) (fargn term 1))))
      (t (let ((arg1 (fargn term 1)) (arg2 (fargn term 2)))
          (cond ((term-order arg1 arg2) (mv (fcons-term* (ffn-symb term) (fargn term 2) (fargn term 1))
                nil))
            (t (mv term nil))))))
    (search-type-alist-rec term
      alt-term
      typ
      type-alist
      unify-subst
      ttree)))

search-type-alistfunction

(defun search-type-alist
  (term typ type-alist unify-subst ttree wrld)
  (mv-let (ans unify-subst ttree rest-type-alist)
    (search-type-alist-with-rest term
      typ
      type-alist
      unify-subst
      ttree
      wrld)
    (declare (ignore rest-type-alist))
    (mv ans unify-subst ttree)))

term-and-typ-to-lookupfunction

(defun term-and-typ-to-lookup
  (hyp wrld ens)
  (mv-let (not-flg term)
    (strip-not hyp)
    (let ((recog-tuple (and (nvariablep term)
           (not (fquotep term))
           (not (flambda-applicationp term))
           (most-recent-enabled-recog-tuple (ffn-symb term) wrld ens))))
      (cond ((and recog-tuple
           (access recognizer-tuple recog-tuple :strongp)) (mv (fargn term 1)
            (if not-flg
              (access recognizer-tuple recog-tuple :false-ts)
              (access recognizer-tuple recog-tuple :true-ts))
            (access recognizer-tuple recog-tuple :rune)))
        (t (mv term
            (if not-flg
              *ts-nil*
              *ts-non-nil*)
            nil))))))

lookup-hypfunction

(defun lookup-hyp
  (hyp type-alist wrld unify-subst ttree ens)
  (mv-let (term typ rune)
    (term-and-typ-to-lookup hyp wrld ens)
    (mv-let (ans unify-subst ttree)
      (search-type-alist term
        typ
        type-alist
        unify-subst
        ttree
        wrld)
      (mv ans
        unify-subst
        (if (and ans rune)
          (push-lemma rune ttree)
          ttree)))))

bind-free-vars-to-unbound-free-varsfunction

(defun bind-free-vars-to-unbound-free-vars
  (vars alist)
  (cond ((endp vars) alist)
    ((assoc-eq (car vars) alist) (bind-free-vars-to-unbound-free-vars (cdr vars) alist))
    (t (bind-free-vars-to-unbound-free-vars (cdr vars)
        (cons (cons (car vars) (packn (list 'unbound-free- (car vars))))
          alist)))))

x-xrunepother

(defabbrev x-xrunep
  (xrune)
  (or (eq (car xrune) :hyp) (eq (car xrune) :conc)))

hyp-xruneother

(defabbrev hyp-xrune
  (n rune)
  (assert$ (not (x-xrunep rune)) (list* :hyp rune n)))

hyp-xrune-runeother

(defabbrev hyp-xrune-rune
  (xrune)
  (assert$ (and (x-xrunep xrune) (eq (car xrune) :hyp))
    (cadr xrune)))

conc-xruneother

(defabbrev conc-xrune
  (rune)
  (assert$ (not (x-xrunep rune)) (list* :conc rune)))

conc-xrune-runeother

(defabbrev conc-xrune-rune
  (xrune)
  (assert$ (and (x-xrunep xrune) (eq (car xrune) :conc))
    (cdr xrune)))

xrune-runeother

(defabbrev xrune-rune
  (xrune)
  (cond ((x-xrunep xrune) (if (eq (car xrune) :hyp)
        (cadr xrune)
        (cdr xrune)))
    (t xrune)))

rune=other

(defabbrev rune=
  (rune1 rune2)
  (and (eq (car rune1) (car rune2))
    (equal (cdr rune1) (cdr rune2))))

xrune=other

(defabbrev xrune=
  (xrune1 xrune2)
  (cond ((eq (car xrune1) :hyp) (and (eq (car xrune2) :hyp)
        (rune= (cadr xrune1) (cadr xrune2))
        (eql (cddr xrune1) (cddr xrune2))))
    ((eq (car xrune1) :conc) (and (eq (car xrune2) :conc)
        (rune= (cdr xrune1) (cdr xrune2))))
    (t (rune= xrune1 xrune2))))

prettyify-xrunefunction

(defun prettyify-xrune
  (xrune)
  (cond ((eq (car xrune) :hyp) (list* :hyp (cddr xrune) (cadr xrune)))
    (t xrune)))

other

(defrec accp-info
  (((cnt-s . cnt-f) stack-s . stack-f) xrune-stack
    xrunep
    totals . old-accp-info)
  t)

other

(defrec accp-entry (xrune (n-s . ap-s) n-f . ap-f) t)

merge-accumulated-persistence-auxfunction

(defun merge-accumulated-persistence-aux
  (xrune entry alist)
  (cond ((endp alist) (list entry))
    ((xrune= xrune (access accp-entry (car alist) :xrune)) (cons (make accp-entry
          :xrune xrune
          :n-s (+ (access accp-entry entry :n-s)
            (access accp-entry (car alist) :n-s))
          :ap-s (+ (access accp-entry entry :ap-s)
            (access accp-entry (car alist) :ap-s))
          :n-f (+ (access accp-entry entry :n-f)
            (access accp-entry (car alist) :n-f))
          :ap-f (+ (access accp-entry entry :ap-f)
            (access accp-entry (car alist) :ap-f)))
        (cdr alist)))
    (t (cons (car alist)
        (merge-accumulated-persistence-aux xrune entry (cdr alist))))))

merge-accumulated-persistence-recfunction

(defun merge-accumulated-persistence-rec
  (new-alist old-alist)
  (cond ((endp new-alist) old-alist)
    (t (merge-accumulated-persistence-rec (cdr new-alist)
        (merge-accumulated-persistence-aux (access accp-entry (car new-alist) :xrune)
          (car new-alist)
          old-alist)))))

merge-accumulated-persistencefunction

(defun merge-accumulated-persistence
  (new-alist old-alist)
  (cond ((null old-alist) new-alist)
    (t (merge-accumulated-persistence-rec new-alist old-alist))))

add-accumulated-persistence-sfunction

(defun add-accumulated-persistence-s
  (xrune delta alist original-alist acc)
  (cond ((null alist) (cons (make accp-entry
          :xrune xrune
          :n-s 1
          :ap-s (or delta 0)
          :n-f 0
          :ap-f 0)
        original-alist))
    ((xrune= xrune (access accp-entry (car alist) :xrune)) (cons (cond (delta (change accp-entry
              (car alist)
              :ap-f 0
              :n-s (1+ (access accp-entry (car alist) :n-s))
              :ap-s (+ delta
                (access accp-entry (car alist) :ap-s)
                (access accp-entry (car alist) :ap-f))))
          (t (assert$ (and (int= (access accp-entry (car alist) :ap-s) 0)
                (int= (access accp-entry (car alist) :ap-f) 0))
              (change accp-entry
                (car alist)
                :ap-f 0
                :n-s (1+ (access accp-entry (car alist) :n-s))))))
        (revappend acc (cdr alist))))
    (t (add-accumulated-persistence-s xrune
        delta
        (cdr alist)
        original-alist
        (cons (car alist) acc)))))

add-accumulated-persistence-ffunction

(defun add-accumulated-persistence-f
  (xrune delta alist original-alist acc)
  (cond ((null alist) (cons (make accp-entry
          :xrune xrune
          :n-s 0
          :ap-s 0
          :n-f 1
          :ap-f (or delta 0))
        original-alist))
    ((xrune= xrune (access accp-entry (car alist) :xrune)) (assert$ (eql (access accp-entry (car alist) :ap-s) 0)
        (cons (cond (delta (change accp-entry
                (car alist)
                :n-f (1+ (access accp-entry (car alist) :n-f))
                :ap-f (+ delta (access accp-entry (car alist) :ap-f))))
            (t (assert$ (eql (access accp-entry (car alist) :ap-f) 0)
                (change accp-entry
                  (car alist)
                  :n-f (1+ (access accp-entry (car alist) :n-f))))))
          (revappend acc (cdr alist)))))
    (t (add-accumulated-persistence-f xrune
        delta
        (cdr alist)
        original-alist
        (cons (car alist) acc)))))

accumulated-persistence-make-failuresfunction

(defun accumulated-persistence-make-failures
  (alist)
  (cond ((null alist) nil)
    (t (cons (change accp-entry
          (car alist)
          :n-f (+ (access accp-entry (car alist) :n-f)
            (access accp-entry (car alist) :n-s))
          :n-s 0
          :ap-f (+ (access accp-entry (car alist) :ap-f)
            (access accp-entry (car alist) :ap-s))
          :ap-s 0)
        (accumulated-persistence-make-failures (cdr alist))))))

add-accumulated-persistencefunction

(defun add-accumulated-persistence
  (xrune success-p delta alist-stack)
  (assert$ (cdr alist-stack)
    (let* ((alist (if success-p
           (car alist-stack)
           (accumulated-persistence-make-failures (car alist-stack)))) (new-alist (cond ((fake-rune-for-anonymous-enabled-rule-p (xrune-rune xrune)) alist)
            (success-p (add-accumulated-persistence-s xrune delta alist alist nil))
            (t (add-accumulated-persistence-f xrune delta alist alist nil)))))
      (cons (merge-accumulated-persistence new-alist (cadr alist-stack))
        (cddr alist-stack)))))

accumulated-persistence-fnfunction

(defun accumulated-persistence-fn
  (flg state)
  (declare (ignorable state))
  (cond ((not (member flg '(t nil :all))) (er hard
        'accumulated-persistence
        "Unrecognized flg argument ~x0."
        flg))
    (t (wormhole-eval 'accumulated-persistence
        '(lambda (whs)
          (set-wormhole-data whs
            (if flg
              (make accp-info
                :cnt-s 0
                :cnt-f 0
                :stack-s nil
                :stack-f nil
                :xrunep (eq flg :all)
                :totals '(nil)
                :old-accp-info (let ((info (wormhole-data whs)))
                  (cond (info (change accp-info info :old-accp-info nil))
                    (t nil))))
              nil)))
        nil))))

accumulated-persistencemacro

(defmacro accumulated-persistence
  (flg)
  (declare (xargs :guard (member-equal flg '(t 't nil 'nil :all ':all))))
  `(accumulated-persistence-fn ,FLG state))

accumulated-persistence-oops-fnfunction

(defun accumulated-persistence-oops-fn
  nil
  (wormhole-eval 'accumulated-persistence
    '(lambda (whs)
      (let* ((info (wormhole-data whs)) (old (and info (access accp-info info :old-accp-info))))
        (cond (old (set-wormhole-data whs old))
          (t (prog2$ (cw "No change: Unable to apply ~
                              accumulated-persistence-oops.~|")
              whs)))))
    nil))

accumulated-persistence-oopsmacro

(defmacro accumulated-persistence-oops
  nil
  '(accumulated-persistence-oops-fn))

set-accumulated-persistencemacro

(defmacro set-accumulated-persistence
  (flg)
  `(accumulated-persistence ,FLG))

merge-car->function

(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))))))

merge-sort-car->function

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

*accp-major-separator*constant

(defconst *accp-major-separator*
  "   --------------------------------~%")

*accp-minor-separator*constant

(defconst *accp-minor-separator*
  "      .............................~%")

show-accumulated-persistence-phrase0function

(defun show-accumulated-persistence-phrase0
  (entry key)
  (let* ((xrune (access accp-entry entry :xrune)) (n-s (access accp-entry entry :n-s))
      (n-f (access accp-entry entry :n-f))
      (n (+ n-s n-f))
      (ap-s (access accp-entry entry :ap-s))
      (ap-f (access accp-entry entry :ap-f))
      (ap (+ ap-s ap-f)))
    (let ((main-msg (msg "~c0 ~c1 (~c2.~f3~f4) ~y5"
           (cons ap 10)
           (cons n 8)
           (cons (floor ap n) 5)
           (mod (floor (* 10 ap) n) 10)
           (mod (floor (* 100 ap) n) 10)
           (prettyify-xrune xrune))))
      (case key
        ((:useless :ratio-a :frames-a :tries-a) (list main-msg))
        (otherwise (list main-msg
            (msg "~c0 ~c1    [useful]~%" (cons ap-s 10) (cons n-s 8))
            (msg "~c0 ~c1    [useless]~%" (cons ap-f 10) (cons n-f 8))))))))

show-accumulated-persistence-phrase1function

(defun show-accumulated-persistence-phrase1
  (key alist mergep acc)
  (cond ((null alist) acc)
    (t (show-accumulated-persistence-phrase1 key
        (cdr alist)
        mergep
        (cons (cond ((and mergep
               (cdr alist)
               (equal (xrune-rune (access accp-entry (cdr (car (cdr alist))) :xrune))
                 (xrune-rune (access accp-entry (cdr (car alist)) :xrune)))) *accp-minor-separator*)
            (t *accp-major-separator*))
          (append (show-accumulated-persistence-phrase0 (cdr (car alist)) key)
            acc))))))

show-accumulated-persistence-remove-uselessfunction

(defun show-accumulated-persistence-remove-useless
  (alist acc)
  (cond ((null alist) (reverse acc))
    ((not (eql (access accp-entry (cdr (car alist)) :n-s) 0)) (show-accumulated-persistence-remove-useless (cdr alist)
        acc))
    (t (show-accumulated-persistence-remove-useless (cdr alist)
        (cons (car alist) acc)))))

show-accumulated-persistence-phrase-keyfunction

(defun show-accumulated-persistence-phrase-key
  (key entry lastcdr)
  (let* ((ap-s (access accp-entry entry :ap-s)) (ap-f (access accp-entry entry :ap-f))
      (ap (+ ap-s ap-f))
      (n-s (access accp-entry entry :n-s))
      (n-f (access accp-entry entry :n-f))
      (n (+ n-s n-f)))
    (case key
      ((:frames :frames-a) (list* ap ap-s n n-s lastcdr))
      (:frames-s (list* ap-s ap n-s n lastcdr))
      (:frames-f (list* ap-f ap n-f n lastcdr))
      ((:tries :tries-a) (list* n n-s ap ap-s lastcdr))
      (:tries-s (list* n-s n ap-s ap lastcdr))
      (:tries-f (list* n-f n ap-f ap lastcdr))
      (:useless (list* ap n lastcdr))
      (otherwise (list* (/ ap n) lastcdr)))))

show-accumulated-persistence-phrase2-mergefunction

(defun show-accumulated-persistence-phrase2-merge
  (key alist last-key-info)
  (cond ((null alist) nil)
    ((x-xrunep (access accp-entry (car alist) :xrune)) (cons (cons (append last-key-info
            (show-accumulated-persistence-phrase-key key
              (car alist)
              nil))
          (car alist))
        (show-accumulated-persistence-phrase2-merge key
          (cdr alist)
          last-key-info)))
    (t (let ((next-key-info (show-accumulated-persistence-phrase-key key
             (car alist)
             (list (access accp-entry (car alist) :xrune)))))
        (cons (cons (append next-key-info '(t)) (car alist))
          (show-accumulated-persistence-phrase2-merge key
            (cdr alist)
            next-key-info))))))

show-accumulated-persistence-phrase2-not-mergefunction

(defun show-accumulated-persistence-phrase2-not-merge
  (key alist)
  (cond ((null alist) nil)
    (t (cons (cons (show-accumulated-persistence-phrase-key key
            (car alist)
            nil)
          (car alist))
        (show-accumulated-persistence-phrase2-not-merge key
          (cdr alist))))))

show-accumulated-persistence-phrase2function

(defun show-accumulated-persistence-phrase2
  (key alist mergep)
  (cond (mergep (show-accumulated-persistence-phrase2-merge key alist nil))
    (t (show-accumulated-persistence-phrase2-not-merge key alist))))

split-xrune-alistfunction

(defun split-xrune-alist
  (alist rune-alist hyp-xrune-alist conc-xrune-alist)
  (cond ((endp alist) (mv rune-alist hyp-xrune-alist conc-xrune-alist))
    (t (let ((xrune (access accp-entry (car alist) :xrune)))
        (case (car xrune)
          (:hyp (split-xrune-alist (cdr alist)
              rune-alist
              (cons (car alist) hyp-xrune-alist)
              conc-xrune-alist))
          (:conc (split-xrune-alist (cdr alist)
              rune-alist
              hyp-xrune-alist
              (cons (car alist) conc-xrune-alist)))
          (t (split-xrune-alist (cdr alist)
              (cons (car alist) rune-alist)
              hyp-xrune-alist
              conc-xrune-alist)))))))

sort-xrune-alist-by-rune1function

(defun sort-xrune-alist-by-rune1
  (rune-alist hyp-xrune-alist conc-xrune-alist acc)
  (cond ((endp rune-alist) (assert$ (and (null hyp-xrune-alist) (null conc-xrune-alist))
        acc))
    ((and hyp-xrune-alist
       (equal (hyp-xrune-rune (caar hyp-xrune-alist))
         (caar rune-alist))) (sort-xrune-alist-by-rune1 rune-alist
        (cdr hyp-xrune-alist)
        conc-xrune-alist
        (cons (car hyp-xrune-alist) acc)))
    ((and conc-xrune-alist
       (equal (conc-xrune-rune (caar conc-xrune-alist))
         (caar rune-alist))) (sort-xrune-alist-by-rune1 rune-alist
        hyp-xrune-alist
        (cdr conc-xrune-alist)
        (cons (car conc-xrune-alist) acc)))
    (t (sort-xrune-alist-by-rune1 (cdr rune-alist)
        hyp-xrune-alist
        conc-xrune-alist
        (cons (car rune-alist) acc)))))

sort-xrune-alist-by-runefunction

(defun sort-xrune-alist-by-rune
  (alist display)
  (cond ((not (member-eq display '(nil :merge))) alist)
    (t (mv-let (rune-alist hyp-xrune-alist conc-xrune-alist)
        (split-xrune-alist alist nil nil nil)
        (cond ((eq display nil) rune-alist)
          (t (sort-xrune-alist-by-rune1 (merge-sort-lexorder rune-alist)
              (merge-sort-lexorder hyp-xrune-alist)
              (merge-sort-lexorder conc-xrune-alist)
              nil)))))))

pop-accp-fnfunction

(defun pop-accp-fn
  (info success-p)
  (let* ((xrune-stack (access accp-info info :xrune-stack)) (xrune (car xrune-stack))
      (xp (x-xrunep xrune))
      (new-cnt (and (not xp)
          (cond (success-p (if (fake-rune-for-anonymous-enabled-rule-p xrune)
                (access accp-info info :cnt-s)
                (1+ (access accp-info info :cnt-s))))
            (t (if (fake-rune-for-anonymous-enabled-rule-p xrune)
                (access accp-info info :cnt-f)
                (1+ (access accp-info info :cnt-f)))))))
      (top-level-p (not (member-equal xrune (cdr xrune-stack)))))
    (cond (xp (change accp-info
          info
          :stack-s (cdr (access accp-info info :stack-s))
          :stack-f (cdr (access accp-info info :stack-f))
          :xrune-stack (cdr xrune-stack)
          :totals (add-accumulated-persistence xrune
            success-p
            (and top-level-p
              (+ (- (access accp-info info :cnt-s)
                  (car (access accp-info info :stack-s)))
                (- (access accp-info info :cnt-f)
                  (car (access accp-info info :stack-f)))))
            (access accp-info info :totals))))
      (success-p (change accp-info
          info
          :cnt-s new-cnt
          :stack-s (cdr (access accp-info info :stack-s))
          :stack-f (cdr (access accp-info info :stack-f))
          :xrune-stack (cdr xrune-stack)
          :totals (add-accumulated-persistence xrune
            success-p
            (and top-level-p
              (+ (- new-cnt (car (access accp-info info :stack-s)))
                (- (access accp-info info :cnt-f)
                  (car (access accp-info info :stack-f)))))
            (access accp-info info :totals))))
      (t (change accp-info
          info
          :cnt-f new-cnt
          :stack-s (cdr (access accp-info info :stack-s))
          :stack-f (cdr (access accp-info info :stack-f))
          :xrune-stack (cdr xrune-stack)
          :totals (add-accumulated-persistence xrune
            success-p
            (and top-level-p
              (+ (- (access accp-info info :cnt-s)
                  (car (access accp-info info :stack-s)))
                (- new-cnt (car (access accp-info info :stack-f)))))
            (access accp-info info :totals)))))))

pop-accp-fn-iteratefunction

(defun pop-accp-fn-iterate
  (info n)
  (if (zp n)
    info
    (pop-accp-fn-iterate (pop-accp-fn info t) (1- n))))

show-accumulated-persistence-listfunction

(defun show-accumulated-persistence-list
  (alist acc)
  (cond ((endp alist) acc)
    (t (let* ((entry (cdar alist)) (xrune (access accp-entry entry :xrune))
          (n-s (access accp-entry entry :n-s))
          (n-f (access accp-entry entry :n-f))
          (n (+ n-s n-f))
          (ap-s (access accp-entry entry :ap-s))
          (ap-f (access accp-entry entry :ap-f))
          (ap (+ ap-s ap-f)))
        (show-accumulated-persistence-list (cdr alist)
          (cons (list ap n (prettyify-xrune xrune)) acc))))))

show-accumulated-persistence-phrasefunction

(defun show-accumulated-persistence-phrase
  (key/display accp-info)
  (let* ((key (car key/display)) (display (cdr key/display))
      (xrune-stack (access accp-info accp-info :xrune-stack))
      (accp-info (cond ((and xrune-stack (member-eq key '(:frames-a :tries-a))) (pop-accp-fn-iterate accp-info (length xrune-stack)))
          (t accp-info)))
      (totals (access accp-info accp-info :totals)))
    (cond ((null totals) (msg "There is no accumulated persistence to show.  Evaluate ~x0 to ~
            activate gathering of accumulated-persistence statistics.~|"
          '(accumulated-persistence t)))
      ((eq key :runes) (msg "~x0"
          (merge-sort-lexorder (strip-cars (car (last totals))))))
      (t (let* ((mergep (eq display :merge)) (alist (merge-sort-lexorder (show-accumulated-persistence-phrase2 key
                  (sort-xrune-alist-by-rune (car (last totals)) display)
                  mergep)))
            (alist (if (eq key :useless)
                (show-accumulated-persistence-remove-useless alist nil)
                alist))
            (header-for-results (if (eq display :list)
                "List of entries (:frames :tries rune):~|"
                "   :frames   :tries    :ratio  rune"))
            (msg-for-results (if (eq display :list)
                (msg "~|~x0~|"
                  (show-accumulated-persistence-list alist nil))
                (msg "~*0~@1"
                  (list ""
                    "~@*"
                    "~@*"
                    "~@*"
                    (show-accumulated-persistence-phrase1 key alist mergep nil))
                  *accp-major-separator*))))
          (cond ((null (cdr totals)) (msg "Accumulated Persistence~@0~|~%~@1~%~@2"
                (if xrune-stack
                  ""
                  (msg " (~x0 :tries useful, ~x1 :tries not useful)"
                    (access accp-info accp-info :cnt-s)
                    (access accp-info accp-info :cnt-f)))
                header-for-results
                msg-for-results))
            (t (msg "Accumulated Persistence~|~%~
                       ***************************************~|~
                       *** NOTE: INCOMPLETE!!!~|~
                       *** ~x0 rule attempts are not considered below.~|~
                       *** Use :frames-a or :tries-a to get more complete ~
                           totals.~|~
                       ***************************************~|~
                       ~%~@1~%~@2"
                (- (+ (access accp-info accp-info :cnt-s)
                    (access accp-info accp-info :cnt-f)
                    (length xrune-stack))
                  (+ (car (last (access accp-info accp-info :stack-s)))
                    (car (last (access accp-info accp-info :stack-f)))))
                header-for-results
                msg-for-results))))))))

show-accumulated-persistence-fnfunction

(defun show-accumulated-persistence-fn
  (sortkey display)
  (cond ((not (member-eq sortkey
         '(:ratio :frames :frames-s :frames-f :frames-a :tries :tries-s :tries-f :tries-a :useless :runes))) (er hard
        'show-accumulated-persistence
        "Unrecognized sortkey argument ~x0."
        sortkey))
    ((not (member-eq display '(t nil :raw :merge :list))) (er hard
        'show-accumulated-persistence
        "Unrecognized display argument ~x0."
        display))
    (t (wormhole 'accumulated-persistence
        '(lambda (whs) (set-wormhole-entry-code whs :enter))
        (cons sortkey display)
        '(state-global-let* ((print-base 10 set-print-base) (print-radix nil set-print-radix))
          (pprogn (io? temporary
              nil
              state
              nil
              (fms "~@0"
                (list (cons #\0
                    (show-accumulated-persistence-phrase (f-get-global 'wormhole-input state)
                      (wormhole-data (f-get-global 'wormhole-status state)))))
                *standard-co*
                state
                nil))
            (value :q)))
        :ld-prompt nil
        :ld-missing-input-ok nil
        :ld-pre-eval-filter :all :ld-pre-eval-print nil
        :ld-post-eval-print :command-conventions :ld-evisc-tuple nil
        :ld-error-triples t
        :ld-error-action :error :ld-query-control-alist nil
        :ld-verbose nil))))

show-accumulated-persistencemacro

(defmacro show-accumulated-persistence
  (&optional (sortkey ':frames) (display 't))
  (declare (xargs :guard (and (member-eq sortkey
          '(:ratio :frames :frames-s :frames-f :frames-a :tries :tries-s :tries-f :tries-a :useless :runes))
        (member-eq display '(t nil :raw :merge :list)))))
  (show-accumulated-persistence-fn sortkey display))

push-accp-fnfunction

(defun push-accp-fn
  (rune x-info info)
  (let ((xrune (cond ((natp x-info) (hyp-xrune x-info rune))
         ((eq x-info :conc) (conc-xrune rune))
         ((null x-info) rune)
         (t (er hard
             'push-accp
             "Implementation error: Bad value of x-info, ~x0."
             x-info)))))
    (change accp-info
      info
      :xrune-stack (cons xrune (access accp-info info :xrune-stack))
      :stack-s (cons (access accp-info info :cnt-s)
        (access accp-info info :stack-s))
      :stack-f (cons (access accp-info info :cnt-f)
        (access accp-info info :stack-f))
      :totals (cons nil (access accp-info info :totals)))))

push-accpfunction

(defun push-accp
  (rune x-info)
  (wormhole-eval 'accumulated-persistence
    '(lambda (whs)
      (let ((info (wormhole-data whs)))
        (cond ((null info) whs)
          ((or (null x-info) (access accp-info info :xrunep)) (set-wormhole-data whs (push-accp-fn rune x-info info)))
          (t whs))))
    (cons :no-wormhole-lock rune)))

pop-accpfunction

(defun pop-accp
  (success-p x-info)
  (wormhole-eval 'accumulated-persistence
    '(lambda (whs)
      (let ((info (wormhole-data whs)))
        (cond ((null info) whs)
          ((or (null x-info) (access accp-info info :xrunep)) (set-wormhole-data whs (pop-accp-fn info success-p)))
          (t whs))))
    (cons :no-wormhole-lock success-p)))

with-accumulated-persistencemacro

(defmacro with-accumulated-persistence
  (rune vars
    success-p
    body
    &optional
    x-info
    (condition 'nil condition-p))
  (flet ((fix-var (var)
       (if (consp var)
         (caddr var)
         var)) (fix-var-declares (var)
        (and (consp var)
          `((declare (type ,(CADR VAR) ,(CADDR VAR)))))))
    (flet ((fix-vars (vars)
         (if (consp vars)
           (cons (fix-var (car vars)) (cdr vars))
           vars)))
      (let ((form `(prog2$ (push-accp ,RUNE ,X-INFO)
             ,(COND
  ((AND (TRUE-LISTP VARS) (= (LENGTH VARS) 1))
   `(LET ((,(FIX-VAR (CAR VARS)) ,BODY))
      ,@(FIX-VAR-DECLARES (CAR VARS))
      (PROG2$ (POP-ACCP ,SUCCESS-P ,X-INFO) ,(FIX-VAR (CAR VARS)))))
  (T
   `(MV-LET ,(FIX-VARS VARS) ,BODY ,@(FIX-VAR-DECLARES (CAR VARS))
            (PROG2$ (POP-ACCP ,SUCCESS-P ,X-INFO) (MV ,@(FIX-VARS VARS)))))))))
        (cond (condition-p `(cond (,CONDITION ,FORM) (t ,BODY)))
          (t form))))))

assume-true-false-<function

(defun assume-true-false-<
  (not-flg arg1 arg2 ts1 ts2 type-alist ttree xttree w)
  (cond ((not not-flg) (let ((strongp (and (or (ts-subsetp ts1 *ts-positive-integer*)
               (and (quotep arg1)
                 (rationalp (unquote arg1))
                 (<= 1 (unquote arg1))))
             (ts-intersectp ts2 *ts-one*))))
        (cond (strongp (extend-type-alist arg2
              (ts-intersection ts2
                (ts-complement *ts-one*)
                (ts-union *ts-positive-rational* *ts-complex-rational*))
              (cons-tag-trees ttree xttree)
              type-alist
              w))
          ((and (ts-subsetp ts1
               (ts-union *ts-non-negative-rational*
                 (ts-complement *ts-acl2-number*)))
             (ts-intersectp ts2
               (ts-complement (ts-union *ts-positive-rational* *ts-complex-rational*)))) (extend-type-alist arg2
              (ts-intersection ts2
                (ts-union *ts-positive-rational* *ts-complex-rational*))
              (cons-tag-trees ttree xttree)
              type-alist
              w))
          ((and (ts-subsetp ts2
               (ts-union *ts-non-positive-rational*
                 (ts-complement *ts-acl2-number*)))
             (ts-intersectp ts1
               (ts-complement (ts-union *ts-negative-rational* *ts-complex-rational*)))) (extend-type-alist arg1
              (ts-intersection ts1
                (ts-union *ts-negative-rational* *ts-complex-rational*))
              (cons-tag-trees ttree xttree)
              type-alist
              w))
          (t type-alist))))
    ((and (ts-subsetp ts1 *ts-negative-rational*)
       (ts-intersectp ts2
         (ts-complement (ts-union *ts-complex-rational* *ts-negative-rational*)))) (extend-type-alist arg2
        (ts-intersection ts2
          (ts-union *ts-complex-rational* *ts-negative-rational*))
        (cons-tag-trees ttree xttree)
        type-alist
        w))
    ((and (ts-subsetp ts1
         (ts-union *ts-non-positive-rational*
           (ts-complement *ts-acl2-number*)))
       (ts-intersectp ts2 *ts-positive-rational*)) (extend-type-alist arg2
        (ts-intersection ts2 (ts-complement *ts-positive-rational*))
        (cons-tag-trees ttree xttree)
        type-alist
        w))
    ((and (ts-subsetp ts2 *ts-positive-rational*)
       (ts-intersectp ts1
         (ts-complement (ts-union *ts-complex-rational* *ts-positive-rational*)))) (extend-type-alist arg1
        (ts-intersection ts1
          (ts-union *ts-complex-rational* *ts-positive-rational*))
        (cons-tag-trees ttree xttree)
        type-alist
        w))
    ((and (ts-subsetp ts2
         (ts-complement (ts-union *ts-complex-rational* *ts-negative-rational*)))
       (ts-intersectp ts1 *ts-negative-rational*)) (extend-type-alist arg1
        (ts-intersection ts1 (ts-complement *ts-negative-rational*))
        (cons-tag-trees ttree xttree)
        type-alist
        w))
    (t type-alist)))

mv-atf-2function

(defun mv-atf-2
  (not-flg true-type-alist
    false-type-alist
    new-term
    xnot-flg
    x
    shared-ttree
    xttree
    ignore)
  (let ((tta0 (and (not (eq ignore :tta))
         (extend-type-alist-simple new-term
           *ts-t*
           shared-ttree
           true-type-alist))) (fta0 (and (not (eq ignore :fta))
          (extend-type-alist-simple new-term
            *ts-nil*
            shared-ttree
            false-type-alist)))
      (same-parity (eq not-flg xnot-flg)))
    (cond ((equal new-term
         (cond (same-parity x) (t (dumb-negate-lit x)))) (mv-atf not-flg nil nil tta0 fta0 nil nil))
      (t (let ((tta1 (extend-type-alist-simple x
               (if same-parity
                 *ts-t*
                 *ts-nil*)
               xttree
               tta0)) (fta1 (extend-type-alist-simple x
                (if same-parity
                  *ts-nil*
                  *ts-t*)
                xttree
                fta0)))
          (mv-atf not-flg nil nil tta1 fta1 nil nil))))))

binding-hyp-pfunction

(defun binding-hyp-p
  (hyp alist wrld)
  (let* ((forcep (and (nvariablep hyp)
         (not (fquotep hyp))
         (or (eq (ffn-symb hyp) 'force)
           (eq (ffn-symb hyp) 'case-split)))) (hyp (if forcep
          (fargn hyp 1)
          hyp))
      (eqp (equalityp hyp)))
    (mv forcep
      (cond (eqp (and (variablep (fargn hyp 1))
            (not (assoc-eq (fargn hyp 1) alist))
            (not (free-varsp (fargn hyp 2) alist))))
        (t (and (nvariablep hyp)
            (not (fquotep hyp))
            (fargs hyp)
            (variablep (fargn hyp 1))
            (equivalence-relationp (ffn-symb hyp) wrld)
            (let ((arg2 (fargn hyp 2)))
              (and (not (assoc-eq (fargn hyp 1) alist))
                (ffn-symb-p arg2 'double-rewrite)
                (not (free-varsp arg2 alist))))))))))

adjust-ignore-for-atfmacro

(defmacro adjust-ignore-for-atf
  (not-flg ignore)
  `(cond ((and ,NOT-FLG (eq ,IGNORE :fta)) :tta)
    ((and ,NOT-FLG (eq ,IGNORE :tta)) :fta)
    (t ,IGNORE)))

backchain-limit-reachedp1function

(defun backchain-limit-reachedp1
  (n ancestors)
  (cond ((int= n 0) t)
    ((null ancestors) nil)
    (t (backchain-limit-reachedp1 (1- n) (cdr ancestors)))))

backchain-limit-reachedpfunction

(defun backchain-limit-reachedp
  (n ancestors)
  (and n (backchain-limit-reachedp1 n ancestors)))

new-backchain-limitfunction

(defun new-backchain-limit
  (new-offset old-limit ancestors)
  (cond ((null new-offset) old-limit)
    ((null old-limit) (+ (length ancestors) new-offset))
    (t (min (+ (length ancestors) new-offset) old-limit))))

other

(defproxy oncep-tp (* *) => *)

oncep-tp-builtinfunction

(defun oncep-tp-builtin
  (rune wrld)
  (declare (ignore rune wrld)
    (xargs :mode :logic :guard t))
  nil)

other

(defattach (oncep-tp oncep-tp-builtin) :skip-checks t)

strengthen-recog-callfunction

(defun strengthen-recog-call
  (x)
  (let ((arg (fargn x 1)))
    (case (ffn-symb x)
      (integerp (cond ((ffn-symb-p arg 'binary-+) (cond ((and (quotep (fargn arg 1))
                 (integerp (unquote (fargn arg 1)))) (mv (ts-complement *ts-acl2-number*) (fargn arg 2)))
              (t (mv nil arg))))
          (t (mv nil arg))))
      (rationalp (cond ((ffn-symb-p arg 'binary-+) (cond ((and (quotep (fargn arg 1))
                 (rationalp (unquote (fargn arg 1)))) (mv (ts-complement *ts-acl2-number*) (fargn arg 2)))
              (t (mv nil arg))))
          ((ffn-symb-p arg 'binary-*) (cond ((and (quotep (fargn arg 1))
                 (rationalp (unquote (fargn arg 1)))
                 (not (eql 0 (unquote (fargn arg 1))))) (mv (ts-complement *ts-acl2-number*) (fargn arg 2)))
              (t (mv nil arg))))
          (t (mv nil arg))))
      (otherwise (mv nil arg)))))

push-lemma?function

(defun push-lemma?
  (rune ttree)
  (if rune
    (push-lemma rune ttree)
    ttree))

other

(defstub use-enhanced-recognizer nil t)

other

(defattach use-enhanced-recognizer
  constant-t-function-arity-0)

strong-recognizer-expr-pfunction

(defun strong-recognizer-expr-p
  (var x ens w)
  (cond ((ffn-symb-p x 'if) (mv-let (var test-true-ts test-false-ts test-runes)
        (strong-recognizer-expr-p var (fargn x 1) ens w)
        (cond (var (mv-let (var tbr-true-ts tbr-false-ts tbr-runes)
              (strong-recognizer-expr-p (and (not (eq var :empty)) var)
                (fargn x 2)
                ens
                w)
              (cond (var (mv-let (var fbr-true-ts fbr-false-ts fbr-runes)
                    (strong-recognizer-expr-p (and (not (eq var :empty)) var)
                      (fargn x 3)
                      ens
                      w)
                    (cond (var (mv var
                          (ts-union (ts-intersection test-true-ts tbr-true-ts)
                            (ts-intersection test-false-ts fbr-true-ts))
                          (ts-union (ts-intersection test-true-ts tbr-false-ts)
                            (ts-intersection test-false-ts fbr-false-ts))
                          (union-equal test-runes (union-equal tbr-runes fbr-runes))))
                      (t (mv nil nil nil nil)))))
                (t (mv nil nil nil nil)))))
          (t (mv nil nil nil nil)))))
    ((variablep x) (mv nil nil nil nil))
    ((equal x *t*) (mv (or var :empty) *ts-unknown* *ts-empty* nil))
    ((equal x *nil*) (mv (or var :empty) *ts-empty* *ts-unknown* nil))
    ((fquotep x) (mv nil nil nil nil))
    ((flambda-applicationp x) (mv nil nil nil nil))
    ((eq (ffn-symb x) 'not) (mv-let (var not-true-ts not-false-ts runes)
        (strong-recognizer-expr-p var (fargn x 1) ens w)
        (mv var
          not-false-ts
          not-true-ts
          (if (and var (not (eq var :empty)))
            (add-to-set-equal '(:definition not) runes)
            runes))))
    ((and (fargs x)
       (not (cdr (fargs x)))
       (or (eq var nil) (eq var :empty) (equal var (fargn x 1)))) (let ((r (most-recent-enabled-recog-tuple (ffn-symb x) w ens)))
        (cond ((and r (access recognizer-tuple r :strongp)) (mv (fargn x 1)
              (access recognizer-tuple r :true-ts)
              (access recognizer-tuple r :false-ts)
              (list (access recognizer-tuple r :rune))))
          (t (mv nil nil nil nil)))))
    ((and (eq (ffn-symb x) 'equal) (use-enhanced-recognizer)) (mv-let (arg evg)
        (cond ((quotep (fargn x 1)) (mv (fargn x 2) (unquote (fargn x 1))))
          ((quotep (fargn x 2)) (mv (fargn x 1) (unquote (fargn x 2))))
          (t (mv nil nil)))
        (cond ((or (null arg)
             (not (or (eq var nil) (eq var :empty) (equal var arg)))) (mv nil nil nil nil))
          (t (let ((ts (case evg
                   ((t) *ts-t*)
                   ((nil) *ts-nil*)
                   (0 *ts-zero*)
                   (1 *ts-one*)
                   (otherwise nil))))
              (cond ((null ts) (mv nil nil nil nil))
                (t (mv arg
                    ts
                    (ts-complement ts)
                    (list *fake-rune-for-anonymous-enabled-rule*)))))))))
    (t (mv nil nil nil nil))))

recognizer-expr-pfunction

(defun recognizer-expr-p
  (x ens w)
  (cond ((eq (ffn-symb x) 'if) (mv-let (var true-ts false-ts runes)
        (strong-recognizer-expr-p nil x ens w)
        (cond ((and var (not (eq var :empty))) (assert$ (ts= false-ts (ts-complement true-ts))
              (mv var t true-ts false-ts runes)))
          (t (mv nil nil nil nil nil)))))
    ((and (fargs x) (not (cdr (fargs x)))) (let ((r (most-recent-enabled-recog-tuple (ffn-symb x) w ens)))
        (cond (r (mv :one (access recognizer-tuple r :strongp)
              (access recognizer-tuple r :true-ts)
              (access recognizer-tuple r :false-ts)
              (access recognizer-tuple r :rune)))
          (t (mv nil nil nil nil nil)))))
    (t (mv nil nil nil nil nil))))

|PUSH-LEMMA[S]|function

(defun |PUSH-LEMMA[S]|
  (flg |RUNE[S]| ttree)
  (cond ((eq flg :one) (push-lemma |RUNE[S]| ttree))
    (t (let ((pair (assoc-eq 'lemma ttree)) (runes (if (member-equal *fake-rune-for-anonymous-enabled-rule*
                |RUNE[S]|)
              (remove1-equal *fake-rune-for-anonymous-enabled-rule*
                |RUNE[S]|)
              |RUNE[S]|)))
        (cond (pair (acons 'lemma
              (union-equal runes (cdr pair))
              (remove-tag-from-tag-tree! 'lemma ttree)))
          (t (acons 'lemma runes ttree)))))))

type-set-recmutual-recursion

(mutual-recursion (defun type-set-rec
    (x force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      ttree
      pot-lst
      pt
      backchain-limit)
    (mv-let (ts0 ttree0)
      (cond ((and (consp dwp) (eq (car dwp) :skip-lookup)) (mv (cadr dwp) (cddr dwp)))
        (t (assoc-type-alist x type-alist w)))
      (cond ((and ts0
           (or (not dwp)
             (and (consp dwp)
               (not (eq (car dwp) :skip-lookup))
               (or (ts-disjointp ts0 (access recognizer-tuple dwp :true-ts))
                 (ts-disjointp ts0 (access recognizer-tuple dwp :false-ts)))))) (mv ts0 (cons-tag-trees ttree ttree0)))
        ((variablep x) (type-set-finish x ts0 ttree0 *ts-unknown* ttree type-alist))
        ((fquotep x) (type-set-finish x
            ts0
            ttree0
            (type-set-quote (cadr x))
            ttree
            type-alist))
        ((flambda-applicationp x) (mv-let (ts1 ttree1)
            (type-set-rec (lambda-body (ffn-symb x))
              nil
              nil
              (zip-variable-type-alist (lambda-formals (ffn-symb x))
                (type-set-lst (fargs x)
                  force-flg
                  nil
                  type-alist
                  ancestors
                  ens
                  w
                  pot-lst
                  pt
                  backchain-limit))
              t
              ens
              w
              ttree
              nil
              pt
              backchain-limit)
            (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist)))
        ((eq (ffn-symb x) 'not) (mv-let (ts1 ttree1)
            (type-set-rec (fargn x 1)
              force-flg
              nil
              type-alist
              ancestors
              ens
              w
              ttree
              pot-lst
              pt
              backchain-limit)
            (mv-let (ts1 ttree1)
              (type-set-not ts1 ttree1 ttree)
              (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist))))
        (t (let* ((fn (ffn-symb x)) (recog-tuple (most-recent-enabled-recog-tuple fn w ens))
              (dwp (if (and (consp dwp) (eq (car dwp) :skip-lookup))
                  nil
                  dwp)))
            (cond (recog-tuple (mv-let (ts1 ttree1)
                  (type-set-rec (fargn x 1)
                    force-flg
                    (and (or force-flg dwp) recog-tuple)
                    type-alist
                    ancestors
                    ens
                    w
                    ttree
                    pot-lst
                    pt
                    backchain-limit)
                  (mv-let (ts1 ttree1)
                    (type-set-recognizer recog-tuple ts1 ttree1 ttree)
                    (mv-let (ts ttree)
                      (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist)
                      (cond ((or (ts= ts *ts-t*) (ts= ts *ts-nil*)) (mv ts ttree))
                        (t (mv-let (ts2 ttree2 extended-p)
                            (type-set-with-rules (getpropc fn 'type-prescriptions nil w)
                              x
                              force-flg
                              dwp
                              type-alist
                              ancestors
                              ens
                              w
                              *ts-unknown*
                              ttree
                              pot-lst
                              pt
                              backchain-limit
                              nil)
                            (declare (ignore extended-p))
                            (mv (ts-intersection ts ts2) ttree2))))))))
              ((eq fn 'if) (mv-let (ts1 ttree1)
                  (mv-let (must-be-true must-be-false
                      true-type-alist
                      false-type-alist
                      ttree1)
                    (assume-true-false-rec (fargn x 1)
                      nil
                      force-flg
                      nil
                      type-alist
                      ancestors
                      ens
                      w
                      pot-lst
                      pt
                      nil
                      backchain-limit)
                    (cond (must-be-true (cond (must-be-false (mv *ts-empty* (cons-tag-trees ttree1 ttree)))
                          (t (type-set-rec (fargn x 2)
                              force-flg
                              nil
                              true-type-alist
                              ancestors
                              ens
                              w
                              (cons-tag-trees ttree1 ttree)
                              pot-lst
                              pt
                              backchain-limit))))
                      (must-be-false (type-set-rec (fargn x 3)
                          force-flg
                          nil
                          false-type-alist
                          ancestors
                          ens
                          w
                          (cons-tag-trees ttree1 ttree)
                          pot-lst
                          pt
                          backchain-limit))
                      (t (mv-let (ts1 ttree)
                          (type-set-rec (fargn x 2)
                            force-flg
                            nil
                            true-type-alist
                            ancestors
                            ens
                            w
                            ttree
                            pot-lst
                            pt
                            backchain-limit)
                          (mv-let (ts2 ttree)
                            (type-set-rec (fargn x 3)
                              force-flg
                              nil
                              false-type-alist
                              ancestors
                              ens
                              w
                              ttree
                              pot-lst
                              pt
                              backchain-limit)
                            (mv (ts-union ts1 ts2) ttree))))))
                  (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist)))
              ((member-eq fn *expandable-boot-strap-non-rec-fns*) (mv-let (ts1 ttree1)
                  (type-set-rec (subcor-var (formals fn w) (fargs x) (bbody fn))
                    force-flg
                    nil
                    type-alist
                    ancestors
                    ens
                    w
                    ttree
                    pot-lst
                    pt
                    backchain-limit)
                  (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist)))
              (t (mv-let (ts1 ttree1 extended-p)
                  (type-set-with-rules (getpropc fn 'type-prescriptions nil w)
                    x
                    force-flg
                    dwp
                    type-alist
                    ancestors
                    ens
                    w
                    *ts-unknown*
                    ttree
                    pot-lst
                    pt
                    backchain-limit
                    nil)
                  (declare (ignore extended-p))
                  (type-set-finish x ts0 ttree0 ts1 ttree1 type-alist)))))))))
  (defun type-set-lst
    (x force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      pot-lst
      pt
      backchain-limit)
    (cond ((null x) nil)
      (t (mv-let (ts ttree)
          (type-set-rec (car x)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            nil
            pot-lst
            pt
            backchain-limit)
          (cons (cons ts ttree)
            (type-set-lst (cdr x)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              pot-lst
              pt
              backchain-limit))))))
  (defun type-set-relieve-hyps-free
    (term typ
      rest-type-alist
      rune
      target
      hyps
      backchain-limit-lst
      force-flg
      dwp
      alist
      type-alist
      ancestors
      ens
      wrld
      ttree
      ttree0
      pot-lst
      pt
      backchain-limit
      bkptr+1)
    (assert$ rest-type-alist
      (mv-let (lookup-hyp-ans alist+ ttree rest-type-alist)
        (search-type-alist-with-rest term
          typ
          rest-type-alist
          alist
          ttree
          wrld)
        (cond ((null lookup-hyp-ans) (mv nil type-alist ttree0))
          ((null rest-type-alist) (type-set-relieve-hyps rune
              target
              (cdr hyps)
              (cdr backchain-limit-lst)
              force-flg
              dwp
              alist+
              type-alist
              ancestors
              ens
              wrld
              ttree
              ttree0
              pot-lst
              pt
              backchain-limit
              bkptr+1))
          (t (mv-let (relieve-hyps-ans type-alist ttree)
              (type-set-relieve-hyps rune
                target
                (cdr hyps)
                (cdr backchain-limit-lst)
                force-flg
                dwp
                alist+
                type-alist
                ancestors
                ens
                wrld
                ttree
                ttree0
                pot-lst
                pt
                backchain-limit
                bkptr+1)
              (cond (relieve-hyps-ans (mv relieve-hyps-ans type-alist ttree))
                (t (type-set-relieve-hyps-free term
                    typ
                    rest-type-alist
                    rune
                    target
                    hyps
                    backchain-limit-lst
                    force-flg
                    dwp
                    alist
                    type-alist
                    ancestors
                    ens
                    wrld
                    ttree
                    ttree0
                    pot-lst
                    pt
                    backchain-limit
                    bkptr+1)))))))))
  (defun type-set-relieve-hyps1
    (hyp forcep
      rune
      target
      hyps
      backchain-limit-lst
      force-flg
      dwp
      alist
      type-alist
      ancestors
      ens
      wrld
      ttree
      ttree0
      pot-lst
      pt
      backchain-limit
      bkptr)
    (mv-let (not-flg atm)
      (strip-not hyp)
      (mv-let (atm1 quotep-atm1 ttree)
        (sublis-var! alist atm ens wrld ttree)
        (cond (quotep-atm1 (cond ((eq not-flg (equal atm1 *nil*)) (type-set-relieve-hyps rune
                  target
                  (cdr hyps)
                  (cdr backchain-limit-lst)
                  force-flg
                  dwp
                  alist
                  type-alist
                  ancestors
                  ens
                  wrld
                  ttree
                  ttree0
                  pot-lst
                  pt
                  backchain-limit
                  (1+ bkptr)))
              (t (mv nil type-alist ttree0))))
          (t (mv-let (on-ancestorsp assumed-true)
              (if (eq ancestors t)
                (mv t nil)
                (ancestors-check (if not-flg
                    (mcons-term* 'not atm1)
                    atm1)
                  ancestors
                  (list rune)))
              (cond (on-ancestorsp (cond (assumed-true (type-set-relieve-hyps rune
                        target
                        (cdr hyps)
                        (cdr backchain-limit-lst)
                        force-flg
                        dwp
                        alist
                        type-alist
                        ancestors
                        ens
                        wrld
                        ttree
                        ttree0
                        pot-lst
                        pt
                        backchain-limit
                        (1+ bkptr)))
                    (t (mv nil type-alist ttree0))))
                ((backchain-limit-reachedp backchain-limit ancestors) (mv-let (force-flg ttree)
                    (cond ((not (and force-flg forcep)) (mv nil ttree))
                      (t (force-assumption rune
                          target
                          (if not-flg
                            (mcons-term* 'not atm1)
                            atm1)
                          type-alist
                          nil
                          (immediate-forcep (ffn-symb (car hyps)) ens)
                          force-flg
                          ttree)))
                    (cond (force-flg (type-set-relieve-hyps rune
                          target
                          (cdr hyps)
                          (cdr backchain-limit-lst)
                          force-flg
                          dwp
                          alist
                          type-alist
                          ancestors
                          ens
                          wrld
                          ttree
                          ttree0
                          pot-lst
                          pt
                          backchain-limit
                          (1+ bkptr)))
                      (t (mv nil type-alist ttree0)))))
                (t (mv-let (flg type-alist ttree2)
                    (with-accumulated-persistence rune
                      (flg type-alist ttree2)
                      flg
                      (mv-let (ts1 ttree1)
                        (type-set-rec atm1
                          force-flg
                          dwp
                          type-alist
                          (push-ancestor (if not-flg
                              atm1
                              (mcons-term* 'not atm1))
                            (list rune)
                            ancestors
                            nil)
                          ens
                          wrld
                          ttree
                          pot-lst
                          pt
                          (new-backchain-limit (car backchain-limit-lst)
                            backchain-limit
                            ancestors))
                        (let ((ts (if not-flg
                               (cond ((ts= ts1 *ts-nil*) *ts-t*)
                                 ((ts-intersectp ts1 *ts-nil*) *ts-boolean*)
                                 (t *ts-nil*))
                               ts1)))
                          (cond ((ts= ts *ts-nil*) (mv nil type-alist ttree0))
                            ((ts-intersectp *ts-nil* ts) (mv-let (force-flg ttree)
                                (cond ((not (and force-flg forcep)) (mv nil ttree))
                                  (t (force-assumption rune
                                      target
                                      (if not-flg
                                        (mcons-term* 'not atm1)
                                        atm1)
                                      type-alist
                                      nil
                                      (immediate-forcep (ffn-symb (car hyps)) ens)
                                      force-flg
                                      ttree)))
                                (cond (force-flg (mv t type-alist ttree))
                                  (t (mv nil type-alist ttree0)))))
                            (t (mv t type-alist ttree1)))))
                      bkptr)
                    (cond (flg (type-set-relieve-hyps rune
                          target
                          (cdr hyps)
                          (cdr backchain-limit-lst)
                          force-flg
                          dwp
                          alist
                          type-alist
                          ancestors
                          ens
                          wrld
                          ttree2
                          ttree0
                          pot-lst
                          pt
                          backchain-limit
                          (1+ bkptr)))
                      (t (mv nil type-alist ttree2))))))))))))
  (defun type-set-relieve-hyps
    (rune target
      hyps
      backchain-limit-lst
      force-flg
      dwp
      alist
      type-alist
      ancestors
      ens
      wrld
      ttree
      ttree0
      pot-lst
      pt
      backchain-limit
      bkptr)
    (cond ((null hyps) (mv t type-alist (cons-tag-trees ttree ttree0)))
      (t (mv-let (forcep bind-flg)
          (binding-hyp-p (car hyps) alist wrld)
          (let ((hyp (if forcep
                 (fargn (car hyps) 1)
                 (car hyps))))
            (cond (bind-flg (type-set-relieve-hyps rune
                  target
                  (cdr hyps)
                  (cdr backchain-limit-lst)
                  force-flg
                  dwp
                  (cons (cons (fargn hyp 1) (fargn hyp 2)) alist)
                  type-alist
                  ancestors
                  ens
                  wrld
                  ttree
                  ttree0
                  pot-lst
                  pt
                  backchain-limit
                  (1+ bkptr)))
              (t (mv-let (term typ compound-rec-rune?)
                  (term-and-typ-to-lookup hyp wrld ens)
                  (mv-let (lookup-hyp-ans alist+ ttree rest-type-alist)
                    (search-type-alist-with-rest term
                      typ
                      type-alist
                      alist
                      ttree
                      wrld)
                    (cond (lookup-hyp-ans (let ((ttree (push-lemma? compound-rec-rune? ttree)))
                          (cond ((and rest-type-alist
                               (not (eq (caar alist) (caar alist+)))
                               (not (oncep-tp rune wrld))) (let ((bkptr+1 (1+ bkptr)))
                                (mv-let (relieve-hyps-ans type-alist ttree)
                                  (type-set-relieve-hyps rune
                                    target
                                    (cdr hyps)
                                    (cdr backchain-limit-lst)
                                    force-flg
                                    dwp
                                    alist+
                                    type-alist
                                    ancestors
                                    ens
                                    wrld
                                    ttree
                                    ttree0
                                    pot-lst
                                    pt
                                    backchain-limit
                                    bkptr+1)
                                  (cond (relieve-hyps-ans (mv relieve-hyps-ans type-alist ttree))
                                    (t (type-set-relieve-hyps-free term
                                        typ
                                        rest-type-alist
                                        rune
                                        target
                                        hyps
                                        backchain-limit-lst
                                        force-flg
                                        dwp
                                        alist
                                        type-alist
                                        ancestors
                                        ens
                                        wrld
                                        ttree
                                        ttree0
                                        pot-lst
                                        pt
                                        backchain-limit
                                        bkptr+1))))))
                            (t (type-set-relieve-hyps rune
                                target
                                (cdr hyps)
                                (cdr backchain-limit-lst)
                                force-flg
                                dwp
                                alist+
                                type-alist
                                ancestors
                                ens
                                wrld
                                ttree
                                ttree0
                                pot-lst
                                pt
                                backchain-limit
                                (1+ bkptr))))))
                      ((free-varsp hyp alist) (let ((fully-bound-alist (if (and forcep force-flg)
                               (bind-free-vars-to-unbound-free-vars (all-vars hyp) alist)
                               alist)))
                          (mv-let (force-flg ttree)
                            (cond ((not (and forcep force-flg)) (mv nil ttree))
                              (t (force-assumption rune
                                  target
                                  (sublis-var fully-bound-alist hyp)
                                  type-alist
                                  nil
                                  (immediate-forcep (ffn-symb (car hyps)) ens)
                                  force-flg
                                  ttree)))
                            (cond (force-flg (type-set-relieve-hyps rune
                                  target
                                  (cdr hyps)
                                  (cdr backchain-limit-lst)
                                  force-flg
                                  dwp
                                  fully-bound-alist
                                  type-alist
                                  ancestors
                                  ens
                                  wrld
                                  ttree
                                  ttree0
                                  pot-lst
                                  pt
                                  backchain-limit
                                  (1+ bkptr)))
                              (t (mv nil type-alist ttree0))))))
                      (t (mv-let (not-flg atm)
                          (strip-not hyp)
                          (mv-let (atm1 quotep-atm1 ttree)
                            (sublis-var! alist atm ens wrld ttree)
                            (cond (quotep-atm1 (cond ((eq not-flg (equal atm1 *nil*)) (type-set-relieve-hyps rune
                                      target
                                      (cdr hyps)
                                      (cdr backchain-limit-lst)
                                      force-flg
                                      dwp
                                      alist
                                      type-alist
                                      ancestors
                                      ens
                                      wrld
                                      ttree
                                      ttree0
                                      pot-lst
                                      pt
                                      backchain-limit
                                      (1+ bkptr)))
                                  (t (mv nil type-alist ttree0))))
                              (t (mv-let (on-ancestorsp assumed-true)
                                  (if (eq ancestors t)
                                    (mv t nil)
                                    (ancestors-check (if not-flg
                                        (mcons-term* 'not atm1)
                                        atm1)
                                      ancestors
                                      (list rune)))
                                  (cond (on-ancestorsp (cond (assumed-true (type-set-relieve-hyps rune
                                            target
                                            (cdr hyps)
                                            (cdr backchain-limit-lst)
                                            force-flg
                                            dwp
                                            alist
                                            type-alist
                                            ancestors
                                            ens
                                            wrld
                                            ttree
                                            ttree0
                                            pot-lst
                                            pt
                                            backchain-limit
                                            (1+ bkptr)))
                                        (t (mv nil type-alist ttree0))))
                                    ((backchain-limit-reachedp backchain-limit ancestors) (mv-let (force-flg ttree)
                                        (cond ((not (and force-flg forcep)) (mv nil ttree))
                                          (t (force-assumption rune
                                              target
                                              (if not-flg
                                                (mcons-term* 'not atm1)
                                                atm1)
                                              type-alist
                                              nil
                                              (immediate-forcep (ffn-symb (car hyps)) ens)
                                              force-flg
                                              ttree)))
                                        (cond (force-flg (type-set-relieve-hyps rune
                                              target
                                              (cdr hyps)
                                              (cdr backchain-limit-lst)
                                              force-flg
                                              dwp
                                              alist
                                              type-alist
                                              ancestors
                                              ens
                                              wrld
                                              ttree
                                              ttree0
                                              pot-lst
                                              pt
                                              backchain-limit
                                              (1+ bkptr)))
                                          (t (mv nil type-alist ttree0)))))
                                    (t (mv-let (flg type-alist ttree2)
                                        (with-accumulated-persistence rune
                                          (flg type-alist ttree2)
                                          flg
                                          (mv-let (ts1 ttree1)
                                            (type-set-rec atm1
                                              force-flg
                                              dwp
                                              type-alist
                                              (push-ancestor (if not-flg
                                                  atm1
                                                  (mcons-term* 'not atm1))
                                                (list rune)
                                                ancestors
                                                nil)
                                              ens
                                              wrld
                                              ttree
                                              pot-lst
                                              pt
                                              (new-backchain-limit (car backchain-limit-lst)
                                                backchain-limit
                                                ancestors))
                                            (let ((ts (if not-flg
                                                   (cond ((ts= ts1 *ts-nil*) *ts-t*)
                                                     ((ts-intersectp ts1 *ts-nil*) *ts-boolean*)
                                                     (t *ts-nil*))
                                                   ts1)))
                                              (cond ((ts= ts *ts-nil*) (mv nil type-alist ttree0))
                                                ((ts-intersectp *ts-nil* ts) (mv-let (force-flg ttree)
                                                    (cond ((not (and force-flg forcep)) (mv nil ttree))
                                                      (t (force-assumption rune
                                                          target
                                                          (if not-flg
                                                            (mcons-term* 'not atm1)
                                                            atm1)
                                                          type-alist
                                                          nil
                                                          (immediate-forcep (ffn-symb (car hyps)) ens)
                                                          force-flg
                                                          ttree)))
                                                    (cond (force-flg (mv t type-alist ttree))
                                                      (t (mv nil type-alist ttree0)))))
                                                (t (mv t type-alist ttree1)))))
                                          bkptr)
                                        (cond (flg (type-set-relieve-hyps rune
                                              target
                                              (cdr hyps)
                                              (cdr backchain-limit-lst)
                                              force-flg
                                              dwp
                                              alist
                                              type-alist
                                              ancestors
                                              ens
                                              wrld
                                              ttree2
                                              ttree0
                                              pot-lst
                                              pt
                                              backchain-limit
                                              (1+ bkptr)))
                                          (t (mv nil type-alist ttree2))))))))))))))))))))))
  (defun extend-type-alist-with-bindings
    (alist force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      ttree
      pot-lst
      pt
      backchain-limit)
    (cond ((null alist) type-alist)
      (t (extend-type-alist-with-bindings (cdr alist)
          force-flg
          dwp
          (cond ((assoc-equal (cdr (car alist)) type-alist) type-alist)
            (t (mv-let (ts ttree1)
                (type-set-rec (cdr (car alist))
                  force-flg
                  dwp
                  type-alist
                  ancestors
                  ens
                  w
                  ttree
                  pot-lst
                  pt
                  backchain-limit)
                (extend-type-alist (cdr (car alist)) ts ttree1 type-alist w))))
          ancestors
          ens
          w
          ttree
          pot-lst
          pt
          backchain-limit))))
  (defun type-set-with-rule
    (tp term
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      ttree
      pot-lst
      pt
      backchain-limit
      extended-p)
    (declare (ignore dwp))
    (cond ((enabled-numep (access type-prescription tp :nume) ens) (mv-let (unify-ans unify-subst)
          (one-way-unify (access type-prescription tp :term) term)
          (cond (unify-ans (with-accumulated-persistence (access type-prescription tp :rune)
                (ts type-alist-out ttree-out extended-p-out)
                (or (not (ts= *ts-unknown* ts))
                  (not (eq type-alist type-alist-out)))
                (let ((hyps (access type-prescription tp :hyps)))
                  (mv-let (type-alist extended-p)
                    (cond ((or (null hyps) extended-p) (mv type-alist extended-p))
                      (t (mv (extend-type-alist-with-bindings unify-subst
                            force-flg
                            nil
                            type-alist
                            ancestors
                            ens
                            w
                            nil
                            pot-lst
                            pt
                            backchain-limit)
                          t)))
                    (mv-let (relieve-hyps-ans type-alist ttree)
                      (type-set-relieve-hyps (access type-prescription tp :rune)
                        term
                        hyps
                        (access type-prescription tp :backchain-limit-lst)
                        force-flg
                        nil
                        unify-subst
                        type-alist
                        ancestors
                        ens
                        w
                        nil
                        ttree
                        pot-lst
                        pt
                        backchain-limit
                        1)
                      (cond (relieve-hyps-ans (mv-let (ts type-alist ttree)
                            (with-accumulated-persistence (access type-prescription tp :rune)
                              (ts type-alist-out ttree)
                              (or (not (ts= *ts-unknown* ts))
                                (not (eq type-alist type-alist-out)))
                              (type-set-with-rule1 unify-subst
                                (access type-prescription tp :vars)
                                force-flg
                                nil
                                type-alist
                                ancestors
                                ens
                                w
                                (access type-prescription tp :basic-ts)
                                (push-lemma (access type-prescription tp :rune) ttree)
                                pot-lst
                                pt
                                backchain-limit)
                              :conc hyps)
                            (mv ts type-alist ttree extended-p)))
                        (t (mv *ts-unknown* type-alist ttree extended-p))))))))
            (t (mv *ts-unknown* type-alist ttree nil)))))
      (t (mv *ts-unknown* type-alist ttree nil))))
  (defun type-set-with-rule1
    (alist vars
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      basic-ts
      ttree
      pot-lst
      pt
      backchain-limit)
    (cond ((null alist) (mv basic-ts type-alist ttree))
      ((member-eq (caar alist) vars) (mv-let (ts ttree)
          (type-set-rec (cdar alist)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree
            pot-lst
            pt
            backchain-limit)
          (type-set-with-rule1 (cdr alist)
            vars
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            (ts-union ts basic-ts)
            ttree
            pot-lst
            pt
            backchain-limit)))
      (t (type-set-with-rule1 (cdr alist)
          vars
          force-flg
          dwp
          type-alist
          ancestors
          ens
          w
          basic-ts
          ttree
          pot-lst
          pt
          backchain-limit))))
  (defun type-set-with-rules
    (tp-lst term
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      ts
      ttree
      pot-lst
      pt
      backchain-limit
      extended-p)
    (cond ((null tp-lst) (mv-let (ts1 ttree1)
          (type-set-primitive term
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree
            pot-lst
            pt
            backchain-limit)
          (let ((ts2 (ts-intersection ts1 ts)))
            (mv ts2
              (if (ts= ts2 ts)
                ttree
                ttree1)
              extended-p))))
      ((ts-subsetp ts
         (access type-prescription (car tp-lst) :basic-ts)) (type-set-with-rules (cdr tp-lst)
          term
          force-flg
          dwp
          type-alist
          ancestors
          ens
          w
          ts
          ttree
          pot-lst
          pt
          backchain-limit
          extended-p))
      (t (mv-let (ts1 type-alist1 ttree1 extended-p)
          (type-set-with-rule (car tp-lst)
            term
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree
            pot-lst
            pt
            backchain-limit
            extended-p)
          (let ((ts2 (ts-intersection ts1 ts)))
            (type-set-with-rules (cdr tp-lst)
              term
              force-flg
              dwp
              type-alist1
              ancestors
              ens
              w
              ts2
              (if (and (ts= ts2 ts) (equal type-alist type-alist1))
                ttree
                ttree1)
              pot-lst
              pt
              backchain-limit
              extended-p))))))
  (defun type-set-primitive
    (term force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      ttree0
      pot-lst
      pt
      backchain-limit)
    (case (ffn-symb term)
      (cons (mv-let (ts2 ttree)
          (type-set-rec (fargn term 2)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-cons ts2 ttree ttree0)))
      (equal (cond ((equal (fargn term 1) (fargn term 2)) (mv *ts-t* ttree0))
          (t (mv-let (ts1 ttree)
              (type-set-rec (fargn term 1)
                force-flg
                dwp
                type-alist
                ancestors
                ens
                w
                ttree0
                pot-lst
                pt
                backchain-limit)
              (mv-let (ts2 ttree)
                (type-set-rec (fargn term 2)
                  force-flg
                  dwp
                  type-alist
                  ancestors
                  ens
                  w
                  ttree
                  pot-lst
                  pt
                  backchain-limit)
                (type-set-equal ts1 ts2 ttree ttree0))))))
      (unary-- (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-unary-- ts1 ttree ttree0)))
      (unary-/ (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-unary-/ ts1 ttree ttree0)))
      (denominator (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-denominator ts1 ttree ttree0)))
      (numerator (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-numerator ts1 ttree ttree0)))
      (car (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-car ts1 ttree ttree0)))
      (cdr (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-cdr ts1 ttree ttree0)))
      (symbol-name (mv *ts-string* (puffert ttree0)))
      (symbol-package-name (mv *ts-string* (puffert ttree0)))
      (intern-in-package-of-symbol (mv-let (ts1 ttree1)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree2)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree0
              pot-lst
              pt
              backchain-limit)
            (type-set-intern-in-package-of-symbol ts1
              ts2
              ttree1
              ttree2
              ttree0))))
      (pkg-witness (mv *ts-symbol* (puffert ttree0)))
      (coerce (mv-let (ts1 ttree1)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree2)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree0
              pot-lst
              pt
              backchain-limit)
            (type-set-coerce term ts1 ts2 ttree1 ttree2 ttree0))))
      (length (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-length ts1 ttree ttree0)))
      (binary-+ (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree
              pot-lst
              pt
              backchain-limit)
            (type-set-binary-+ term ts1 ts2 ttree ttree0))))
      (binary-* (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree
              pot-lst
              pt
              backchain-limit)
            (type-set-binary-* ts1 ts2 ttree ttree0))))
      (< (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree
              pot-lst
              pt
              backchain-limit)
            (type-set-< (fargn term 1)
              (fargn term 2)
              ts1
              ts2
              type-alist
              ttree
              ttree0
              pot-lst
              pt))))
      (not (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-not ts1 ttree ttree0)))
      (realpart (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-realpart ts1 ttree ttree0)))
      (imagpart (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-imagpart ts1 ttree ttree0)))
      (complex (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (mv-let (ts2 ttree)
            (type-set-rec (fargn term 2)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              w
              ttree
              pot-lst
              pt
              backchain-limit)
            (type-set-complex ts1 ts2 ttree ttree0))))
      (char-code (mv-let (ts1 ttree)
          (type-set-rec (fargn term 1)
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            ttree0
            pot-lst
            pt
            backchain-limit)
          (type-set-char-code ts1 ttree ttree0)))
      (otherwise (mv *ts-unknown* ttree0))))
  (defun assume-true-false-if
    (not-flg x
      xttree
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      pot-lst
      pt
      backchain-limit)
    (let ((test (fargn x 1)) (true-branch (fargn x 2))
        (false-branch (fargn x 3)))
      (mv-let (test-mbt test-mbf test-tta test-fta test-ttree)
        (assume-true-false-rec test
          xttree
          force-flg
          dwp
          type-alist
          ancestors
          ens
          w
          pot-lst
          pt
          nil
          backchain-limit)
        (cond (test-mbt (mv-let (mbt mbf tta fta ttree)
              (assume-true-false-rec true-branch
                test-ttree
                force-flg
                dwp
                test-tta
                ancestors
                ens
                w
                pot-lst
                pt
                nil
                backchain-limit)
              (mv-atf not-flg mbt mbf tta fta ttree nil)))
          (test-mbf (mv-let (mbt mbf tta fta ttree)
              (assume-true-false-rec false-branch
                test-ttree
                force-flg
                dwp
                test-fta
                ancestors
                ens
                w
                pot-lst
                pt
                nil
                backchain-limit)
              (mv-atf not-flg mbt mbf tta fta ttree nil)))
          (t (mv-let (tb-mbt tb-mbf tb-tta tb-fta tb-ttree)
              (assume-true-false-rec true-branch
                xttree
                force-flg
                dwp
                test-tta
                ancestors
                ens
                w
                pot-lst
                pt
                nil
                backchain-limit)
              (mv-let (fb-mbt fb-mbf fb-tta fb-fta fb-ttree)
                (assume-true-false-rec false-branch
                  xttree
                  force-flg
                  dwp
                  test-fta
                  ancestors
                  ens
                  w
                  pot-lst
                  pt
                  nil
                  backchain-limit)
                (cond ((and tb-mbf fb-mbf) (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg nil t nil type-alist xttree x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            t
                            nil
                            (extend-type-alist-simple x
                              *ts-nil*
                              (cons-tag-trees tb-ttree fb-ttree)
                              type-alist)
                            tb-ttree
                            fb-ttree)))))
                  ((and tb-mbt fb-mbt) (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg t nil type-alist nil xttree x-ts-ttree))
                        (t (mv-atf not-flg
                            t
                            nil
                            (extend-type-alist-simple x
                              (ts-intersection x-ts *ts-non-nil*)
                              (cons-tag-trees x-ts-ttree
                                (cons-tag-trees tb-ttree fb-ttree))
                              type-alist)
                            nil
                            tb-ttree
                            fb-ttree)))))
                  ((and tb-mbt fb-mbf) (mv-atf not-flg
                      nil
                      nil
                      (infect-new-type-alist-entries tb-tta
                        type-alist
                        (cons-tag-trees tb-ttree fb-ttree))
                      (infect-new-type-alist-entries fb-fta
                        type-alist
                        (cons-tag-trees tb-ttree fb-ttree))
                      nil
                      nil))
                  ((and tb-mbf fb-mbt) (mv-atf not-flg
                      nil
                      nil
                      (infect-new-type-alist-entries fb-tta
                        type-alist
                        (cons-tag-trees tb-ttree fb-ttree))
                      (infect-new-type-alist-entries tb-fta
                        type-alist
                        (cons-tag-trees tb-ttree fb-ttree))
                      nil
                      nil))
                  (tb-mbt (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg
                            nil
                            t
                            nil
                            (infect-new-type-alist-entries fb-fta type-alist tb-ttree)
                            xttree
                            x-ts-ttree))
                        ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg t nil type-alist nil xttree x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            nil
                            (extend-type-alist-simple x
                              (ts-intersection x-ts *ts-non-nil*)
                              (cons-tag-trees x-ts-ttree xttree)
                              type-alist)
                            (infect-new-type-alist-entries fb-fta type-alist tb-ttree)
                            nil
                            nil)))))
                  (tb-mbf (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg nil t nil type-alist xttree x-ts-ttree))
                        ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg
                            t
                            nil
                            (infect-new-type-alist-entries fb-tta type-alist tb-ttree)
                            nil
                            xttree
                            x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            nil
                            (infect-new-type-alist-entries fb-tta type-alist tb-ttree)
                            (extend-type-alist-simple x *ts-nil* xttree type-alist)
                            nil
                            nil)))))
                  (fb-mbt (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg
                            nil
                            t
                            nil
                            (infect-new-type-alist-entries tb-fta type-alist fb-ttree)
                            xttree
                            x-ts-ttree))
                        ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg t nil type-alist nil xttree x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            nil
                            (extend-type-alist-simple x
                              (ts-intersection x-ts *ts-non-nil*)
                              (cons-tag-trees x-ts-ttree xttree)
                              type-alist)
                            (infect-new-type-alist-entries tb-fta type-alist fb-ttree)
                            nil
                            nil)))))
                  (fb-mbf (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg nil t nil type-alist xttree x-ts-ttree))
                        ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg
                            t
                            nil
                            (infect-new-type-alist-entries tb-tta type-alist fb-ttree)
                            nil
                            xttree
                            x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            nil
                            (infect-new-type-alist-entries tb-tta type-alist fb-ttree)
                            (extend-type-alist-simple x *ts-nil* xttree type-alist)
                            nil
                            nil)))))
                  (t (mv-let (x-ts x-ts-ttree)
                      (look-in-type-alist x type-alist w)
                      (cond ((ts= x-ts *ts-nil*) (mv-atf not-flg nil t nil type-alist xttree x-ts-ttree))
                        ((ts-disjointp x-ts *ts-nil*) (mv-atf not-flg t nil type-alist nil xttree x-ts-ttree))
                        (t (mv-atf not-flg
                            nil
                            nil
                            (extend-type-alist-simple x
                              (ts-intersection x-ts *ts-non-nil*)
                              (cons-tag-trees x-ts-ttree xttree)
                              type-alist)
                            (extend-type-alist-simple x *ts-nil* xttree type-alist)
                            nil
                            nil)))))))))))))
  (defun assume-true-false-rec
    (x xttree
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      pot-lst
      pt
      ignore0
      backchain-limit)
    (mv-let (xnot-flg x)
      (cond ((nvariablep x) (cond ((eq (ffn-symb x) 'not) (mv t (fargn x 1)))
            ((and (eq (ffn-symb x) 'if)
               (equal (fargn x 2) *nil*)
               (equal (fargn x 3) *t*)) (mv t (fargn x 1)))
            (t (mv nil x))))
        (t (mv nil x)))
      (cond ((variablep x) (assume-true-false1 xnot-flg
            x
            xttree
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            pot-lst
            pt
            backchain-limit))
        ((fquotep x) (if (equal x *nil*)
            (mv-atf xnot-flg nil t nil type-alist nil xttree)
            (mv-atf xnot-flg t nil type-alist nil nil xttree)))
        ((flambda-applicationp x) (assume-true-false1 xnot-flg
            x
            xttree
            force-flg
            dwp
            type-alist
            ancestors
            ens
            w
            pot-lst
            pt
            backchain-limit))
        (t (mv-let (var strongp true-ts false-ts |RUNE[S]|)
            (recognizer-expr-p x ens w)
            (let ((ignore (adjust-ignore-for-atf xnot-flg ignore0)))
              (cond (var (mv-let (ts ttree)
                    (cond (strongp (mv nil nil))
                      (t (assoc-type-alist x type-alist w)))
                    (cond ((and ts (ts= ts *ts-nil*)) (mv-atf xnot-flg nil t nil type-alist ttree xttree))
                      ((and ts (ts-disjointp ts *ts-nil*)) (mv-atf xnot-flg t nil type-alist nil ttree xttree))
                      (t (mv-let (ts0 arg)
                          (if (eq var :one)
                            (strengthen-recog-call x)
                            (mv nil var))
                          (mv-let (ts ttree)
                            (type-set-rec arg
                              force-flg
                              dwp
                              type-alist
                              ancestors
                              ens
                              w
                              nil
                              pot-lst
                              pt
                              backchain-limit)
                            (let ((t-int (ts-intersection ts
                                   (if ts0
                                     (ts-union ts0 true-ts)
                                     true-ts))) (f-int (ts-intersection ts false-ts)))
                              (cond ((ts= t-int *ts-empty*) (cond ((ts= f-int *ts-empty*) (mv-atf xnot-flg
                                        t
                                        t
                                        type-alist
                                        type-alist
                                        (|PUSH-LEMMA[S]| var
                                          |RUNE[S]|
                                          (if ts0
                                            (puffert ttree)
                                            ttree))
                                        xttree))
                                    (t (mv-atf xnot-flg
                                        nil
                                        t
                                        nil
                                        type-alist
                                        (|PUSH-LEMMA[S]| var
                                          |RUNE[S]|
                                          (if ts0
                                            (puffert ttree)
                                            ttree))
                                        xttree))))
                                ((ts= f-int *ts-empty*) (mv-atf xnot-flg
                                    t
                                    nil
                                    type-alist
                                    nil
                                    (|PUSH-LEMMA[S]| var |RUNE[S]| ttree)
                                    xttree))
                                (t (let ((shared-ttree (|PUSH-LEMMA[S]| var
                                         |RUNE[S]|
                                         (if ts0
                                           (puffert (cons-tag-trees ttree xttree))
                                           (cons-tag-trees ttree xttree)))))
                                    (mv-atf xnot-flg
                                      nil
                                      nil
                                      (and (not (eq ignore :tta))
                                        (let ((type-alist0 (if strongp
                                               type-alist
                                               (extend-type-alist-simple x
                                                 *ts-t*
                                                 (|PUSH-LEMMA[S]| var |RUNE[S]| xttree)
                                                 type-alist))))
                                          (cond ((ts= t-int ts) type-alist0)
                                            (t (extend-with-proper/improper-cons-ts-tuple arg
                                                t-int
                                                shared-ttree
                                                force-flg
                                                dwp
                                                type-alist
                                                ancestors
                                                ens
                                                type-alist0
                                                w
                                                pot-lst
                                                pt
                                                backchain-limit)))))
                                      (and (not (eq ignore :fta))
                                        (let ((type-alist0 (if strongp
                                               type-alist
                                               (extend-type-alist-simple x *ts-nil* xttree type-alist))))
                                          (cond ((ts= f-int ts) type-alist0)
                                            (t (extend-with-proper/improper-cons-ts-tuple arg
                                                f-int
                                                shared-ttree
                                                force-flg
                                                dwp
                                                type-alist
                                                ancestors
                                                ens
                                                type-alist0
                                                w
                                                pot-lst
                                                pt
                                                backchain-limit)))))
                                      nil
                                      nil)))))))))))
                ((member-eq (ffn-symb x) *expandable-boot-strap-non-rec-fns*) (mv-let (mbt mbf tta fta ttree)
                    (assume-true-false-rec (subcor-var (formals (ffn-symb x) w)
                        (fargs x)
                        (bbody (ffn-symb x)))
                      xttree
                      force-flg
                      dwp
                      type-alist
                      ancestors
                      ens
                      w
                      pot-lst
                      pt
                      ignore
                      backchain-limit)
                    (if xnot-flg
                      (mv mbf mbt fta tta ttree)
                      (mv mbt mbf tta fta ttree))))
                ((eq (ffn-symb x) 'equal) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
                    (cond ((equal arg1 arg2) (mv-atf xnot-flg t nil type-alist nil nil (puffert xttree)))
                      ((and (quotep arg1) (quotep arg2)) (mv-atf xnot-flg
                          nil
                          t
                          nil
                          type-alist
                          nil
                          (push-lemma '(:executable-counterpart equal) xttree)))
                      (t (mv-let (occursp1 canonicalp1 arg1-canon ttree1)
                          (canonical-representative 'equal arg1 type-alist)
                          (cond ((and occursp1 (equal arg1-canon arg2)) (mv-atf xnot-flg
                                t
                                nil
                                type-alist
                                nil
                                nil
                                (puffert (cons-tag-trees ttree1 xttree))))
                            ((and occursp1 (quotep arg1-canon) (quotep arg2)) (mv-atf xnot-flg
                                nil
                                t
                                nil
                                type-alist
                                nil
                                (push-lemma '(:executable-counterpart equal)
                                  (puffert (cons-tag-trees ttree1 xttree)))))
                            (t (mv-let (occursp2 canonicalp2 arg2-canon ttree2)
                                (canonical-representative 'equal arg2 type-alist)
                                (cond ((and occursp2 (equal arg1-canon arg2-canon)) (mv-atf xnot-flg
                                      t
                                      nil
                                      type-alist
                                      nil
                                      nil
                                      (puffert (cons-tag-trees xttree (cons-tag-trees ttree1 ttree2)))))
                                  ((and occursp2 (quotep arg1-canon) (quotep arg2-canon)) (mv-atf xnot-flg
                                      nil
                                      t
                                      nil
                                      type-alist
                                      nil
                                      (push-lemma '(:executable-counterpart equal)
                                        (puffert (cons-tag-trees xttree (cons-tag-trees ttree1 ttree2))))))
                                  (t (let ((temp-temp (assoc-equiv 'equal arg1-canon arg2-canon type-alist)))
                                      (cond (temp-temp (cond ((ts= (cadr temp-temp) *ts-t*) (mv-atf (er hard
                                                  'assume-true-false
                                                  "Please send the authors of ACL2 a ~
                                           replayable transcript of this ~
                                           problem if possible, so that they ~
                                           can see what went wrong in the ~
                                           function assume-true-false.  The ~
                                           offending call was ~x0.  The ~
                                           surprising type-set arose from a ~
                                           call of ~x1."
                                                  (list 'assume-true-false
                                                    (kwote x)
                                                    '<xttree>
                                                    force-flg
                                                    (kwote type-alist)
                                                    '<ens>
                                                    '<w>)
                                                  (list 'assoc-equiv
                                                    ''equal
                                                    (kwote arg1-canon)
                                                    (kwote arg2-canon)
                                                    '<same_type-alist>))
                                                nil
                                                nil
                                                nil
                                                nil
                                                nil
                                                nil))
                                            ((ts= (cadr temp-temp) *ts-nil*) (mv-atf xnot-flg
                                                nil
                                                t
                                                nil
                                                type-alist
                                                nil
                                                (if (and canonicalp1 canonicalp2)
                                                  (cons-tag-trees (cddr temp-temp) xttree)
                                                  (puffert (cons-tag-trees (cddr temp-temp)
                                                      (cons-tag-trees ttree1 (cons-tag-trees ttree2 xttree)))))))
                                            (t (let ((erp (assume-true-false-error type-alist x (cadr temp-temp))))
                                                (mv erp nil nil nil nil)))))
                                        (t (mv-let (ts1 ttree)
                                            (type-set-rec arg1
                                              force-flg
                                              dwp
                                              type-alist
                                              ancestors
                                              ens
                                              w
                                              nil
                                              pot-lst
                                              pt
                                              backchain-limit)
                                            (mv-let (ts2 ttree)
                                              (type-set-rec arg2
                                                force-flg
                                                dwp
                                                type-alist
                                                ancestors
                                                ens
                                                w
                                                ttree
                                                pot-lst
                                                pt
                                                backchain-limit)
                                              (let ((int (ts-intersection ts1 ts2)))
                                                (cond ((ts= int *ts-empty*) (mv-atf xnot-flg
                                                      nil
                                                      t
                                                      nil
                                                      type-alist
                                                      nil
                                                      (puffert (cons-tag-trees ttree xttree))))
                                                  ((and (ts= ts1 ts2) (member ts1 *singleton-type-sets*)) (mv-atf xnot-flg
                                                      t
                                                      nil
                                                      type-alist
                                                      nil
                                                      nil
                                                      (puffert (cons-tag-trees ttree xttree))))
                                                  (t (let* ((swap-flg (term-order arg1-canon arg2-canon)) (shared-ttree-tta-p (and (not (eq ignore :tta))
                                                            (or (not (ts= ts1 int)) (not (ts= ts2 int)))))
                                                        (shared-ttree (cond (shared-ttree-tta-p (cons-tag-trees ttree xttree))
                                                            (t nil)))
                                                        (xttree+ (if (and canonicalp1 canonicalp2)
                                                            xttree
                                                            (puffert (cons-tag-trees ttree1 (cons-tag-trees ttree2 xttree)))))
                                                        (true-type-alist1 (and (not (eq ignore :tta))
                                                            (extend-type-alist1 'equal
                                                              occursp1
                                                              occursp2
                                                              (and canonicalp1 canonicalp2)
                                                              arg1-canon
                                                              arg2-canon
                                                              swap-flg
                                                              x
                                                              *ts-t*
                                                              xttree+
                                                              type-alist)))
                                                        (true-type-alist2 (and (not (eq ignore :tta))
                                                            (cond ((ts= ts1 int) true-type-alist1)
                                                              (t (extend-with-proper/improper-cons-ts-tuple arg1
                                                                  int
                                                                  shared-ttree
                                                                  force-flg
                                                                  dwp
                                                                  type-alist
                                                                  ancestors
                                                                  ens
                                                                  true-type-alist1
                                                                  w
                                                                  pot-lst
                                                                  pt
                                                                  backchain-limit)))))
                                                        (true-type-alist3 (and (not (eq ignore :tta))
                                                            (cond ((ts= ts2 int) true-type-alist2)
                                                              (t (extend-with-proper/improper-cons-ts-tuple arg2
                                                                  int
                                                                  shared-ttree
                                                                  force-flg
                                                                  dwp
                                                                  type-alist
                                                                  ancestors
                                                                  ens
                                                                  true-type-alist2
                                                                  w
                                                                  pot-lst
                                                                  pt
                                                                  backchain-limit)))))
                                                        (false-type-alist1 (and (not (eq ignore :fta))
                                                            (extend-type-alist1 'equal
                                                              occursp1
                                                              occursp2
                                                              (and canonicalp1 canonicalp2)
                                                              arg1-canon
                                                              arg2-canon
                                                              swap-flg
                                                              x
                                                              *ts-nil*
                                                              xttree+
                                                              type-alist)))
                                                        (false-type-alist2 (and (not (eq ignore :fta))
                                                            (cond ((or (ts= ts2 *ts-t*)
                                                                 (ts= ts2 *ts-nil*)
                                                                 (ts= ts2 *ts-zero*)
                                                                 (and (ts= ts2 *ts-one*)
                                                                   (or (variablep arg1) (assoc-equal arg1 type-alist)))) (extend-with-proper/improper-cons-ts-tuple arg1
                                                                  (ts-intersection ts1 (ts-complement ts2))
                                                                  (if shared-ttree-tta-p
                                                                    shared-ttree
                                                                    (cons-tag-trees ttree xttree))
                                                                  force-flg
                                                                  dwp
                                                                  type-alist
                                                                  ancestors
                                                                  ens
                                                                  false-type-alist1
                                                                  w
                                                                  pot-lst
                                                                  pt
                                                                  backchain-limit))
                                                              (t false-type-alist1))))
                                                        (false-type-alist3 (and (not (eq ignore :fta))
                                                            (cond ((or (ts= ts1 *ts-t*)
                                                                 (ts= ts1 *ts-nil*)
                                                                 (ts= ts1 *ts-zero*)
                                                                 (and (ts= ts1 *ts-one*)
                                                                   (or (variablep arg2) (assoc-equal arg2 type-alist)))) (extend-with-proper/improper-cons-ts-tuple arg2
                                                                  (ts-intersection ts2 (ts-complement ts1))
                                                                  (if shared-ttree-tta-p
                                                                    shared-ttree
                                                                    (cons-tag-trees ttree xttree))
                                                                  force-flg
                                                                  dwp
                                                                  type-alist
                                                                  ancestors
                                                                  ens
                                                                  false-type-alist2
                                                                  w
                                                                  pot-lst
                                                                  pt
                                                                  backchain-limit))
                                                              (t false-type-alist2)))))
                                                      (mv-atf xnot-flg
                                                        nil
                                                        nil
                                                        true-type-alist3
                                                        false-type-alist3
                                                        nil
                                                        nil))))))))))))))))))))
                ((eq (ffn-symb x) '<) (mv-let (ts0 ttree)
                    (type-set-rec x
                      force-flg
                      dwp
                      type-alist
                      ancestors
                      ens
                      w
                      nil
                      pot-lst
                      pt
                      backchain-limit)
                    (cond ((ts= ts0 *ts-nil*) (mv-atf xnot-flg nil t nil type-alist ttree xttree))
                      ((ts-disjointp ts0 *ts-nil*) (mv-atf xnot-flg t nil type-alist nil ttree xttree))
                      (t (mv-let (ts1 ttree)
                          (type-set-rec (fargn x 1)
                            force-flg
                            dwp
                            type-alist
                            ancestors
                            ens
                            w
                            nil
                            pot-lst
                            pt
                            backchain-limit)
                          (mv-let (ts2 ttree)
                            (type-set-rec (fargn x 2)
                              force-flg
                              dwp
                              type-alist
                              ancestors
                              ens
                              w
                              ttree
                              pot-lst
                              pt
                              backchain-limit)
                            (mv-let (not-flg arg1 arg2 ts1 ts2)
                              (cond ((and (equal (fargn x 2) *1*)
                                   (ts-subsetp ts1
                                     (ts-union (ts-complement *ts-acl2-number*) *ts-integer*))) (mv (not xnot-flg) *0* (fargn x 1) *ts-zero* ts1))
                                ((and (equal (fargn x 2) *2*)
                                   (ts-subsetp ts1
                                     (ts-union (ts-complement *ts-acl2-number*) *ts-integer*))) (mv (not xnot-flg) *1* (fargn x 1) *ts-one* ts1))
                                ((and (equal (fargn x 1) *-1*)
                                   (ts-subsetp ts2
                                     (ts-union (ts-complement *ts-acl2-number*) *ts-integer*))) (mv (not xnot-flg) (fargn x 2) *0* ts2 *ts-zero*))
                                (t (mv xnot-flg (fargn x 1) (fargn x 2) ts1 ts2)))
                              (mv-let (not-flg arg1 arg2 ts1 ts2 ttree)
                                (cond ((and (equal arg1 *0*)
                                     (ts-subsetp ts2 *ts-integer*)
                                     (ffn-symb-p arg2 'binary-+)
                                     (equal (fargn arg2 1) *1*)) (mv-let (tsx ttree)
                                      (type-set-rec (fargn arg2 2)
                                        force-flg
                                        dwp
                                        type-alist
                                        ancestors
                                        ens
                                        w
                                        ttree
                                        pot-lst
                                        pt
                                        backchain-limit)
                                      (mv (not not-flg) (fargn arg2 2) *0* tsx *ts-zero* ttree)))
                                  ((and (equal arg2 *0*)
                                     (ts-subsetp ts1 *ts-integer*)
                                     (ffn-symb-p arg1 'binary-+)
                                     (equal (fargn arg1 1) *-1*)) (mv-let (tsx ttree)
                                      (type-set-rec (fargn arg1 2)
                                        force-flg
                                        dwp
                                        type-alist
                                        ancestors
                                        ens
                                        w
                                        ttree
                                        pot-lst
                                        pt
                                        backchain-limit)
                                      (mv (not not-flg) *0* (fargn arg1 2) *ts-zero* tsx ttree)))
                                  (t (mv not-flg arg1 arg2 ts1 ts2 ttree)))
                                (cond ((equal arg1 *0*) (cond ((ts-subsetp ts2 *ts-positive-rational*) (mv-atf not-flg t nil type-alist nil ttree xttree))
                                      ((ts-subsetp ts2
                                         (ts-union (ts-complement *ts-acl2-number*)
                                           *ts-non-positive-rational*)) (mv-atf not-flg nil t nil type-alist ttree xttree))
                                      (t (let* ((shared-ttree (cons-tag-trees ttree xttree)) (ignore (adjust-ignore-for-atf not-flg ignore0))
                                            (true-type-alist (and (not (eq ignore :tta))
                                                (let ((ts (ts-intersection ts2
                                                       (ts-union *ts-positive-rational* *ts-complex-rational*))))
                                                  (cond ((ts= ts2 ts) type-alist)
                                                    (t (extend-type-alist arg2
                                                        (the-type-set ts)
                                                        shared-ttree
                                                        type-alist
                                                        w))))))
                                            (false-type-alist (and (not (eq ignore :fta))
                                                (let ((ts (ts-intersection ts2 (ts-complement *ts-positive-rational*))))
                                                  (cond ((ts= ts2 ts) type-alist)
                                                    (t (extend-type-alist arg2
                                                        (the-type-set ts)
                                                        shared-ttree
                                                        type-alist
                                                        w)))))))
                                          (mv-atf-2 not-flg
                                            true-type-alist
                                            false-type-alist
                                            (mcons-term* '< *0* arg2)
                                            xnot-flg
                                            x
                                            shared-ttree
                                            xttree
                                            ignore)))))
                                  ((equal arg1 *1*) (cond ((ts-subsetp ts2 *ts-integer>1*) (mv-atf not-flg t nil type-alist nil ttree xttree))
                                      ((ts-subsetp ts2
                                         (ts-union (ts-complement *ts-acl2-number*)
                                           *ts-one*
                                           *ts-non-positive-rational*)) (mv-atf not-flg nil t nil type-alist ttree xttree))
                                      (t (let* ((shared-ttree (cons-tag-trees ttree xttree)) (ignore (adjust-ignore-for-atf not-flg ignore0))
                                            (true-type-alist (and (not (eq ignore :tta))
                                                (let ((ts (ts-intersection ts2
                                                       (ts-union *ts-integer>1*
                                                         *ts-positive-ratio*
                                                         *ts-complex-rational*))))
                                                  (cond ((ts= ts2 ts) type-alist)
                                                    (t (extend-type-alist arg2
                                                        (the-type-set ts)
                                                        shared-ttree
                                                        type-alist
                                                        w))))))
                                            (false-type-alist (and (not (eq ignore :fta))
                                                (cond ((variablep arg2) (let ((ts (ts-intersection ts2 (ts-complement *ts-integer>1*))))
                                                      (cond ((ts= ts2 ts) type-alist)
                                                        (t (extend-type-alist arg2
                                                            (the-type-set ts)
                                                            shared-ttree
                                                            type-alist
                                                            w)))))
                                                  (t type-alist)))))
                                          (mv-atf-2 not-flg
                                            true-type-alist
                                            false-type-alist
                                            (mcons-term* '< *1* arg2)
                                            xnot-flg
                                            x
                                            shared-ttree
                                            xttree
                                            ignore)))))
                                  ((equal arg2 *0*) (cond ((ts-subsetp ts1 *ts-negative-rational*) (mv-atf not-flg t nil type-alist nil ttree xttree))
                                      ((ts-subsetp ts1
                                         (ts-union (ts-complement *ts-acl2-number*)
                                           *ts-non-negative-rational*)) (mv-atf not-flg nil t nil type-alist ttree xttree))
                                      (t (let* ((shared-ttree (cons-tag-trees ttree xttree)) (ignore (adjust-ignore-for-atf not-flg ignore0))
                                            (true-type-alist (and (not (eq ignore :tta))
                                                (let ((ts (ts-intersection ts1
                                                       (ts-union *ts-negative-rational* *ts-complex-rational*))))
                                                  (cond ((ts= ts1 ts) type-alist)
                                                    (t (extend-type-alist arg1
                                                        (the-type-set ts)
                                                        shared-ttree
                                                        type-alist
                                                        w))))))
                                            (false-type-alist (and (not (eq ignore :fta))
                                                (let ((ts (ts-intersection ts1 (ts-complement *ts-negative-rational*))))
                                                  (cond ((ts= ts1 ts) type-alist)
                                                    (t (extend-type-alist arg1
                                                        (the-type-set ts)
                                                        shared-ttree
                                                        type-alist
                                                        w)))))))
                                          (mv-atf-2 not-flg
                                            true-type-alist
                                            false-type-alist
                                            (mcons-term* '< arg1 *0*)
                                            xnot-flg
                                            x
                                            shared-ttree
                                            xttree
                                            ignore)))))
                                  (t (mv-let (mbt mbf tta fta dttree)
                                      (assume-true-false1 xnot-flg
                                        x
                                        xttree
                                        force-flg
                                        dwp
                                        type-alist
                                        ancestors
                                        ens
                                        w
                                        pot-lst
                                        pt
                                        backchain-limit)
                                      (cond ((or mbt mbf) (mv mbt mbf tta fta dttree))
                                        (t (let ((tta (and (not (eq ignore0 :tta))
                                                 (assume-true-false-< not-flg
                                                   arg1
                                                   arg2
                                                   ts1
                                                   ts2
                                                   tta
                                                   ttree
                                                   xttree
                                                   w))) (fta (and (not (eq ignore0 :fta))
                                                  (assume-true-false-< (not not-flg)
                                                    arg1
                                                    arg2
                                                    ts1
                                                    ts2
                                                    fta
                                                    ttree
                                                    xttree
                                                    w))))
                                            (mv nil nil tta fta nil)))))))))))))))
                ((equivalence-relationp (ffn-symb x) w) (let ((arg1 (fargn x 1)) (arg2 (fargn x 2)))
                    (cond ((equal arg1 arg2) (mv-atf xnot-flg t nil type-alist nil nil (puffert xttree)))
                      (t (let ((equiv (ffn-symb x)))
                          (mv-let (occursp1 canonicalp1 arg1-canon ttree1)
                            (canonical-representative equiv arg1 type-alist)
                            (cond ((and occursp1 (equal arg1-canon arg2)) (mv-atf xnot-flg
                                  t
                                  nil
                                  type-alist
                                  nil
                                  nil
                                  (puffert (cons-tag-trees ttree1 xttree))))
                              (t (mv-let (occursp2 canonicalp2 arg2-canon ttree2)
                                  (canonical-representative equiv arg2 type-alist)
                                  (cond ((and occursp2 (equal arg1-canon arg2-canon)) (mv-atf xnot-flg
                                        t
                                        nil
                                        type-alist
                                        nil
                                        nil
                                        (puffert (cons-tag-trees xttree (cons-tag-trees ttree1 ttree2)))))
                                    (t (let ((temp-temp (assoc-equiv equiv arg1-canon arg2-canon type-alist)))
                                        (cond (temp-temp (cond ((ts= (cadr temp-temp) *ts-t*) (mv-atf (er hard
                                                    'assume-true-false
                                                    "Please send the authors of ~
                                               ACL2 a replayable transcript ~
                                               of this problem if possible, ~
                                               so that they can see what went ~
                                               wrong in the function ~
                                               assume-true-false.  The ~
                                               offending call was ~x0.  The ~
                                               surprising type-set arose from ~
                                               a call of ~x1."
                                                    (list 'assume-true-false
                                                      (kwote x)
                                                      '<xttree>
                                                      force-flg
                                                      (kwote type-alist)
                                                      '<ens>
                                                      '<w>)
                                                    (list 'assoc-equiv
                                                      (kwote equiv)
                                                      (kwote arg1-canon)
                                                      (kwote arg2-canon)
                                                      '<same_type-alist>))
                                                  nil
                                                  nil
                                                  nil
                                                  nil
                                                  nil
                                                  nil))
                                              ((ts= (cadr temp-temp) *ts-nil*) (mv-atf xnot-flg
                                                  nil
                                                  t
                                                  nil
                                                  type-alist
                                                  nil
                                                  (if (and canonicalp1 canonicalp2)
                                                    (cons-tag-trees (cddr temp-temp) xttree)
                                                    (puffert (cons-tag-trees (cddr temp-temp)
                                                        (cons-tag-trees ttree1 (cons-tag-trees ttree2 xttree)))))))
                                              (t (let ((erp (assume-true-false-error type-alist x (cadr temp-temp))))
                                                  (mv erp nil nil nil nil)))))
                                          (t (let ((swap-flg (term-order arg1-canon arg2-canon)) (xttree+ (if (and canonicalp1 canonicalp2)
                                                    xttree
                                                    (puffert (cons-tag-trees ttree1 (cons-tag-trees ttree2 xttree))))))
                                              (mv-atf xnot-flg
                                                nil
                                                nil
                                                (and (not (eq ignore :tta))
                                                  (extend-type-alist1 equiv
                                                    occursp1
                                                    occursp2
                                                    (and canonicalp1 canonicalp2)
                                                    arg1-canon
                                                    arg2-canon
                                                    swap-flg
                                                    x
                                                    *ts-t*
                                                    xttree+
                                                    type-alist))
                                                (and (not (eq ignore :fta))
                                                  (extend-type-alist1 equiv
                                                    occursp1
                                                    occursp2
                                                    (and canonicalp1 canonicalp2)
                                                    arg1-canon
                                                    arg2-canon
                                                    swap-flg
                                                    x
                                                    *ts-nil*
                                                    xttree+
                                                    type-alist))
                                                nil
                                                nil))))))))))))))))
                ((or (eq (ffn-symb x) 'car) (eq (ffn-symb x) 'cdr)) (mv-let (mbt mbf tta fta ttree)
                    (assume-true-false1 xnot-flg
                      x
                      xttree
                      force-flg
                      dwp
                      type-alist
                      ancestors
                      ens
                      w
                      pot-lst
                      pt
                      backchain-limit)
                    (cond ((or mbt mbf) (mv mbt mbf tta fta ttree))
                      (t (let ((tta (if xnot-flg
                               fta
                               tta)) (fta (if xnot-flg
                                tta
                                fta)))
                          (mv-let (mbt1 mbf tta1 fta1 ttree)
                            (assume-true-false-rec (fargn x 1)
                              xttree
                              force-flg
                              dwp
                              tta
                              ancestors
                              ens
                              w
                              pot-lst
                              pt
                              :fta backchain-limit)
                            (declare (ignore mbt1 fta1))
                            (mv-atf xnot-flg mbt mbf tta1 fta ttree nil)))))))
                ((eq (ffn-symb x) 'if) (assume-true-false-if xnot-flg
                    x
                    xttree
                    force-flg
                    dwp
                    type-alist
                    ancestors
                    ens
                    w
                    pot-lst
                    pt
                    backchain-limit))
                (t (assume-true-false1 xnot-flg
                    x
                    xttree
                    force-flg
                    dwp
                    type-alist
                    ancestors
                    ens
                    w
                    pot-lst
                    pt
                    backchain-limit)))))))))
  (defun assume-true-false1
    (not-flg x
      xttree
      force-flg
      dwp
      type-alist
      ancestors
      ens
      w
      pot-lst
      pt
      backchain-limit)
    (mv-let (ts ttree)
      (type-set-rec x
        force-flg
        dwp
        type-alist
        ancestors
        ens
        w
        nil
        pot-lst
        pt
        backchain-limit)
      (cond ((ts= ts *ts-nil*) (mv-atf not-flg nil t nil type-alist ttree xttree))
        ((ts-disjointp ts *ts-nil*) (mv-atf not-flg t nil type-alist nil ttree xttree))
        (t (mv-atf not-flg
            nil
            nil
            (extend-with-proper/improper-cons-ts-tuple x
              (ts-intersection ts *ts-non-nil*)
              (cons-tag-trees ttree xttree)
              force-flg
              dwp
              type-alist
              ancestors
              ens
              type-alist
              w
              pot-lst
              pt
              backchain-limit)
            (extend-type-alist-simple x *ts-nil* xttree type-alist)
            nil
            nil)))))
  (defun proper/improper-cons-ts-tuple
    (term ts
      ttree
      force-flg
      dwp
      type-alist
      ancestors
      ens
      wrld
      pot-lst
      pt
      backchain-limit)
    (cond ((and (ffn-symb-p term 'cons)
         (or (ts= ts *ts-proper-cons*) (ts= ts *ts-improper-cons*))) (let* ((x (non-cons-cdr term)))
          (mv-let (tsx ttreex)
            (type-set-rec x
              force-flg
              dwp
              type-alist
              ancestors
              ens
              wrld
              ttree
              pot-lst
              pt
              backchain-limit)
            (cond ((ts= ts *ts-proper-cons*) (mv x (ts-intersection tsx *ts-true-list*) ttreex))
              (t (mv x
                  (ts-intersection tsx (ts-complement *ts-true-list*))
                  ttreex))))))
      (t (mv term ts ttree))))
  (defun extend-with-proper/improper-cons-ts-tuple
    (term ts
      ttree
      force-flg
      dwp
      type-alist
      ancestors
      ens
      type-alist-to-be-extended
      wrld
      pot-lst
      pt
      backchain-limit)
    (mv-let (term ts ttree)
      (proper/improper-cons-ts-tuple term
        ts
        ttree
        force-flg
        dwp
        type-alist
        ancestors
        ens
        wrld
        pot-lst
        pt
        backchain-limit)
      (extend-type-alist term
        ts
        ttree
        type-alist-to-be-extended
        wrld))))

type-setfunction

(defun type-set
  (x force-flg dwp type-alist ens w ttree pot-lst pt)
  (let ((dwp (get-dwp dwp w)))
    (type-set-rec x
      force-flg
      dwp
      type-alist
      nil
      ens
      w
      ttree
      pot-lst
      pt
      (backchain-limit w :ts))))

type-set-bcfunction

(defun type-set-bc
  (x force-flg
    dwp
    type-alist
    ens
    w
    ttree
    pot-lst
    pt
    ts-backchain-limit)
  (let ((dwp (get-dwp dwp w)))
    (type-set-rec x
      force-flg
      dwp
      type-alist
      nil
      ens
      w
      ttree
      pot-lst
      pt
      ts-backchain-limit)))

other

(defstub assume-true-false-aggressive-p nil t)

other

(defattach assume-true-false-aggressive-p
  constant-nil-function-arity-0)

top-level-if-reduce-recfunction

(defun top-level-if-reduce-rec
  (test term not-flg ts)
  (cond ((ffn-symb-p term 'if) (cond ((equal test (fargn term 1)) (mv t
            (if not-flg
              (fargn term 3)
              (fargn term 2))))
        ((and (ffn-symb-p (fargn term 1) 'not)
           (equal test (fargn (fargn term 1) 1))) (mv t
            (if not-flg
              (fargn term 2)
              (fargn term 3))))
        (t (mv-let (changedp-tbr tbr)
            (top-level-if-reduce-rec test (fargn term 2) not-flg ts)
            (mv-let (changedp-fbr fbr)
              (top-level-if-reduce-rec test (fargn term 3) not-flg ts)
              (cond ((or changedp-tbr changedp-fbr) (mv t
                    (cond ((equal tbr fbr) tbr)
                      ((and (equal tbr *t*)
                         (equal fbr *nil*)
                         (ts= ts (ts-complement *ts-nil*))) (fargn term 1))
                      ((and (equal tbr *nil*)
                         (equal fbr *t*)
                         (ts= ts *nil*)
                         (ffn-symb-p (fargn term 1) 'not)) (fargn (fargn term 1) 1))
                      (t (fcons-term* 'if (fargn term 1) tbr fbr)))))
                (t (mv nil term))))))))
    (t (mv nil term))))

top-level-if-reducefunction

(defun top-level-if-reduce
  (test term not-flg ts)
  (mv-let (changedp val)
    (top-level-if-reduce-rec test term not-flg ts)
    (declare (ignore changedp))
    val))

top-level-if-pfunction

(defun top-level-if-p
  (test term)
  (cond ((ffn-symb-p term 'if) (or (equal test (fargn term 1))
        (and (ffn-symb-p (fargn term 1) 'not)
          (equal test (fargn (fargn term 1) 1)))
        (top-level-if-p test (fargn term 2))
        (top-level-if-p test (fargn term 3))))
    (t nil)))

type-alist-reducible-entriesfunction

(defun type-alist-reducible-entries
  (term type-alist bound)
  (cond ((or (endp type-alist) (and bound (zp bound))) nil)
    (t (let* ((rest-type-alist (cdr type-alist)) (bound-1 (and bound (1- bound)))
          (entry (car type-alist))
          (term2 (car entry)))
        (cond ((top-level-if-p term term2) (cons entry
              (type-alist-reducible-entries term rest-type-alist bound-1)))
          (t (type-alist-reducible-entries term rest-type-alist bound-1)))))))

assume-true-false-aggressive-1function

(defun assume-true-false-aggressive-1
  (entries tta fta x xttree wrld ignore0 not-flg)
  (cond ((endp entries) (mv nil nil tta fta nil))
    (t (let* ((entry (car entries)) (term (car entry))
          (ts (cadr entry))
          (new-ttree (cons-tag-trees xttree (cddr entry)))
          (new-tta (if (eq ignore0 :tta)
              tta
              (extend-type-alist (top-level-if-reduce x term not-flg ts)
                ts
                new-ttree
                tta
                wrld)))
          (new-fta (if (eq ignore0 :fta)
              fta
              (extend-type-alist (top-level-if-reduce x term (not not-flg) ts)
                ts
                new-ttree
                fta
                wrld))))
        (assume-true-false-aggressive-1 (cdr entries)
          new-tta
          new-fta
          x
          xttree
          wrld
          ignore0
          not-flg)))))

assume-true-false-aggressivefunction

(defun assume-true-false-aggressive
  (x xttree
    force-flg
    dwp
    type-alist
    ens
    w
    pot-lst
    pt
    ignore0
    ts-backchain-limit
    bound)
  (mv-let (mbt mbf tta fta ttree)
    (assume-true-false-rec x
      xttree
      force-flg
      dwp
      type-alist
      nil
      ens
      w
      pot-lst
      pt
      ignore0
      ts-backchain-limit)
    (cond ((or mbt mbf) (mv mbt mbf tta fta ttree))
      (t (mv-let (not-flg atm)
          (strip-not x)
          (let ((entries (type-alist-reducible-entries atm
                 type-alist
                 (and (natp bound) bound))))
            (assume-true-false-aggressive-1 entries
              (set-difference-equal tta entries)
              (set-difference-equal fta entries)
              atm
              xttree
              w
              ignore0
              not-flg)))))))

assume-true-falsefunction

(defun assume-true-false
  (x xttree force-flg dwp type-alist ens w pot-lst pt ignore0)
  (let ((bound (assume-true-false-aggressive-p)) (dwp (get-dwp dwp w)))
    (cond (bound (assume-true-false-aggressive x
          xttree
          force-flg
          dwp
          type-alist
          ens
          w
          pot-lst
          pt
          ignore0
          (backchain-limit w :ts)
          bound))
      (t (assume-true-false-rec x
          xttree
          force-flg
          dwp
          type-alist
          nil
          ens
          w
          pot-lst
          pt
          ignore0
          (backchain-limit w :ts))))))

assume-true-false-bcfunction

(defun assume-true-false-bc
  (x xttree
    force-flg
    dwp
    type-alist
    ens
    w
    pot-lst
    pt
    ignore0
    ts-backchain-limit)
  (let ((bound (assume-true-false-aggressive-p)) (dwp (get-dwp dwp w)))
    (cond (bound (assume-true-false-aggressive x
          xttree
          force-flg
          dwp
          type-alist
          ens
          w
          pot-lst
          pt
          ignore0
          ts-backchain-limit
          bound))
      (t (assume-true-false-rec x
          xttree
          force-flg
          dwp
          type-alist
          nil
          ens
          w
          pot-lst
          pt
          ignore0
          ts-backchain-limit)))))

ok-to-force-ensfunction

(defun ok-to-force-ens
  (ens)
  (and (enabled-numep *force-xnume* ens) t))

add-linear-assumptionfunction

(defun add-linear-assumption
  (target term
    type-alist
    ens
    immediatep
    force-flg
    wrld
    tag-tree)
  (mv-let (ts ttree)
    (type-set term
      force-flg
      nil
      type-alist
      ens
      wrld
      nil
      nil
      nil)
    (cond ((ts= ts *ts-nil*) (mv :known-false (cons-tag-trees ttree tag-tree)))
      ((ts-disjointp ts *ts-nil*) (mv :known-true (cons-tag-trees ttree tag-tree)))
      (t (mv-let (forced tag-tree)
          (cond ((not force-flg) (mv nil tag-tree))
            (t (force-assumption 'equal
                target
                term
                type-alist
                nil
                immediatep
                force-flg
                tag-tree)))
          (cond ((not forced) (mv :failed tag-tree))
            (t (mv :added tag-tree))))))))

return-type-alistfunction

(defun return-type-alist
  (hitp car-type-alist
    rest-type-alist
    original-type-alist
    wrld)
  (if hitp
    (mv-let (ts ttree)
      (assoc-type-alist (car car-type-alist) rest-type-alist wrld)
      (let* ((ts (or ts *ts-unknown*)) (int (ts-intersection ts (cadr car-type-alist))))
        (cond ((ts= int ts) rest-type-alist)
          ((ts= int (cadr car-type-alist)) (extend-type-alist (car car-type-alist)
              (cadr car-type-alist)
              (cddr car-type-alist)
              rest-type-alist
              wrld))
          (t (extend-type-alist (car car-type-alist)
              int
              (cons-tag-trees ttree (cddr car-type-alist))
              rest-type-alist
              wrld)))))
    original-type-alist))

type-alist-equality-loop1function

(defun type-alist-equality-loop1
  (type-alist top-level-type-alist ens w)
  (cond ((null type-alist) (mv nil nil nil))
    (t (mv-let (hitp rest-type-alist rest-ttree)
        (type-alist-equality-loop1 (cdr type-alist)
          top-level-type-alist
          ens
          w)
        (cond ((eq hitp 'contradiction) (mv hitp rest-type-alist rest-ttree))
          ((and (ffn-symb-p (caar type-alist) 'equal)
             (ts= (cadar type-alist) *ts-t*)) (let ((arg1 (fargn (caar type-alist) 1)) (arg2 (fargn (caar type-alist) 2))
                (ttree0 (cddar type-alist)))
              (mv-let (ts1 ttree)
                (type-set arg1
                  nil
                  nil
                  top-level-type-alist
                  ens
                  w
                  nil
                  nil
                  nil)
                (mv-let (ts2 ttree)
                  (type-set arg2
                    nil
                    nil
                    top-level-type-alist
                    ens
                    w
                    ttree
                    nil
                    nil)
                  (let ((int (ts-intersection ts1 ts2)))
                    (cond ((ts= int *ts-empty*) (mv 'contradiction nil (puffert ttree)))
                      ((ts= ts1 ts2) (mv hitp
                          (return-type-alist hitp
                            (car type-alist)
                            rest-type-alist
                            type-alist
                            w)
                          nil))
                      (t (mv t
                          (let ((shared-ttree (puffert (cons-tag-trees ttree0 ttree))) (type-alist (return-type-alist hitp
                                  (car type-alist)
                                  rest-type-alist
                                  type-alist
                                  w))
                              (backchain-limit (backchain-limit w :ts)))
                            (cond ((ts= ts1 int) (extend-with-proper/improper-cons-ts-tuple arg2
                                  int
                                  shared-ttree
                                  nil
                                  nil
                                  top-level-type-alist
                                  nil
                                  ens
                                  type-alist
                                  w
                                  nil
                                  nil
                                  backchain-limit))
                              ((ts= ts2 int) (extend-with-proper/improper-cons-ts-tuple arg1
                                  int
                                  shared-ttree
                                  nil
                                  nil
                                  top-level-type-alist
                                  nil
                                  ens
                                  type-alist
                                  w
                                  nil
                                  nil
                                  backchain-limit))
                              (t (extend-with-proper/improper-cons-ts-tuple arg2
                                  int
                                  shared-ttree
                                  nil
                                  nil
                                  top-level-type-alist
                                  nil
                                  ens
                                  (extend-with-proper/improper-cons-ts-tuple arg1
                                    int
                                    shared-ttree
                                    nil
                                    nil
                                    top-level-type-alist
                                    nil
                                    ens
                                    type-alist
                                    w
                                    nil
                                    nil
                                    backchain-limit)
                                  w
                                  nil
                                  nil
                                  backchain-limit))))
                          nil))))))))
          (t (mv hitp
              (return-type-alist hitp
                (car type-alist)
                rest-type-alist
                type-alist
                w)
              nil)))))))

clean-up-alistfunction

(defun clean-up-alist
  (alist ans)
  (cond ((null alist) ans)
    ((assoc-equal (caar alist) ans) (clean-up-alist (cdr alist) ans))
    (t (clean-up-alist (cdr alist) (cons (car alist) ans)))))

duplicate-keyspfunction

(defun duplicate-keysp
  (alist)
  (cond ((null alist) nil)
    ((assoc-equal (caar alist) (cdr alist)) (car alist))
    (t (duplicate-keysp (cdr alist)))))

clean-type-alistfunction

(defun clean-type-alist (type-alist) type-alist)

type-alist-equality-loop-exitfunction

(defun type-alist-equality-loop-exit
  (type-alist)
  (er hard
    'type-alist-equality-loop-exit
    "We're apparently in an infinite type-alist-equality-loop!  The ~
       offending type-alist is:~%~x0"
    type-alist))

*type-alist-equality-loop-max-depth*constant

(defconst *type-alist-equality-loop-max-depth* 10)

type-alist-equality-loopfunction

(defun type-alist-equality-loop
  (type-alist0 ens w n)
  (let ((type-alist (clean-type-alist type-alist0)))
    (mv-let (hitp type-alist ttree)
      (type-alist-equality-loop1 type-alist type-alist ens w)
      (cond ((eq hitp 'contradiction) (mv t nil ttree))
        ((= n 0) (if (or (not hitp) (equal type-alist type-alist0))
            (mv nil type-alist nil)
            (mv nil (type-alist-equality-loop-exit type-alist) nil)))
        (hitp (type-alist-equality-loop type-alist ens w (1- n)))
        (t (mv nil type-alist nil))))))

put-assoc-equal-tsfunction

(defun put-assoc-equal-ts
  (term ts ttree type-alist)
  (declare (xargs :guard (alistp type-alist)))
  (cond ((endp type-alist) (list (list* term ts ttree)))
    ((equal term (caar type-alist)) (let ((ts1 (ts-intersection ts (cadar type-alist))))
        (cond ((ts= ts1 (cadar type-alist)) type-alist)
          (t (cons (list* term ts ttree) (cdr type-alist))))))
    (t (cons (car type-alist)
        (put-assoc-equal-ts term ts ttree (cdr type-alist))))))

reconsider-type-alistfunction

(defun reconsider-type-alist
  (type-alist xtype-alist force-flg ens w pot-lst pt)
  (cond ((null type-alist) (mv nil xtype-alist nil))
    ((ffn-symb-p (caar type-alist) 'if) (reconsider-type-alist (cdr type-alist)
        xtype-alist
        force-flg
        ens
        w
        pot-lst
        pt))
    (t (mv-let (ts ttree)
        (type-set (caar type-alist)
          force-flg
          (cons :skip-lookup (cdar type-alist))
          xtype-alist
          ens
          w
          nil
          pot-lst
          pt)
        (cond ((ts= ts *ts-empty*) (mv t nil ttree))
          (t (reconsider-type-alist (cdr type-alist)
              (cond ((ts-subsetp (cadar type-alist) ts) xtype-alist)
                (t (put-assoc-equal-ts (caar type-alist) ts ttree xtype-alist)))
              force-flg
              ens
              w
              pot-lst
              pt)))))))

type-alist-clause-finish1function

(defun type-alist-clause-finish1
  (lits ttree-lst force-flg type-alist ens wrld)
  (cond ((null lits) (mv nil type-alist nil))
    (t (mv-let (mbt mbf tta fta ttree)
        (assume-true-false (car lits)
          (car ttree-lst)
          force-flg
          nil
          type-alist
          ens
          wrld
          nil
          nil
          :tta)
        (declare (ignore tta))
        (cond (mbt (mv t nil ttree))
          (mbf (type-alist-clause-finish1 (cdr lits)
              (cdr ttree-lst)
              force-flg
              type-alist
              ens
              wrld))
          (t (type-alist-clause-finish1 (cdr lits)
              (cdr ttree-lst)
              force-flg
              fta
              ens
              wrld)))))))

type-alist-clause-finishfunction

(defun type-alist-clause-finish
  (lits ttree-lst force-flg type-alist ens wrld pot-lst pt)
  (mv-let (contradictionp type-alist ttree)
    (type-alist-clause-finish1 lits
      ttree-lst
      force-flg
      type-alist
      ens
      wrld)
    (cond (contradictionp (mv contradictionp type-alist ttree))
      (t (mv-let (contradictionp new-type-alist ttree)
          (reconsider-type-alist type-alist
            type-alist
            force-flg
            ens
            wrld
            pot-lst
            pt)
          (cond (contradictionp (mv contradictionp new-type-alist ttree))
            ((or (equal new-type-alist type-alist) (null pot-lst)) (mv contradictionp new-type-alist ttree))
            (t (reconsider-type-alist new-type-alist
                new-type-alist
                force-flg
                ens
                wrld
                pot-lst
                pt))))))))

sort-lits-heavy-pmutual-recursion

(mutual-recursion (defun sort-lits-heavy-p
    (term)
    (declare (xargs :guard (pseudo-termp term)))
    (cond ((variablep term) term)
      ((fquotep term) nil)
      ((flambda-applicationp term) t)
      (t (sort-lits-heavy-listp (fargs term) nil))))
  (defun sort-lits-heavy-listp
    (lst var)
    (declare (xargs :guard (and (pseudo-term-listp lst) (symbolp var))))
    (cond ((endp lst) var)
      (t (let ((x1 (sort-lits-heavy-p (car lst))))
          (or (eq x1 t)
            (and x1 var (not (eq x1 var)))
            (sort-lits-heavy-listp (cdr lst) (or x1 var))))))))

sort-lits1function

(defun sort-lits1
  (cl ttree-lst)
  (cond ((endp cl) (mv nil nil nil nil))
    (t (mv-let (cl-pre ttree-lst-pre cl-post ttree-lst-post)
        (sort-lits1 (cdr cl) (cdr ttree-lst))
        (cond ((eq (sort-lits-heavy-p (car cl)) t) (mv cl-pre
              ttree-lst-pre
              (cons (car cl) cl-post)
              (cons (car ttree-lst) ttree-lst-post)))
          (t (mv (cons (car cl) cl-pre)
              (cons (car ttree-lst) ttree-lst-pre)
              cl-post
              ttree-lst-post)))))))

sort-litsfunction

(defun sort-lits
  (cl ttree-lst)
  (mv-let (cl-pre tree-lst-pre cl-post ttree-lst-post)
    (sort-lits1 cl ttree-lst)
    (mv (append? cl-pre cl-post)
      (append? tree-lst-pre ttree-lst-post))))

type-alist-clausefunction

(defun type-alist-clause
  (cl ttree-lst force-flg type-alist ens wrld pot-lst pt)
  (if force-flg
    (type-alist-clause-finish cl
      ttree-lst
      force-flg
      type-alist
      ens
      wrld
      pot-lst
      pt)
    (mv-let (contradictionp type-alist0 ttree0)
      (type-alist-clause-finish cl
        ttree-lst
        nil
        type-alist
        ens
        wrld
        pot-lst
        pt)
      (cond (contradictionp (mv t nil ttree0))
        (t (type-alist-equality-loop type-alist0
            ens
            wrld
            *type-alist-equality-loop-max-depth*))))))

known-whether-nilfunction

(defun known-whether-nil
  (x type-alist ens force-flg dwp wrld ttree)
  (cond ((quotep x) (mv t (equal x *nil*) ttree))
    (t (mv-let (ts ttree1)
        (type-set x force-flg dwp type-alist ens wrld ttree nil nil)
        (cond ((ts= ts *ts-nil*) (mv t t ttree1))
          ((ts-intersectp ts *ts-nil*) (mv nil nil ttree))
          (t (mv t nil ttree1)))))))

ts-booleanpfunction

(defun ts-booleanp
  (term ens wrld)
  (mv-let (ts ttree)
    (type-set term nil nil nil ens wrld nil nil nil)
    (cond ((tagged-objectsp 'assumption ttree) (er hard
          'ts-booleanp
          "It was thought impossible for a call of type-set with ~
                      force-flg = nil to produce an 'assumption, but ~
                      ts-booleanp did it on ~x0."
          term))
      (t (ts-subsetp ts *ts-boolean*)))))

weak-cons-occurfunction

(defun weak-cons-occur
  (x y)
  (cond ((variablep y) (eq x y))
    ((fquotep y) nil)
    ((eq (ffn-symb y) 'cons) (or (weak-cons-occur x (fargn y 1))
        (weak-cons-occur x (fargn y 2))))
    (t (equal x y))))

equal-x-cons-x-ypfunction

(defun equal-x-cons-x-yp
  (lhs rhs)
  (cond ((variablep lhs) (cond ((consityp rhs) (or (weak-cons-occur lhs (fargn rhs 1))
            (weak-cons-occur lhs (fargn rhs 2))))
        (t nil)))
    ((fquotep lhs) nil)
    ((eq (ffn-symb lhs) 'cons) (cond ((variablep rhs) (or (weak-cons-occur rhs (fargn lhs 1))
            (weak-cons-occur rhs (fargn lhs 2))))
        ((fquotep rhs) nil)
        ((eq (ffn-symb rhs) 'cons) nil)
        (t (or (weak-cons-occur rhs (fargn lhs 1))
            (weak-cons-occur rhs (fargn lhs 2))))))
    ((consityp rhs) (or (weak-cons-occur lhs (fargn rhs 1))
        (weak-cons-occur lhs (fargn rhs 2))))
    (t nil)))

not-identfunction

(defun not-ident
  (term1 term2 type-alist ens wrld)
  (cond ((and (quotep term1) (quotep term2)) (mv (not (equal term1 term2)) nil))
    (t (mv-let (ts1 ttree)
        (type-set term1 nil nil type-alist ens wrld nil nil nil)
        (mv-let (ts2 ttree)
          (type-set term2 nil nil type-alist ens wrld ttree nil nil)
          (cond ((ts-disjointp ts1 ts2) (mv t ttree))
            ((equal-x-cons-x-yp term1 term2) (mv t nil))
            (t (mv nil nil))))))))

first-iffunction

(defun first-if
  (args i)
  (cond ((null args) (mv nil nil))
    ((ffn-symb-p (car args) 'if) (mv i (car args)))
    (t (first-if (cdr args) (1+ i)))))

all-variablepfunction

(defun all-variablep
  (lst)
  (cond ((null lst) t)
    (t (and (variablep (car lst)) (all-variablep (cdr lst))))))

normalize-with-type-setfunction

(defun normalize-with-type-set
  (term iff-flg type-alist ens wrld ttree ts-backchain-limit)
  (mv-let (ts new-ttree)
    (type-set-bc term
      nil
      nil
      type-alist
      ens
      wrld
      ttree
      nil
      nil
      ts-backchain-limit)
    (let ((new-term (cond ((ts-intersectp ts *ts-nil*) (cond ((ts= ts *ts-nil*) *nil*) (t term)))
           (iff-flg *t*)
           ((ts= ts *ts-t*) *t*)
           ((ts= ts *ts-zero*) *0*)
           ((ts= ts *ts-one*) *1*)
           (t term))))
      (mv new-term
        (if (equal term new-term)
          ttree
          new-ttree)))))

normalizemutual-recursion

(mutual-recursion (defun normalize
    (term iff-flg type-alist ens wrld ttree ts-backchain-limit)
    (cond ((variablep term) (normalize-with-type-set term
          iff-flg
          type-alist
          ens
          wrld
          ttree
          ts-backchain-limit))
      ((fquotep term) (mv (cond ((and iff-flg (not (equal term *nil*))) *t*) (t term))
          ttree))
      ((flambda-applicationp term) (mv-let (normal-args ttree)
          (normalize-lst (fargs term)
            nil
            type-alist
            ens
            wrld
            ttree
            ts-backchain-limit)
          (mv-let (normal-body ttree)
            (normalize (lambda-body (ffn-symb term))
              iff-flg
              (zip-variable-type-alist (lambda-formals (ffn-symb term))
                (type-set-lst normal-args
                  nil
                  nil
                  type-alist
                  nil
                  ens
                  wrld
                  nil
                  nil
                  ts-backchain-limit))
              ens
              wrld
              ttree
              ts-backchain-limit)
            (mv (mcons-term (list 'lambda (lambda-formals (ffn-symb term)) normal-body)
                normal-args)
              ttree))))
      ((eq (ffn-symb term) 'if) (mv-let (t1 ttree)
          (normalize (fargn term 1)
            t
            type-alist
            ens
            wrld
            ttree
            ts-backchain-limit)
          (let ((t2 (fargn term 2)) (t3 (fargn term 3)))
            (mv-let (mbt mbf tta fta ttree1)
              (assume-true-false-bc t1
                nil
                nil
                nil
                type-alist
                ens
                wrld
                nil
                nil
                nil
                ts-backchain-limit)
              (cond (mbt (normalize t2
                    iff-flg
                    type-alist
                    ens
                    wrld
                    (cons-tag-trees ttree1 ttree)
                    ts-backchain-limit))
                (mbf (normalize t3
                    iff-flg
                    type-alist
                    ens
                    wrld
                    (cons-tag-trees ttree1 ttree)
                    ts-backchain-limit))
                ((ffn-symb-p t1 'if) (let ((t11 (fargn t1 1)) (t12 (fargn t1 2)) (t13 (fargn t1 3)))
                    (normalize (mcons-term* 'if
                        t11
                        (mcons-term* 'if t12 t2 t3)
                        (mcons-term* 'if t13 t2 t3))
                      iff-flg
                      type-alist
                      ens
                      wrld
                      ttree
                      ts-backchain-limit)))
                (t (mv-let (t2 ttree)
                    (normalize t2 iff-flg tta ens wrld ttree ts-backchain-limit)
                    (mv-let (t3 ttree)
                      (normalize t3 iff-flg fta ens wrld ttree ts-backchain-limit)
                      (cond ((equal t2 t3) (mv t2 ttree))
                        ((and (equal t1 t2) (equal t3 *nil*)) (mv t1 ttree))
                        ((and (equal t2 *t*) (equal t3 *nil*)) (cond (iff-flg (mv t1 ttree))
                            (t (mv-let (ts1 ttree1)
                                (type-set-bc t1
                                  nil
                                  nil
                                  type-alist
                                  ens
                                  wrld
                                  nil
                                  nil
                                  nil
                                  ts-backchain-limit)
                                (cond ((ts-subsetp ts1 *ts-boolean*) (mv t1 (cons-tag-trees ttree1 ttree)))
                                  (t (mv (mcons-term* 'if t1 t2 t3) ttree)))))))
                        (t (mv (mcons-term* 'if t1 t2 t3) ttree)))))))))))
      ((eq (ffn-symb term) 'hide) (mv term ttree))
      (t (mv-let (normal-args ttree)
          (normalize-lst (fargs term)
            nil
            type-alist
            ens
            wrld
            ttree
            ts-backchain-limit)
          (let ((term (cons-term (ffn-symb term) normal-args)))
            (cond ((fquotep term) (mv term ttree))
              ((eq (ffn-symb term) 'equal) (cond ((equal (fargn term 1) (fargn term 2)) (mv *t* ttree))
                  (t (mv-let (not-ident ttree1)
                      (not-ident (fargn term 1)
                        (fargn term 2)
                        type-alist
                        ens
                        wrld)
                      (cond (not-ident (mv *nil* (cons-tag-trees ttree1 ttree)))
                        (t (distribute-first-if term
                            iff-flg
                            type-alist
                            ens
                            wrld
                            ttree
                            ts-backchain-limit)))))))
              (t (distribute-first-if term
                  iff-flg
                  type-alist
                  ens
                  wrld
                  ttree
                  ts-backchain-limit))))))))
  (defun normalize-lst
    (args iff-flg type-alist ens wrld ttree ts-backchain-limit)
    (cond ((null args) (mv nil ttree))
      (t (mv-let (normal-arg ttree)
          (normalize (car args)
            iff-flg
            type-alist
            ens
            wrld
            ttree
            ts-backchain-limit)
          (mv-let (normal-args ttree)
            (normalize-lst (cdr args)
              iff-flg
              type-alist
              ens
              wrld
              ttree
              ts-backchain-limit)
            (mv (cons normal-arg normal-args) ttree))))))
  (defun normalize-or-distribute-first-if
    (term iff-flg type-alist ens wrld ttree ts-backchain-limit)
    (cond ((or (variablep term) (fquotep term)) (normalize term
          iff-flg
          type-alist
          ens
          wrld
          ttree
          ts-backchain-limit))
      ((eq (ffn-symb term) 'equal) (cond ((equal (fargn term 1) (fargn term 2)) (mv *t* ttree))
          (t (mv-let (not-ident ttree1)
              (not-ident (fargn term 1)
                (fargn term 2)
                type-alist
                ens
                wrld)
              (cond (not-ident (mv *nil* (cons-tag-trees ttree1 ttree)))
                (t (distribute-first-if term
                    iff-flg
                    type-alist
                    ens
                    wrld
                    ttree
                    ts-backchain-limit)))))))
      (t (distribute-first-if term
          iff-flg
          type-alist
          ens
          wrld
          ttree
          ts-backchain-limit))))
  (defun distribute-first-if
    (term iff-flg type-alist ens wrld ttree ts-backchain-limit)
    (mv-let (n if-expr)
      (first-if (fargs term) 0)
      (cond ((null n) (cond ((member-eq (ffn-symb term)
               *expandable-boot-strap-non-rec-fns*) (normalize (subcor-var (formals (ffn-symb term) wrld)
                  (fargs term)
                  (bbody (ffn-symb term)))
                iff-flg
                type-alist
                ens
                wrld
                ttree
                ts-backchain-limit))
            (t (normalize-with-type-set term
                iff-flg
                type-alist
                ens
                wrld
                ttree
                ts-backchain-limit))))
        (t (let ((t1 (fargn if-expr 1)))
            (mv-let (mbt mbf tta fta ttree1)
              (assume-true-false-bc t1
                nil
                nil
                nil
                type-alist
                ens
                wrld
                nil
                nil
                nil
                ts-backchain-limit)
              (cond (mbt (normalize-or-distribute-first-if (cons-term (ffn-symb term)
                      (subst-for-nth-arg (fargn if-expr 2) n (fargs term)))
                    iff-flg
                    type-alist
                    ens
                    wrld
                    (cons-tag-trees ttree1 ttree)
                    ts-backchain-limit))
                (mbf (normalize-or-distribute-first-if (cons-term (ffn-symb term)
                      (subst-for-nth-arg (fargn if-expr 3) n (fargs term)))
                    iff-flg
                    type-alist
                    ens
                    wrld
                    (cons-tag-trees ttree1 ttree)
                    ts-backchain-limit))
                (t (mv-let (t2 ttree)
                    (normalize-or-distribute-first-if (cons-term (ffn-symb term)
                        (subst-for-nth-arg (fargn if-expr 2) n (fargs term)))
                      iff-flg
                      tta
                      ens
                      wrld
                      ttree
                      ts-backchain-limit)
                    (mv-let (t3 ttree)
                      (normalize-or-distribute-first-if (cons-term (ffn-symb term)
                          (subst-for-nth-arg (fargn if-expr 3) n (fargs term)))
                        iff-flg
                        fta
                        ens
                        wrld
                        ttree
                        ts-backchain-limit)
                      (cond ((equal t2 t3) (mv t2 ttree))
                        ((and (equal t1 t2) (equal t3 *nil*)) (mv t1 ttree))
                        ((and (equal t2 *t*) (equal t3 *nil*)) (cond (iff-flg (mv t1 ttree))
                            (t (mv-let (ts1 ttree1)
                                (type-set-bc t1
                                  nil
                                  nil
                                  type-alist
                                  ens
                                  wrld
                                  nil
                                  nil
                                  nil
                                  ts-backchain-limit)
                                (cond ((ts-subsetp ts1 *ts-boolean*) (mv t1 (cons-tag-trees ttree1 ttree)))
                                  (t (mv (mcons-term* 'if t1 t2 t3) ttree)))))))
                        (t (mv (mcons-term* 'if t1 t2 t3) ttree))))))))))))))

decode-type-set1function

(defun decode-type-set1
  (ts alist)
  (cond ((ts= ts *ts-empty*) nil)
    ((null alist) (list ts))
    ((ts-subsetp (cdar alist) ts) (cons (caar alist)
        (decode-type-set1 (ts-intersection ts (ts-complement (cdar alist)))
          (cdr alist))))
    (t (decode-type-set1 ts (cdr alist)))))

decode-type-setfunction

(defun decode-type-set
  (ts)
  (cond ((ts= ts *ts-unknown*) '*ts-unknown*)
    ((ts= ts *ts-empty*) '*ts-empty*)
    ((ts-complementp ts) (list 'ts-complement (decode-type-set (ts-complement ts))))
    (t (let ((lst (decode-type-set1 ts *code-type-set-alist*)))
        (cond ((null (cdr lst)) (car lst)) (t (cons 'ts-union lst)))))))

dtsmacro

(defmacro dts
  (term type-alist)
  `(mv-let (ts ttree)
    (type-set ,TERM
      nil
      nil
      ,TYPE-ALIST
      (ens state)
      (w state)
      nil
      nil
      nil)
    (mv (decode-type-set ts) ttree)))

ensfunction

(defun ens
  (state)
  (declare (xargs :guard t))
  (f-get-global 'global-enabled-structure state))