• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Define-sk
      • Defines
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
        • Defmin-int-implementation
          • Defmin-int-fn
          • Defmin-int-macro-definition
          • Defmin-int-input-processing
          • Defmin-int-event-generation
            • Defmin-int-gen-everything
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Support
      • Defthm-signed-byte-p
      • Defthm-unsigned-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmin-int-event-generation

Defmin-int-gen-everything

Generate the top-level event.

Signature

(defmin-int-gen-everything f y x1...xn body guard verify-guards) 
  → 
event

Arguments

f — Guard (symbolp f).

y — Guard (symbolp y).

x1...xn — Guard (symbol-listp x1...xn).

verify-guards — Guard (booleanp verify-guards).

Returns

event — A pseudo-event-formp.

The events are generated inside an encapsulate. Some events are only local, just used to prove the first helper theorem f.existsp-when-nonempty-and-bounded. The exported theorems that have hints are generated first locally with the hints, then non-locally and redundantly without hints, to keep the history ``cleaner''.

Definitions and Theorems

Function: defmin-int-gen-everything

(defun defmin-int-gen-everything
       (f y x1...xn body guard verify-guards)
 (declare (xargs :guard (and (symbolp f)
                             (symbolp y)
                             (symbol-listp x1...xn)
                             (booleanp verify-guards))))
 (let ((__function__ 'defmin-int-gen-everything))
  (declare (ignorable __function__))
  (b*
   ((y0 (genvar y (symbol-name y)
                0 (list* y x1...xn)))
    (y1 (genvar y (symbol-name y)
                1 (list* y y0 x1...xn)))
    (x1...xn-y (rcons y x1...xn))
    (elementp (add-suffix-to-fn f ".ELEMENTP"))
    (lboundp (add-suffix-to-fn f ".LBOUNDP"))
    (existsp (add-suffix-to-fn f ".EXISTSP"))
    (existsp-witness (add-suffix-to-fn existsp "-WITNESS"))
    (lboundp-witness (add-suffix-to-fn lboundp "-WITNESS"))
    (lboundp-necc (add-suffix-to-fn lboundp "-NECC"))
    (existsp-suff (add-suffix-to-fn existsp "-SUFF"))
    (pkgwit (pkg-witness (symbol-package-name f)))
    (booleanp-of-lboundp (packn-pos (list 'booleanp-of lboundp)
                                    pkgwit))
    (booleanp-of-existsp (packn-pos (list 'booleanp-of existsp)
                                    pkgwit))
    (maybe-integerp-of-f (packn-pos (list 'maybe-integerp-of- f)
                                    pkgwit))
    (integerp-of-f-equal-existsp
         (packn-pos (list 'integerp-of- f '-equal- existsp)
                    pkgwit))
    (integerp-of-f-when-existsp
         (packn-pos (list 'integerp-of- f '-when- existsp)
                    pkgwit))
    (f-iff-existsp (packn-pos (list f '-iff- existsp)
                              pkgwit))
    (not-f-when-not-existsp
         (packn-pos (list 'not- f '-when-not- existsp)
                    pkgwit))
    (elementp-of-f-when-existsp
         (packn-pos (list elementp '-of- f '-when- existsp)
                    pkgwit))
    (lboundp-of-f-when-existsp
         (packn-pos (list lboundp '-of- f '-when- 'existsp)
                    pkgwit))
    (f-leq-when-existsp-linear
         (packn-pos (list f '-leq-when- existsp '-linear)
                    pkgwit))
    (f-leq-when-existsp-rewrite
         (packn-pos (list f '-leq-when- existsp '-rewrite)
                    pkgwit))
    (f-geq-when-existsp-linear
         (packn-pos (list f '-geq-when- existsp '-linear)
                    pkgwit))
    (f-geq-when-existsp-rewrite
         (packn-pos (list f '-geq-when- existsp '-rewrite)
                    pkgwit))
    (lbound-leq-member (packn-pos (list f '.lbound-leq-member)
                                  pkgwit))
    (lbound-nonmember-gt-member
         (packn-pos (list f '.lbound-nonmember-gt-member)
                    pkgwit))
    (find-min (packn-pos (list f '.find-min) pkgwit))
    (find-min-lboundp-preservation
         (packn-pos (list f '.find-min-lboundp-preservation)
                    pkgwit))
    (elementp-of-find-min (packn-pos (list f '.elementp-of-find-min)
                                     pkgwit))
    (lboundp-of-find-min (packn-pos (list f '.lboundp-of-find-min)
                                    pkgwit))
    (existsp-when-nonempty-and-bounded
         (packn-pos (list f '.existsp-when-nonempty-and-bounded)
                    pkgwit))
    (equal-when-member-and-lbound
         (packn-pos (list f '.equal-when-member-and-lbound)
                    pkgwit))
    (elementp-events
     (cons
      (cons
       'defun
       (cons
        elementp
        (cons
         x1...xn-y
         (cons
          (cons
           'declare
           (cons
            (cons
             'xargs
             (cons
              ':guard
              (cons (cons 'and
                          (cons guard
                                (cons (cons 'integerp (cons y 'nil))
                                      'nil)))
                    'nil)))
            'nil))
          (cons body 'nil)))))
      (append (and verify-guards
                   (cons (cons 'verify-guards
                               (cons elementp 'nil))
                         'nil))
              (cons (cons 'in-theory
                          (cons (cons 'disable (cons elementp 'nil))
                                'nil))
                    'nil))))
    (lboundp-events
     (cons
      (cons
       'defun-sk
       (cons
        lboundp
        (cons
         x1...xn-y
         (cons
          (cons
           'declare
           (cons
            (cons
             'xargs
             (cons
              ':guard
              (cons (cons 'and
                          (cons guard
                                (cons (cons 'integerp (cons y 'nil))
                                      'nil)))
                    '(:verify-guards nil))))
            'nil))
          (cons
           (cons
            'forall
            (cons
             (cons y1 'nil)
             (cons
              (cons
               'impliez
               (cons
                (cons
                  'and
                  (cons (cons 'integerp (cons y1 'nil))
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil)))
                (cons (cons '<=
                            (cons (cons 'ifix (cons y 'nil))
                                  (cons y1 'nil)))
                      'nil)))
              'nil)))
           (cons
            ':rewrite
            (cons
             (cons
              'implies
              (cons
               (cons
                'and
                (cons
                  (cons lboundp x1...xn-y)
                  (cons (cons 'integerp (cons y1 'nil))
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil))))
               (cons (cons '<=
                           (cons (cons 'ifix (cons y 'nil))
                                 (cons y1 'nil)))
                     'nil)))
             'nil)))))))
      (append
       (and verify-guards
            (cons (cons 'verify-guards
                        (cons lboundp 'nil))
                  'nil))
       (cons
        (cons
             'defthm
             (cons booleanp-of-lboundp
                   (cons (cons 'booleanp
                               (cons (cons lboundp x1...xn-y) 'nil))
                         'nil)))
        (cons
          (cons 'in-theory
                (cons (cons 'disable
                            (cons lboundp (cons lboundp-necc 'nil)))
                      'nil))
          'nil)))))
    (existsp-events
     (cons
      (cons
       'defun-sk
       (cons
        existsp
        (cons
         x1...xn
         (cons
          (cons
              'declare
              (cons (cons 'xargs
                          (cons ':guard
                                (cons guard '(:verify-guards nil))))
                    'nil))
          (cons
           (cons
            'exists
            (cons
             (cons y 'nil)
             (cons
              (cons
                 'and
                 (cons (cons 'integerp (cons y 'nil))
                       (cons (cons elementp x1...xn-y)
                             (cons (cons lboundp x1...xn-y) 'nil))))
              'nil)))
           'nil)))))
      (append
       (and verify-guards
            (cons (cons 'verify-guards
                        (cons existsp 'nil))
                  'nil))
       (cons
        (cons 'defthm
              (cons booleanp-of-existsp
                    (cons (cons 'booleanp
                                (cons (cons existsp x1...xn) 'nil))
                          'nil)))
        (cons
          (cons 'in-theory
                (cons (cons 'disable
                            (cons existsp (cons existsp-suff 'nil)))
                      'nil))
          'nil)))))
    (f-events
     (cons
      (cons
       'defun
       (cons
        f
        (cons
         x1...xn
         (cons
              (cons 'declare
                    (cons (cons 'xargs
                                (cons ':guard (cons guard 'nil)))
                          'nil))
              (cons (cons 'if
                          (cons (cons existsp x1...xn)
                                (cons (cons existsp-witness x1...xn)
                                      '(nil))))
                    'nil)))))
      (append
       (and verify-guards
            (cons (cons 'verify-guards (cons f 'nil))
                  'nil))
       (append
        (and
         (null x1...xn)
         (cons
             (cons 'in-theory
                   (cons (cons 'disable
                               (cons (cons ':e (cons f 'nil)) 'nil))
                         'nil))
             'nil))
        (cons
         (cons
          'local
          (cons
           (cons
            'defthm
            (cons
             maybe-integerp-of-f
             (cons
              (cons 'maybe-integerp
                    (cons (cons f x1...xn) 'nil))
              (cons
               ':hints
               (cons
                (cons
                 (cons '"Goal"
                       (cons ':in-theory
                             (cons (cons 'enable
                                         (cons 'maybe-integerp
                                               (cons existsp 'nil)))
                                   'nil)))
                 'nil)
                'nil)))))
           'nil))
         (cons
          (cons 'defthm
                (cons maybe-integerp-of-f
                      (cons (cons 'maybe-integerp
                                  (cons (cons f x1...xn) 'nil))
                            'nil)))
          (cons
           (cons
            'local
            (cons
             (cons
              'defthm
              (cons
               integerp-of-f-equal-existsp
               (cons
                (cons 'equal
                      (cons (cons 'integerp
                                  (cons (cons f x1...xn) 'nil))
                            (cons (cons existsp x1...xn) 'nil)))
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                      '"Goal"
                      (cons ':in-theory
                            (cons (cons 'enable (cons existsp 'nil))
                                  'nil)))
                   'nil)
                  'nil)))))
             'nil))
           (cons
            (cons
             'defthm
             (cons
              integerp-of-f-equal-existsp
              (cons (cons 'equal
                          (cons (cons 'integerp
                                      (cons (cons f x1...xn) 'nil))
                                (cons (cons existsp x1...xn) 'nil)))
                    'nil)))
            (cons
             (cons
              'defthm
              (cons
               integerp-of-f-when-existsp
               (cons
                (cons
                     'implies
                     (cons (cons existsp x1...xn)
                           (cons (cons 'integerp
                                       (cons (cons f x1...xn) 'nil))
                                 'nil)))
                '(:rule-classes :type-prescription))))
             (cons
              (cons
               'local
               (cons
                (cons
                 'defthm
                 (cons
                  f-iff-existsp
                  (cons
                   (cons 'iff
                         (cons (cons f x1...xn)
                               (cons (cons existsp x1...xn) 'nil)))
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons
                            ':in-theory
                            (cons (cons 'enable (cons existsp 'nil))
                                  'nil)))
                      'nil)
                     'nil)))))
                'nil))
              (cons
               (cons
                'defthm
                (cons
                 f-iff-existsp
                 (cons
                    (cons 'iff
                          (cons (cons f x1...xn)
                                (cons (cons existsp x1...xn) 'nil)))
                    'nil)))
               (cons
                (cons
                 'defthm
                 (cons
                  not-f-when-not-existsp
                  (cons
                   (cons
                    'implies
                    (cons
                      (cons 'not
                            (cons (cons existsp x1...xn) 'nil))
                      (cons (cons 'not (cons (cons f x1...xn) 'nil))
                            'nil)))
                   '(:rule-classes :type-prescription))))
                (cons
                 (cons
                  'local
                  (cons
                   (cons
                    'defthm
                    (cons
                     elementp-of-f-when-existsp
                     (cons
                      (cons
                       'implies
                       (cons
                        (cons existsp x1...xn)
                        (cons
                         (cons
                          elementp
                          (append
                              x1...xn (cons (cons f x1...xn) 'nil)))
                         'nil)))
                      (cons
                       ':hints
                       (cons
                        (cons
                         (cons
                          '"Goal"
                          (cons
                            ':in-theory
                            (cons (cons 'enable (cons existsp 'nil))
                                  'nil)))
                         'nil)
                        'nil)))))
                   'nil))
                 (cons
                  (cons
                   'defthm
                   (cons
                    elementp-of-f-when-existsp
                    (cons
                     (cons
                      'implies
                      (cons
                       (cons existsp x1...xn)
                       (cons
                        (cons
                         elementp
                         (append
                              x1...xn (cons (cons f x1...xn) 'nil)))
                        'nil)))
                     'nil)))
                  (cons
                   (cons
                    'local
                    (cons
                     (cons
                      'defthm
                      (cons
                       lboundp-of-f-when-existsp
                       (cons
                        (cons
                         'implies
                         (cons
                          (cons existsp x1...xn)
                          (cons
                           (cons
                            lboundp
                            (append
                              x1...xn (cons (cons f x1...xn) 'nil)))
                           'nil)))
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                                  (cons 'enable (cons existsp 'nil))
                                  'nil)))
                           'nil)
                          'nil)))))
                     'nil))
                   (cons
                    (cons
                     'defthm
                     (cons
                      lboundp-of-f-when-existsp
                      (cons
                       (cons
                        'implies
                        (cons
                         (cons existsp x1...xn)
                         (cons
                          (cons
                           lboundp
                           (append
                              x1...xn (cons (cons f x1...xn) 'nil)))
                          'nil)))
                       'nil)))
                    (cons
                     (cons
                      'local
                      (cons
                       (cons
                        'defthm
                        (cons
                         f-leq-when-existsp-linear
                         (cons
                          (cons
                           'implies
                           (cons
                            (cons
                             'and
                             (cons
                              (cons existsp x1...xn)
                              (cons
                               (cons
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                               (cons (cons 'integerp (cons y1 'nil))
                                     'nil))))
                            (cons (cons '<=
                                        (cons (cons f x1...xn)
                                              (cons y1 'nil)))
                                  'nil)))
                          (cons
                           ':rule-classes
                           (cons
                            ':linear
                            (cons
                             ':hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':in-theory
                                 (cons
                                  (cons 'disable (cons f 'nil))
                                  (cons
                                   ':use
                                   (cons
                                    (cons
                                     lboundp-of-f-when-existsp
                                     (cons
                                      (cons
                                       ':instance
                                       (cons
                                        lboundp-necc
                                        (cons
                                         (cons
                                              y
                                              (cons (cons f x1...xn)
                                                    'nil))
                                         'nil)))
                                      'nil))
                                    'nil)))))
                               'nil)
                              'nil)))))))
                       'nil))
                     (cons
                      (cons
                       'defthm
                       (cons
                        f-leq-when-existsp-linear
                        (cons
                         (cons
                          'implies
                          (cons
                           (cons
                            'and
                            (cons
                             (cons existsp x1...xn)
                             (cons
                              (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              (cons (cons 'integerp (cons y1 'nil))
                                    'nil))))
                           (cons
                            (cons
                             '<=
                             (cons (cons f x1...xn) (cons y1 'nil)))
                            'nil)))
                         '(:rule-classes :linear))))
                      (cons
                       (cons
                        'local
                        (cons
                         (cons
                          'defthm
                          (cons
                           f-leq-when-existsp-rewrite
                           (cons
                            (cons
                             'implies
                             (cons
                              (cons
                               'and
                               (cons
                                (cons existsp x1...xn)
                                (cons
                                 (cons
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                                 (cons
                                     (cons 'integerp (cons y1 'nil))
                                     'nil))))
                              (cons (cons '<=
                                          (cons (cons f x1...xn)
                                                (cons y1 'nil)))
                                    'nil)))
                            (cons
                             ':hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':by
                                 (cons
                                   f-leq-when-existsp-linear 'nil)))
                               'nil)
                              'nil)))))
                         'nil))
                       (cons
                        (cons
                         'defthm
                         (cons
                          f-leq-when-existsp-rewrite
                          (cons
                           (cons
                            'implies
                            (cons
                             (cons
                              'and
                              (cons
                               (cons existsp x1...xn)
                               (cons
                                (cons
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                                (cons
                                     (cons 'integerp (cons y1 'nil))
                                     'nil))))
                             (cons (cons '<=
                                         (cons (cons f x1...xn)
                                               (cons y1 'nil)))
                                   'nil)))
                           'nil)))
                        (cons
                         (cons
                          'local
                          (cons
                           (cons
                            'defthm
                            (cons
                             f-geq-when-existsp-linear
                             (cons
                              (cons
                               'implies
                               (cons
                                (cons
                                 'and
                                 (cons
                                  (cons existsp x1...xn)
                                  (cons
                                   (cons
                                    lboundp
                                    (append x1...xn (cons y1 'nil)))
                                   (cons
                                     (cons 'integerp (cons y1 'nil))
                                     'nil))))
                                (cons (cons '>=
                                            (cons (cons f x1...xn)
                                                  (cons y1 'nil)))
                                      'nil)))
                              (cons
                               ':rule-classes
                               (cons
                                ':linear
                                (cons
                                 ':hints
                                 (cons
                                  (cons
                                   (cons
                                    '"Goal"
                                    (cons
                                     ':in-theory
                                     (cons
                                      (cons 'disable (cons f 'nil))
                                      (cons
                                       ':use
                                       (cons
                                        (cons
                                         ':instance
                                         (cons
                                          lboundp-necc
                                          (cons
                                           (cons
                                              y1
                                              (cons (cons f x1...xn)
                                                    'nil))
                                           (cons
                                             (cons y (cons y1 'nil))
                                             'nil))))
                                        'nil)))))
                                   'nil)
                                  'nil)))))))
                           'nil))
                         (cons
                          (cons
                           'defthm
                           (cons
                            f-geq-when-existsp-linear
                            (cons
                             (cons
                              'implies
                              (cons
                               (cons
                                'and
                                (cons
                                 (cons existsp x1...xn)
                                 (cons
                                  (cons
                                    lboundp
                                    (append x1...xn (cons y1 'nil)))
                                  (cons
                                     (cons 'integerp (cons y1 'nil))
                                     'nil))))
                               (cons (cons '>=
                                           (cons (cons f x1...xn)
                                                 (cons y1 'nil)))
                                     'nil)))
                             '(:rule-classes :linear))))
                          (cons
                           (cons
                            'local
                            (cons
                             (cons
                              'defthm
                              (cons
                               f-geq-when-existsp-rewrite
                               (cons
                                (cons
                                 'implies
                                 (cons
                                  (cons
                                   'and
                                   (cons
                                    (cons existsp x1...xn)
                                    (cons
                                     (cons
                                       lboundp
                                       (append
                                            x1...xn (cons y1 'nil)))
                                     (cons (cons 'integerp
                                                 (cons y1 'nil))
                                           'nil))))
                                  (cons (cons '>=
                                              (cons (cons f x1...xn)
                                                    (cons y1 'nil)))
                                        'nil)))
                                (cons
                                 ':hints
                                 (cons
                                  (cons
                                   (cons
                                    '"Goal"
                                    (cons
                                     ':by
                                     (cons f-geq-when-existsp-linear
                                           'nil)))
                                   'nil)
                                  'nil)))))
                             'nil))
                           (cons
                            (cons
                             'defthm
                             (cons
                              f-geq-when-existsp-rewrite
                              (cons
                               (cons
                                'implies
                                (cons
                                 (cons
                                  'and
                                  (cons
                                   (cons existsp x1...xn)
                                   (cons
                                    (cons
                                       lboundp
                                       (append
                                            x1...xn (cons y1 'nil)))
                                    (cons
                                     (cons 'integerp (cons y1 'nil))
                                     'nil))))
                                 (cons (cons '>=
                                             (cons (cons f x1...xn)
                                                   (cons y1 'nil)))
                                       'nil)))
                               'nil)))
                            (cons
                             (cons
                                 'in-theory
                                 (cons (cons 'disable (cons f 'nil))
                                       'nil))
                             'nil)))))))))))))))))))))))))
    (existsp-when-non-empty-and-bounded-events
     (cons
      (cons
       'local
       (cons
        (cons
         'defthm
         (cons
          lbound-leq-member
          (cons
           (cons
            'implies
            (cons
             (cons
              'and
              (cons
               (cons 'integerp (cons y0 'nil))
               (cons
                (cons elementp
                      (append x1...xn (cons y0 'nil)))
                (cons
                 (cons 'integerp (cons y1 'nil))
                 (cons
                      (cons lboundp (append x1...xn (cons y1 'nil)))
                      'nil)))))
             (cons (cons '<= (cons y1 (cons y0 'nil)))
                   'nil)))
           (cons
            ':rule-classes
            (cons
             'nil
             (cons
              ':hints
              (cons
               (cons
                (cons
                 '"Goal"
                 (cons
                  ':use
                  (cons
                   (cons
                    ':instance
                    (cons
                       lboundp-necc
                       (cons (cons y (cons y1 'nil))
                             (cons (cons y1 (cons y0 'nil)) 'nil))))
                   'nil)))
                'nil)
               'nil)))))))
        'nil))
      (cons
       (cons
        'local
        (cons
         (cons
          'defthm
          (cons
           lbound-nonmember-gt-member
           (cons
            (cons
             'implies
             (cons
              (cons
               'and
               (cons
                (cons 'integerp (cons y0 'nil))
                (cons
                 (cons elementp
                       (append x1...xn (cons y0 'nil)))
                 (cons
                  (cons 'integerp (cons y1 'nil))
                  (cons
                   (cons lboundp (append x1...xn (cons y1 'nil)))
                   (cons
                    (cons
                        'not
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil))
                    'nil))))))
              (cons (cons '< (cons y1 (cons y0 'nil)))
                    'nil)))
            (cons
             ':rule-classes
             (cons
              'nil
              (cons
               ':hints
               (cons
                   (cons (cons '"Goal"
                               (cons ':use
                                     (cons lbound-leq-member 'nil)))
                         'nil)
                   'nil)))))))
         'nil))
       (cons
        (cons
         'local
         (cons
          (cons
           'defun
           (cons
            find-min
            (cons
             (append x1...xn (cons y1 (cons y0 'nil)))
             (cons
              (cons
               'declare
               (cons
                (cons
                 'xargs
                 (cons
                  ':measure
                  (cons
                   (cons 'nfix
                         (cons (cons '- (cons y0 (cons y1 'nil)))
                               'nil))
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons
                            ':use
                            (cons lbound-nonmember-gt-member 'nil)))
                      'nil)
                     'nil)))))
                'nil))
              (cons
               (cons
                'if
                (cons
                 (cons
                  'and
                  (cons
                   (cons 'integerp (cons y0 'nil))
                   (cons
                    (cons elementp
                          (append x1...xn (cons y0 'nil)))
                    (cons
                     (cons 'integerp (cons y1 'nil))
                     (cons
                      (cons lboundp (append x1...xn (cons y1 'nil)))
                      'nil)))))
                 (cons
                  (cons
                   'if
                   (cons
                    (cons elementp
                          (append x1...xn (cons y1 'nil)))
                    (cons
                     y1
                     (cons
                       (cons find-min
                             (append x1...xn
                                     (cons (cons '1+ (cons y1 'nil))
                                           (cons y0 'nil))))
                       'nil))))
                  '(0))))
               'nil)))))
          'nil))
        (cons
         (cons
          'local
          (cons
           (cons
            'defthm
            (cons
             find-min-lboundp-preservation
             (cons
              (cons
               'implies
               (cons
                (cons
                 'and
                 (cons
                  (cons 'integerp (cons y0 'nil))
                  (cons
                   (cons elementp
                         (append x1...xn (cons y0 'nil)))
                   (cons
                    (cons 'integerp (cons y1 'nil))
                    (cons
                     (cons lboundp (append x1...xn (cons y1 'nil)))
                     (cons
                      (cons
                        'not
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil))
                      'nil))))))
                (cons
                 (cons
                     lboundp
                     (append x1...xn
                             (cons (cons '1+ (cons y1 'nil)) 'nil)))
                 'nil)))
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':expand
                   (cons
                    (cons
                     (cons
                        lboundp
                        (append
                             x1...xn
                             (cons (cons '1+ (cons y1 'nil)) 'nil)))
                     'nil)
                    (cons
                     ':use
                     (cons
                      (cons
                       ':instance
                       (cons
                        lboundp-necc
                        (cons
                         (cons y (cons y1 'nil))
                         (cons
                          (cons
                           y1
                           (cons
                            (cons
                             lboundp-witness
                             (append x1...xn
                                     (cons (cons '1+ (cons y1 'nil))
                                           'nil)))
                            'nil))
                          'nil))))
                      'nil)))))
                 'nil)
                'nil)))))
           'nil))
         (cons
          (cons
           'local
           (cons
            (cons
             'defthm
             (cons
              elementp-of-find-min
              (cons
               (cons
                'implies
                (cons
                 (cons
                  'and
                  (cons
                   (cons 'integerp (cons y0 'nil))
                   (cons
                    (cons elementp
                          (append x1...xn (cons y0 'nil)))
                    (cons
                     (cons 'integerp (cons y1 'nil))
                     (cons
                      (cons lboundp (append x1...xn (cons y1 'nil)))
                      'nil)))))
                 (cons
                  (cons
                   elementp
                   (append
                    x1...xn
                    (cons
                     (cons
                          find-min
                          (append x1...xn (cons y1 (cons y0 'nil))))
                     'nil)))
                  'nil)))
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                   'quote
                   (cons
                    (cons
                     ':use
                     (cons
                      (cons
                           ':instance
                           (cons lboundp-necc
                                 (cons (cons y (cons y1 'nil))
                                       (cons (cons y1 '(0)) 'nil))))
                      'nil))
                    'nil))
                  (cons
                   (cons
                    'quote
                    (cons
                     (cons
                      ':use
                      (cons
                       (cons
                        ':instance
                        (cons
                         lboundp-necc
                         (cons
                             (cons y '(0))
                             (cons (cons y1 (cons y0 'nil)) 'nil))))
                       'nil))
                     'nil))
                   'nil))
                 'nil)))))
            'nil))
          (cons
           (cons
            'local
            (cons
             (cons
              'defthm
              (cons
               lboundp-of-find-min
               (cons
                (cons
                 'implies
                 (cons
                  (cons
                   'and
                   (cons
                    (cons 'integerp (cons y0 'nil))
                    (cons
                     (cons elementp
                           (append x1...xn (cons y0 'nil)))
                     (cons
                      (cons 'integerp (cons y1 'nil))
                      (cons
                       (cons
                            lboundp (append x1...xn (cons y1 'nil)))
                       'nil)))))
                  (cons
                   (cons
                    lboundp
                    (append
                     x1...xn
                     (cons
                      (cons
                          find-min
                          (append x1...xn (cons y1 (cons y0 'nil))))
                      'nil)))
                   'nil)))
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    'quote
                    (cons
                     (cons
                      ':use
                      (cons
                       (cons
                           ':instance
                           (cons lboundp-necc
                                 (cons (cons y (cons y1 'nil))
                                       (cons (cons y1 '(0)) 'nil))))
                       'nil))
                     'nil))
                   (cons
                    (cons
                     'quote
                     (cons
                      (cons
                       ':use
                       (cons
                        (cons
                         ':instance
                         (cons
                          lboundp-necc
                          (cons
                             (cons y '(0))
                             (cons (cons y1 (cons y0 'nil)) 'nil))))
                        'nil))
                      'nil))
                    'nil))
                  'nil)))))
             'nil))
           (cons
            (cons
             'local
             (cons
              (cons
               'defthm
               (cons
                existsp-when-nonempty-and-bounded
                (cons
                 (cons
                  'implies
                  (cons
                   (cons
                    'and
                    (cons
                     (cons 'integerp (cons y0 'nil))
                     (cons
                      (cons elementp
                            (append x1...xn (cons y0 'nil)))
                      (cons
                       (cons 'integerp (cons y1 'nil))
                       (cons
                        (cons
                            lboundp (append x1...xn (cons y1 'nil)))
                        'nil)))))
                   (cons (cons existsp x1...xn) 'nil)))
                 (cons
                  ':rule-classes
                  (cons
                   'nil
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons
                        ':use
                        (cons
                         (cons
                          ':instance
                          (cons
                           existsp-suff
                           (cons
                            (cons
                             y
                             (cons
                              (cons
                               find-min
                               (append
                                  x1...xn (cons y1 (cons y0 'nil))))
                              'nil))
                            'nil)))
                         'nil)))
                      'nil)
                     'nil)))))))
              'nil))
            (cons
             (cons
              'defthm
              (cons
               existsp-when-nonempty-and-bounded
               (cons
                (cons
                 'implies
                 (cons
                  (cons
                   'and
                   (cons
                    (cons 'integerp (cons y0 'nil))
                    (cons
                     (cons elementp
                           (append x1...xn (cons y0 'nil)))
                     (cons
                      (cons 'integerp (cons y1 'nil))
                      (cons
                       (cons
                            lboundp (append x1...xn (cons y1 'nil)))
                       'nil)))))
                  (cons (cons existsp x1...xn) 'nil)))
                '(:rule-classes nil))))
             'nil)))))))))
    (equal-when-member-and-bound
     (cons
      (cons
       'local
       (cons
        (cons
         'defthm
         (cons
          equal-when-member-and-lbound
          (cons
           (cons
            'implies
            (cons
             (cons
              'and
              (cons
               (cons 'integerp (cons y 'nil))
               (cons
                 (cons elementp (append x1...xn (cons y 'nil)))
                 (cons (cons lboundp (append x1...xn (cons y 'nil)))
                       'nil))))
             (cons (cons 'equal
                         (cons (cons f x1...xn) (cons y 'nil)))
                   'nil)))
           (cons
            ':rule-classes
            (cons
             'nil
             (cons
              ':hints
              (cons
               (cons
                (cons
                 '"Goal"
                 (cons
                  ':in-theory
                  (cons
                   (cons
                      'disable
                      (cons f-leq-when-existsp-rewrite
                            (cons f-geq-when-existsp-rewrite 'nil)))
                   (cons
                    ':use
                    (cons
                     (cons
                      (cons
                       ':instance
                       (cons
                        existsp-when-nonempty-and-bounded
                        (cons (cons y0 (cons y 'nil))
                              (cons (cons y1 (cons y 'nil)) 'nil))))
                      (cons
                       (cons
                         ':instance
                         (cons f-leq-when-existsp-rewrite
                               (cons (cons y1 (cons y 'nil)) 'nil)))
                       (cons
                        (cons
                         ':instance
                         (cons
                          lboundp-necc
                          (cons
                              (cons y1 (cons (cons f x1...xn) 'nil))
                              'nil)))
                        'nil)))
                     'nil)))))
                'nil)
               'nil)))))))
        'nil))
      (cons
       (cons
        'defthm
        (cons
         equal-when-member-and-lbound
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons 'integerp (cons y 'nil))
              (cons
                 (cons elementp (append x1...xn (cons y 'nil)))
                 (cons (cons lboundp (append x1...xn (cons y 'nil)))
                       'nil))))
            (cons (cons 'equal
                        (cons (cons f x1...xn) (cons y 'nil)))
                  'nil)))
          '(:rule-classes nil))))
       'nil))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(set-verify-guards-eagerness 0)
      (append
       elementp-events
       (append
        lboundp-events
        (append
           existsp-events
           (append f-events
                   (append existsp-when-non-empty-and-bounded-events
                           equal-when-member-and-bound)))))))))))