• 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
      • Defines
      • Define-sk
      • Error-value-tuples
      • Defmax-nat
        • Defmax-nat-implementation
          • Defmax-nat-fn
          • Defmax-nat-macro-definition
          • Defmax-nat-input-processing
          • Defmax-nat-event-generation
            • Defmax-nat-gen-everything
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Defthm-unsigned-byte-p
      • Support
      • Defthm-signed-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmax-nat-event-generation

Defmax-nat-gen-everything

Generate the top-level event.

Signature

(defmax-nat-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: defmax-nat-gen-everything

(defun defmax-nat-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__ 'defmax-nat-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"))
    (uboundp (add-suffix-to-fn f ".UBOUNDP"))
    (existsp (add-suffix-to-fn f ".EXISTSP"))
    (existsp-witness (add-suffix-to-fn existsp "-WITNESS"))
    (uboundp-witness (add-suffix-to-fn uboundp "-WITNESS"))
    (uboundp-necc (add-suffix-to-fn uboundp "-NECC"))
    (existsp-suff (add-suffix-to-fn existsp "-SUFF"))
    (pkgwit (pkg-witness (symbol-package-name f)))
    (booleanp-of-uboundp (packn-pos (list 'booleanp-of uboundp)
                                    pkgwit))
    (booleanp-of-existsp (packn-pos (list 'booleanp-of existsp)
                                    pkgwit))
    (maybe-natp-of-f (packn-pos (list 'maybe-natp-of- f)
                                pkgwit))
    (natp-of-f-equal-existsp
         (packn-pos (list 'natp-of- f '-equal- existsp)
                    pkgwit))
    (natp-of-f-when-existsp
         (packn-pos (list 'natp-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))
    (uboundp-of-f-when-existsp
         (packn-pos (list uboundp '-of- f '-when- 'existsp)
                    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))
    (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))
    (ubound-geq-member (packn-pos (list f '.ubound-geq-member)
                                  pkgwit))
    (ubound-nonmember-gt-member
         (packn-pos (list f '.ubound-nonmember-gt-member)
                    pkgwit))
    (find-max (packn-pos (list f '.find-max) pkgwit))
    (find-max-uboundp-preservation
         (packn-pos (list f '.find-max-uboundp-preservation)
                    pkgwit))
    (elementp-of-find-max (packn-pos (list f '.elementp-of-find-max)
                                     pkgwit))
    (uboundp-of-find-max (packn-pos (list f '.uboundp-of-find-max)
                                    pkgwit))
    (existsp-when-nonempty-and-bounded
         (packn-pos (list f '.existsp-when-nonempty-and-bounded)
                    pkgwit))
    (equal-when-member-and-ubound
         (packn-pos (list f '.equal-when-member-and-ubound)
                    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 'natp (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))))
    (uboundp-events
     (cons
      (cons
       'defun-sk
       (cons
        uboundp
        (cons
         x1...xn-y
         (cons
          (cons
           'declare
           (cons
            (cons
             'xargs
             (cons
              ':guard
              (cons
                (cons 'and
                      (cons guard
                            (cons (cons 'natp (cons y 'nil)) 'nil)))
                '(:verify-guards nil))))
            'nil))
          (cons
           (cons
            'forall
            (cons
             (cons y1 'nil)
             (cons
              (cons
               'impliez
               (cons
                (cons
                  'and
                  (cons (cons 'natp (cons y1 'nil))
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil)))
                (cons (cons '>=
                            (cons (cons 'nfix (cons y 'nil))
                                  (cons y1 'nil)))
                      'nil)))
              'nil)))
           (cons
            ':rewrite
            (cons
             (cons
              'implies
              (cons
               (cons
                'and
                (cons
                  (cons uboundp x1...xn-y)
                  (cons (cons 'natp (cons y1 'nil))
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil))))
               (cons (cons '>=
                           (cons (cons 'nfix (cons y 'nil))
                                 (cons y1 'nil)))
                     'nil)))
             'nil)))))))
      (append
       (and verify-guards
            (cons (cons 'verify-guards
                        (cons uboundp 'nil))
                  'nil))
       (cons
        (cons
             'defthm
             (cons booleanp-of-uboundp
                   (cons (cons 'booleanp
                               (cons (cons uboundp x1...xn-y) 'nil))
                         'nil)))
        (cons
          (cons 'in-theory
                (cons (cons 'disable
                            (cons uboundp (cons uboundp-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 'natp (cons y 'nil))
                       (cons (cons elementp x1...xn-y)
                             (cons (cons uboundp 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-natp-of-f
             (cons
              (cons 'maybe-natp
                    (cons (cons f x1...xn) 'nil))
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                       (cons 'enable
                             (cons 'maybe-natp (cons existsp 'nil)))
                       'nil)))
                 'nil)
                'nil)))))
           'nil))
         (cons
          (cons 'defthm
                (cons maybe-natp-of-f
                      (cons (cons 'maybe-natp
                                  (cons (cons f x1...xn) 'nil))
                            'nil)))
          (cons
           (cons
            'local
            (cons
             (cons
              'defthm
              (cons
               natp-of-f-equal-existsp
               (cons
                (cons 'equal
                      (cons (cons 'natp
                                  (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
              natp-of-f-equal-existsp
              (cons (cons 'equal
                          (cons (cons 'natp
                                      (cons (cons f x1...xn) 'nil))
                                (cons (cons existsp x1...xn) 'nil)))
                    'nil)))
            (cons
             (cons
              'defthm
              (cons
               natp-of-f-when-existsp
               (cons
                (cons
                     'implies
                     (cons (cons existsp x1...xn)
                           (cons (cons 'natp
                                       (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
                       uboundp-of-f-when-existsp
                       (cons
                        (cons
                         'implies
                         (cons
                          (cons existsp x1...xn)
                          (cons
                           (cons
                            uboundp
                            (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
                      uboundp-of-f-when-existsp
                      (cons
                       (cons
                        'implies
                        (cons
                         (cons existsp x1...xn)
                         (cons
                          (cons
                           uboundp
                           (append
                              x1...xn (cons (cons f x1...xn) '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
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                               (cons (cons 'natp (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
                                 ':use
                                 (cons
                                  (cons
                                   uboundp-of-f-when-existsp
                                   (cons
                                    (cons
                                     ':instance
                                     (cons
                                      uboundp-necc
                                      (cons
                                        (cons y
                                              (cons (cons f x1...xn)
                                                    'nil))
                                        '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 elementp
                                    (append x1...xn (cons y1 'nil)))
                              (cons (cons 'natp (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
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                                 (cons (cons 'natp (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
                                    elementp
                                    (append x1...xn (cons y1 'nil)))
                                (cons (cons 'natp (cons y1 'nil))
                                      'nil))))
                             (cons (cons '>=
                                         (cons (cons f x1...xn)
                                               (cons y1 '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
                                    uboundp
                                    (append x1...xn (cons y1 'nil)))
                                   (cons (cons 'natp (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
                                          uboundp-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-leq-when-existsp-linear
                            (cons
                             (cons
                              'implies
                              (cons
                               (cons
                                'and
                                (cons
                                 (cons existsp x1...xn)
                                 (cons
                                  (cons
                                    uboundp
                                    (append x1...xn (cons y1 'nil)))
                                  (cons (cons 'natp (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
                                       uboundp
                                       (append
                                            x1...xn (cons y1 'nil)))
                                     (cons
                                         (cons 'natp (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
                                       uboundp
                                       (append
                                            x1...xn (cons y1 'nil)))
                                    (cons
                                         (cons 'natp (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
          ubound-geq-member
          (cons
           (cons
            'implies
            (cons
             (cons
              'and
              (cons
               (cons 'natp (cons y0 'nil))
               (cons
                (cons elementp
                      (append x1...xn (cons y0 'nil)))
                (cons
                 (cons 'natp (cons y1 'nil))
                 (cons
                      (cons uboundp (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
                       uboundp-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
           ubound-nonmember-gt-member
           (cons
            (cons
             'implies
             (cons
              (cons
               'and
               (cons
                (cons 'natp (cons y0 'nil))
                (cons
                 (cons elementp
                       (append x1...xn (cons y0 'nil)))
                 (cons
                  (cons 'natp (cons y1 'nil))
                  (cons
                   (cons uboundp (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 ubound-geq-member 'nil)))
                         'nil)
                   'nil)))))))
         'nil))
       (cons
        (cons
         'local
         (cons
          (cons
           'defun
           (cons
            find-max
            (cons
             (append x1...xn (cons y1 (cons y0 'nil)))
             (cons
              (cons
               'declare
               (cons
                (cons
                 'xargs
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                      '"Goal"
                      (cons ':use
                            (cons ubound-nonmember-gt-member 'nil)))
                    'nil)
                   'nil)))
                'nil))
              (cons
               (cons
                'if
                (cons
                 (cons
                  'and
                  (cons
                   (cons 'natp (cons y0 'nil))
                   (cons
                    (cons elementp
                          (append x1...xn (cons y0 'nil)))
                    (cons
                     (cons 'natp (cons y1 'nil))
                     (cons
                      (cons uboundp (append x1...xn (cons y1 'nil)))
                      'nil)))))
                 (cons
                  (cons
                   'if
                   (cons
                    (cons elementp
                          (append x1...xn (cons y1 'nil)))
                    (cons
                     y1
                     (cons
                       (cons find-max
                             (append x1...xn
                                     (cons (cons '1- (cons y1 'nil))
                                           (cons y0 'nil))))
                       'nil))))
                  '(0))))
               'nil)))))
          'nil))
        (cons
         (cons
          'local
          (cons
           (cons
            'defthm
            (cons
             find-max-uboundp-preservation
             (cons
              (cons
               'implies
               (cons
                (cons
                 'and
                 (cons
                  (cons 'natp (cons y0 'nil))
                  (cons
                   (cons elementp
                         (append x1...xn (cons y0 'nil)))
                   (cons
                    (cons 'natp (cons y1 'nil))
                    (cons
                     (cons uboundp (append x1...xn (cons y1 'nil)))
                     (cons
                      (cons
                        'not
                        (cons (cons elementp
                                    (append x1...xn (cons y1 'nil)))
                              'nil))
                      'nil))))))
                (cons
                 (cons
                     uboundp
                     (append x1...xn
                             (cons (cons '1- (cons y1 'nil)) 'nil)))
                 'nil)))
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':expand
                   (cons
                    (cons
                     (cons
                        uboundp
                        (append
                             x1...xn
                             (cons (cons '1- (cons y1 'nil)) 'nil)))
                     'nil)
                    (cons
                     ':use
                     (cons
                      (cons
                       ':instance
                       (cons
                        uboundp-necc
                        (cons
                         (cons y (cons y1 'nil))
                         (cons
                          (cons
                           y1
                           (cons
                            (cons
                             uboundp-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-max
              (cons
               (cons
                'implies
                (cons
                 (cons
                  'and
                  (cons
                   (cons 'natp (cons y0 'nil))
                   (cons
                    (cons elementp
                          (append x1...xn (cons y0 'nil)))
                    (cons
                     (cons 'natp (cons y1 'nil))
                     (cons
                      (cons uboundp (append x1...xn (cons y1 'nil)))
                      'nil)))))
                 (cons
                  (cons
                   elementp
                   (append
                    x1...xn
                    (cons
                     (cons
                          find-max
                          (append x1...xn (cons y1 (cons y0 'nil))))
                     'nil)))
                  'nil)))
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                   'quote
                   (cons
                    (cons
                     ':use
                     (cons
                      (cons
                           ':instance
                           (cons uboundp-necc
                                 (cons (cons y (cons y1 'nil))
                                       (cons (cons y1 '(0)) 'nil))))
                      'nil))
                    'nil))
                  (cons
                   (cons
                    'quote
                    (cons
                     (cons
                      ':use
                      (cons
                       (cons
                        ':instance
                        (cons
                         uboundp-necc
                         (cons
                             (cons y '(0))
                             (cons (cons y1 (cons y0 'nil)) 'nil))))
                       'nil))
                     'nil))
                   'nil))
                 'nil)))))
            'nil))
          (cons
           (cons
            'local
            (cons
             (cons
              'defthm
              (cons
               uboundp-of-find-max
               (cons
                (cons
                 'implies
                 (cons
                  (cons
                   'and
                   (cons
                    (cons 'natp (cons y0 'nil))
                    (cons
                     (cons elementp
                           (append x1...xn (cons y0 'nil)))
                     (cons
                      (cons 'natp (cons y1 'nil))
                      (cons
                       (cons
                            uboundp (append x1...xn (cons y1 'nil)))
                       'nil)))))
                  (cons
                   (cons
                    uboundp
                    (append
                     x1...xn
                     (cons
                      (cons
                          find-max
                          (append x1...xn (cons y1 (cons y0 'nil))))
                      'nil)))
                   'nil)))
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    'quote
                    (cons
                     (cons
                      ':use
                      (cons
                       (cons
                           ':instance
                           (cons uboundp-necc
                                 (cons (cons y (cons y1 'nil))
                                       (cons (cons y1 '(0)) 'nil))))
                       'nil))
                     'nil))
                   (cons
                    (cons
                     'quote
                     (cons
                      (cons
                       ':use
                       (cons
                        (cons
                         ':instance
                         (cons
                          uboundp-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 'natp (cons y0 'nil))
                     (cons
                      (cons elementp
                            (append x1...xn (cons y0 'nil)))
                      (cons
                       (cons 'natp (cons y1 'nil))
                       (cons
                        (cons
                            uboundp (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-max
                               (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 'natp (cons y0 'nil))
                    (cons
                     (cons elementp
                           (append x1...xn (cons y0 'nil)))
                     (cons
                      (cons 'natp (cons y1 'nil))
                      (cons
                       (cons
                            uboundp (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-ubound
          (cons
           (cons
            'implies
            (cons
             (cons
              'and
              (cons
               (cons 'natp (cons y 'nil))
               (cons
                 (cons elementp (append x1...xn (cons y 'nil)))
                 (cons (cons uboundp (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-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-geq-when-existsp-rewrite
                               (cons (cons y1 (cons y 'nil)) 'nil)))
                       (cons
                        (cons
                         ':instance
                         (cons
                          uboundp-necc
                          (cons
                              (cons y1 (cons (cons f x1...xn) 'nil))
                              'nil)))
                        'nil)))
                     'nil)))))
                'nil)
               'nil)))))))
        'nil))
      (cons
       (cons
        'defthm
        (cons
         equal-when-member-and-ubound
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons 'natp (cons y 'nil))
              (cons
                 (cons elementp (append x1...xn (cons y 'nil)))
                 (cons (cons uboundp (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
        uboundp-events
        (append
           existsp-events
           (append f-events
                   (append existsp-when-non-empty-and-bounded-events
                           equal-when-member-and-bound)))))))))))