		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Def-integer-operations-2

Event to generate the ACL2 models of the C integer operations that involve two integer types.

Signature
(def-integer-operations-2 type1 type2) → event
Arguments: type1 — Guard (typep type1).; type2 — Guard (typep type2).
Returns: event — Type (pseudo-event-formp event).

These include all the strict pure binary operators.

For all the operations except shifts, we treat two cases differently: when the two usual arithmetic conversions applied to the operand types yields the same as the two operand types (which must therefore be equal), we generate a definition that performs a direct computation; otherwise, we generate a definition that converts the operands to the common type and then calls the function for that type as operand types. For shift operations, we turn the second operand into an ACL2 integer and then we call the shift function generated by def-integer-operations-1; the result has the promoted type of the first operand.

Definitions and Theorems

Function: def-integer-operations-2

(defun def-integer-operations-2 (type1 type2)
 (declare (xargs :guard (and (typep type1) (typep type2))))
 (declare (xargs :guard (and (type-nonchar-integerp type1)
                             (type-nonchar-integerp type2))))
 (let ((__function__ 'def-integer-operations-2))
  (declare (ignorable __function__))
  (b* ((type1-string (integer-type-xdoc-string type1))
       (type2-string (integer-type-xdoc-string type2))
       (type (uaconvert-types type1 type2))
       (samep (and (equal type type1)
                   (equal type type2)))
       (signedp (type-signed-integerp type))
       (ptype1 (promote-type type1))
       (<type1> (integer-type-to-fixtype type1))
       (<type2> (integer-type-to-fixtype type2))
       (<type> (integer-type-to-fixtype type))
       (<ptype1> (integer-type-to-fixtype ptype1))
       (<type1>p (pack <type1> 'p))
       (<type2>p (pack <type2> 'p))
       (<type>p (pack <type> 'p))
       (<ptype1>p (pack <ptype1> 'p))
       (integer-from-<type1> (pack 'integer-from- <type1>))
       (integer-from-<type2> (pack 'integer-from- <type2>))
       (<type>-from-integer (pack <type> '-from-integer))
       (<type>-from-integer-mod (pack <type>-from-integer '-mod))
       (<type>-integerp (pack <type> '-integerp))
       (<type>-from-<type1> (pack <type> '-from- <type1>))
       (<type>-from-<type2> (pack <type> '-from- <type2>))
       (add-<type1>-<type2> (pack 'add- <type1> '- <type2>))
       (add-<type1>-<type2>-okp (pack add-<type1>-<type2> '-okp))
       (add-<type>-<type> (pack 'add- <type> '- <type>))
       (add-<type>-<type>-okp (pack add-<type>-<type> '-okp))
       (sub-<type1>-<type2> (pack 'sub- <type1> '- <type2>))
       (sub-<type1>-<type2>-okp (pack sub-<type1>-<type2> '-okp))
       (sub-<type>-<type> (pack 'sub- <type> '- <type>))
       (sub-<type>-<type>-okp (pack sub-<type>-<type> '-okp))
       (mul-<type1>-<type2> (pack 'mul- <type1> '- <type2>))
       (mul-<type1>-<type2>-okp (pack mul-<type1>-<type2> '-okp))
       (mul-<type>-<type> (pack 'mul- <type> '- <type>))
       (mul-<type>-<type>-okp (pack mul-<type>-<type> '-okp))
       (div-<type1>-<type2> (pack 'div- <type1> '- <type2>))
       (div-<type1>-<type2>-okp (pack div-<type1>-<type2> '-okp))
       (div-<type>-<type> (pack 'div- <type> '- <type>))
       (div-<type>-<type>-okp (pack div-<type>-<type> '-okp))
       (rem-<type1>-<type2> (pack 'rem- <type1> '- <type2>))
       (rem-<type1>-<type2>-okp (pack rem-<type1>-<type2> '-okp))
       (rem-<type>-<type> (pack 'rem- <type> '- <type>))
       (rem-<type>-<type>-okp (pack rem-<type>-<type> '-okp))
       (shl-<type1>-<type2> (pack 'shl- <type1> '- <type2>))
       (shl-<type1>-<type2>-okp (pack shl-<type1>-<type2> '-okp))
       (shl-<type1> (pack 'shl- <type1>))
       (shl-<type1>-okp (pack shl-<type1> '-okp))
       (shr-<type1>-<type2> (pack 'shr- <type1> '- <type2>))
       (shr-<type1>-<type2>-okp (pack shr-<type1>-<type2> '-okp))
       (shr-<type1> (pack 'shr- <type1>))
       (shr-<type1>-okp (pack shr-<type1> '-okp))
       (lt-<type1>-<type2> (pack 'lt- <type1> '- <type2>))
       (lt-<type>-<type> (pack 'lt- <type> '- <type>))
       (gt-<type1>-<type2> (pack 'gt- <type1> '- <type2>))
       (gt-<type>-<type> (pack 'gt- <type> '- <type>))
       (le-<type1>-<type2> (pack 'le- <type1> '- <type2>))
       (le-<type>-<type> (pack 'le- <type> '- <type>))
       (ge-<type1>-<type2> (pack 'ge- <type1> '- <type2>))
       (ge-<type>-<type> (pack 'ge- <type> '- <type>))
       (eq-<type1>-<type2> (pack 'eq- <type1> '- <type2>))
       (eq-<type>-<type> (pack 'eq- <type> '- <type>))
       (ne-<type1>-<type2> (pack 'ne- <type1> '- <type2>))
       (ne-<type>-<type> (pack 'ne- <type> '- <type>))
       (bitand-<type1>-<type2> (pack 'bitand- <type1> '- <type2>))
       (bitand-<type>-<type> (pack 'bitand- <type> '- <type>))
       (bitxor-<type1>-<type2> (pack 'bitxor- <type1> '- <type2>))
       (bitxor-<type>-<type> (pack 'bitxor- <type> '- <type>))
       (bitior-<type1>-<type2> (pack 'bitior- <type1> '- <type2>))
       (bitior-<type>-<type> (pack 'bitior- <type> '- <type>)))
   (cons
    'progn
    (cons
     '(set-ignore-ok t)
     (cons
      '(set-irrelevant-formals-ok t)
      (append
       (and
        signedp
        (cons
         (cons
          'defun-integer
          (cons
           add-<type1>-<type2>-okp
           (cons
            ':arg1-type
            (cons
             <type1>p
             (cons
              ':arg2-type
              (cons
               <type2>p
               (cons
                ':res-type
                (cons
                 'booleanp
                 (cons
                  ':short
                  (cons
                   (str::cat "Check if the addition of a value of "
                             type1-string " and a value of "
                             type2-string " is well-defined.")
                   (cons
                    ':body
                    (cons
                     (if samep
                      (cons
                       <type>-integerp
                       (cons
                        (cons
                         '+
                         (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                        'nil))
                      (cons
                       add-<type>-<type>-okp
                       (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                     'nil))))))))))))
         'nil))
       (cons
        (cons
         'defun-integer
         (cons
          add-<type1>-<type2>
          (cons
           ':arg1-type
           (cons
            <type1>p
            (cons
             ':arg2-type
             (cons
              <type2>p
              (append
               (and
                   signedp
                   (cons ':guard
                         (cons (cons add-<type1>-<type2>-okp '(x y))
                               'nil)))
               (cons
                ':res-type
                (cons
                 <type>p
                 (cons
                  ':short
                  (cons
                   (str::cat "Addition of a value of "
                             type1-string " and a value of "
                             type2-string " [C17:6.5.6].")
                   (cons
                    ':body
                    (cons
                     (if samep
                      (cons
                       (if signedp <type>-from-integer
                         <type>-from-integer-mod)
                       (cons
                        (cons
                         '+
                         (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                        'nil))
                      (cons
                       add-<type>-<type>
                       (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                     (and
                      signedp
                      (cons
                       ':guard-hints
                       (cons
                        (cons
                         (cons
                          '"Goal"
                          (cons
                           ':in-theory
                           (cons
                            (cons
                                'enable
                                (cons add-<type1>-<type2>-okp 'nil))
                            'nil)))
                         'nil)
                        'nil))))))))))))))))
        (append
         (and
          signedp
          (cons
           (cons
            'defun-integer
            (cons
             sub-<type1>-<type2>-okp
             (cons
              ':arg1-type
              (cons
               <type1>p
               (cons
                ':arg2-type
                (cons
                 <type2>p
                 (cons
                  ':res-type
                  (cons
                   'booleanp
                   (cons
                    ':short
                    (cons
                     (str::cat
                          "Check if the subtraction of a value of "
                          type1-string " and a value of "
                          type2-string " is well-defined.")
                     (cons
                      ':body
                      (cons
                       (if samep
                        (cons
                         <type>-integerp
                         (cons
                          (cons
                           '-
                           (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                          'nil))
                        (cons
                         sub-<type>-<type>-okp
                         (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                       'nil))))))))))))
           'nil))
         (cons
          (cons
           'defun-integer
           (cons
            sub-<type1>-<type2>
            (cons
             ':arg1-type
             (cons
              <type1>p
              (cons
               ':arg2-type
               (cons
                <type2>p
                (append
                 (and
                   signedp
                   (cons ':guard
                         (cons (cons sub-<type1>-<type2>-okp '(x y))
                               'nil)))
                 (cons
                  ':res-type
                  (cons
                   <type>p
                   (cons
                    ':short
                    (cons
                     (str::cat "Subtraction of a value of "
                               type1-string " and a value of "
                               type2-string " [C17:6.5.6].")
                     (cons
                      ':body
                      (cons
                       (if samep
                        (cons
                         (if signedp <type>-from-integer
                           <type>-from-integer-mod)
                         (cons
                          (cons
                           '-
                           (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                          'nil))
                        (cons
                         sub-<type>-<type>
                         (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                       (and
                        signedp
                        (cons
                         ':guard-hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                                'enable
                                (cons sub-<type1>-<type2>-okp 'nil))
                              'nil)))
                           'nil)
                          'nil))))))))))))))))
          (append
           (and
            signedp
            (cons
             (cons
              'defun-integer
              (cons
               mul-<type1>-<type2>-okp
               (cons
                ':arg1-type
                (cons
                 <type1>p
                 (cons
                  ':arg2-type
                  (cons
                   <type2>p
                   (cons
                    ':res-type
                    (cons
                     'booleanp
                     (cons
                      ':short
                      (cons
                       (str::cat
                        "Check if the multiplication of a value of "
                        type1-string " and a value of "
                        type2-string " is well-defined.")
                       (cons
                        ':body
                        (cons
                         (if samep
                          (cons
                           <type>-integerp
                           (cons
                            (cons
                             '*
                             (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                            'nil))
                          (cons
                           mul-<type>-<type>-okp
                           (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                         'nil))))))))))))
             'nil))
           (cons
            (cons
             'defun-integer
             (cons
              mul-<type1>-<type2>
              (cons
               ':arg1-type
               (cons
                <type1>p
                (cons
                 ':arg2-type
                 (cons
                  <type2>p
                  (append
                   (and
                    signedp
                    (cons
                         ':guard
                         (cons (cons mul-<type1>-<type2>-okp '(x y))
                               'nil)))
                   (cons
                    ':res-type
                    (cons
                     <type>p
                     (cons
                      ':short
                      (cons
                       (str::cat "Multiplication of a value of "
                                 type1-string " and a value of "
                                 type2-string " [C17:6.5.5].")
                       (cons
                        ':body
                        (cons
                         (if samep
                          (cons
                           (if signedp <type>-from-integer
                             <type>-from-integer-mod)
                           (cons
                            (cons
                             '*
                             (cons
                              (cons integer-from-<type1> '(x))
                              (cons (cons integer-from-<type2> '(y))
                                    'nil)))
                            'nil))
                          (cons
                           mul-<type>-<type>
                           (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                         (and
                          signedp
                          (cons
                           ':guard-hints
                           (cons
                            (cons
                             (cons
                              '"Goal"
                              (cons
                               ':in-theory
                               (cons
                                (cons
                                 'enable
                                 (cons
                                      mul-<type1>-<type2>-okp 'nil))
                                'nil)))
                             'nil)
                            'nil))))))))))))))))
            (cons
             (cons
              'defun-integer
              (cons
               div-<type1>-<type2>-okp
               (cons
                ':arg1-type
                (cons
                 <type1>p
                 (cons
                  ':arg2-type
                  (cons
                   <type2>p
                   (cons
                    ':res-type
                    (cons
                     'booleanp
                     (cons
                      ':short
                      (cons
                       (str::cat
                            "Check if the division of a value of "
                            type1-string " and a value of "
                            type2-string " is well-defined.")
                       (cons
                        ':body
                        (cons
                         (if samep
                          (if signedp
                           (cons
                            'and
                            (cons
                             (cons
                              'not
                              (cons
                               (cons
                                'equal
                                (cons
                                    (cons integer-from-<type2> '(y))
                                    '(0)))
                               'nil))
                             (cons
                              (cons
                               <type>-integerp
                               (cons
                                (cons
                                 'truncate
                                 (cons
                                  (cons integer-from-<type1> '(x))
                                  (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                                'nil))
                              'nil)))
                           (cons
                            'not
                            (cons
                             (cons
                              'equal
                              (cons (cons integer-from-<type2> '(y))
                                    '(0)))
                             'nil)))
                          (cons
                           div-<type>-<type>-okp
                           (cons
                            (if (eq <type> <type1>)
                                'x
                              (cons <type>-from-<type1> '(x)))
                            (cons (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                         'nil))))))))))))
             (cons
              (cons
               'defun-integer
               (cons
                div-<type1>-<type2>
                (cons
                 ':arg1-type
                 (cons
                  <type1>p
                  (cons
                   ':arg2-type
                   (cons
                    <type2>p
                    (cons
                     ':guard
                     (cons
                      (cons div-<type1>-<type2>-okp '(x y))
                      (cons
                       ':res-type
                       (cons
                        <type>p
                        (cons
                         ':short
                         (cons
                          (str::cat "Division of a value of "
                                    type1-string " and a value of "
                                    type2-string " [C17:6.5.5].")
                          (cons
                           ':body
                           (cons
                            (if samep
                             (cons
                              (if signedp <type>-from-integer
                                <type>-from-integer-mod)
                              (cons
                               (cons
                                'truncate
                                (cons
                                 (cons integer-from-<type1> '(x))
                                 (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                               'nil))
                             (cons
                              div-<type>-<type>
                              (cons
                               (if (eq <type> <type1>)
                                   'x
                                 (cons <type>-from-<type1> '(x)))
                               (cons
                                  (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                            (cons
                             ':guard-hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':in-theory
                                 (cons
                                  (cons
                                   'enable
                                   (cons
                                      div-<type1>-<type2>-okp 'nil))
                                  'nil)))
                               'nil)
                              'nil))))))))))))))))
              (cons
               (cons
                'defun-integer
                (cons
                 rem-<type1>-<type2>-okp
                 (cons
                  ':arg1-type
                  (cons
                   <type1>p
                   (cons
                    ':arg2-type
                    (cons
                     <type2>p
                     (cons
                      ':res-type
                      (cons
                       'booleanp
                       (cons
                        ':short
                        (cons
                         (str::cat
                             "Check if the remainder of a value of "
                             type1-string " and a value of "
                             type2-string " is well-defined.")
                         (cons
                          ':body
                          (cons
                           (if samep
                            (if signedp
                             (cons
                              'and
                              (cons
                               (cons
                                'not
                                (cons
                                 (cons
                                  'equal
                                  (cons
                                    (cons integer-from-<type2> '(y))
                                    '(0)))
                                 'nil))
                               (cons
                                (cons
                                 <type>-integerp
                                 (cons
                                  (cons
                                   'rem
                                   (cons
                                    (cons integer-from-<type1> '(x))
                                    (cons
                                     (cons
                                          integer-from-<type2> '(y))
                                     'nil)))
                                  'nil))
                                'nil)))
                             (cons
                              'not
                              (cons
                               (cons
                                'equal
                                (cons
                                    (cons integer-from-<type2> '(y))
                                    '(0)))
                               'nil)))
                            (cons
                             rem-<type>-<type>-okp
                             (cons
                              (if (eq <type> <type1>)
                                  'x
                                (cons <type>-from-<type1> '(x)))
                              (cons
                                  (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                           'nil))))))))))))
               (cons
                (cons
                 'defun-integer
                 (cons
                  rem-<type1>-<type2>
                  (cons
                   ':arg1-type
                   (cons
                    <type1>p
                    (cons
                     ':arg2-type
                     (cons
                      <type2>p
                      (cons
                       ':guard
                       (cons
                        (cons rem-<type1>-<type2>-okp '(x y))
                        (cons
                         ':res-type
                         (cons
                          <type>p
                          (cons
                           ':short
                           (cons
                            (str::cat
                                 "Remainder of a value of "
                                 type1-string " and a value of "
                                 type2-string " [C17:6.5.5].")
                            (cons
                             ':body
                             (cons
                              (if samep
                               (cons
                                (if signedp <type>-from-integer
                                  <type>-from-integer-mod)
                                (cons
                                 (cons
                                  'rem
                                  (cons
                                   (cons integer-from-<type1> '(x))
                                   (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                                 'nil))
                               (cons
                                rem-<type>-<type>
                                (cons
                                 (if (eq <type> <type1>)
                                     'x
                                   (cons <type>-from-<type1> '(x)))
                                 (cons
                                  (if (eq <type> <type2>)
                                      'y
                                    (cons <type>-from-<type2> '(y)))
                                  'nil))))
                              (cons
                               ':guard-hints
                               (cons
                                (cons
                                 (cons
                                  '"Goal"
                                  (cons
                                   ':in-theory
                                   (cons
                                    (cons
                                       'enable
                                       (cons rem-<type1>-<type2>-okp
                                             (and (not signedp)
                                                  (list 'rem))))
                                    'nil)))
                                 'nil)
                                'nil))))))))))))))))
                (cons
                 (cons
                  'defun-integer
                  (cons
                   shl-<type1>-<type2>-okp
                   (cons
                    ':arg1-type
                    (cons
                     <type1>p
                     (cons
                      ':arg2-type
                      (cons
                       <type2>p
                       (cons
                        ':res-type
                        (cons
                         'booleanp
                         (cons
                          ':short
                          (cons
                           (str::cat
                            "Check if the left shift of a value of "
                            type1-string " by a value of "
                            type2-string " is well-defined.")
                           (cons
                            ':body
                            (cons
                             (cons
                              shl-<type1>-okp
                              (cons
                               'x
                               (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                             'nil))))))))))))
                 (cons
                  (cons
                   'defun-integer
                   (cons
                    shl-<type1>-<type2>
                    (cons
                     ':arg1-type
                     (cons
                      <type1>p
                      (cons
                       ':arg2-type
                       (cons
                        <type2>p
                        (cons
                         ':guard
                         (cons
                          (cons shl-<type1>-<type2>-okp '(x y))
                          (cons
                           ':res-type
                           (cons
                            <ptype1>p
                            (cons
                             ':short
                             (cons
                              (str::cat
                                   "Left shift of a value of "
                                   type1-string " and a value of "
                                   type2-string " [C17:6.5.7].")
                              (cons
                               ':body
                               (cons
                                (cons
                                 shl-<type1>
                                 (cons
                                  'x
                                  (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                                (cons
                                 ':guard-hints
                                 (cons
                                  (cons
                                   (cons
                                    '"Goal"
                                    (cons
                                     ':in-theory
                                     (cons
                                      (cons
                                       'enable
                                       (cons shl-<type1>-<type2>-okp
                                             'nil))
                                      'nil)))
                                   'nil)
                                  'nil))))))))))))))))
                  (cons
                   (cons
                    'defun-integer
                    (cons
                     shr-<type1>-<type2>-okp
                     (cons
                      ':arg1-type
                      (cons
                       <type1>p
                       (cons
                        ':arg2-type
                        (cons
                         <type2>p
                         (cons
                          ':res-type
                          (cons
                           'booleanp
                           (cons
                            ':short
                            (cons
                             (str::cat
                              "Check if the right shift of a value of "
                              type1-string " by a value of "
                              type2-string " is well-defined.")
                             (cons
                              ':body
                              (cons
                               (cons
                                shr-<type1>-okp
                                (cons
                                 'x
                                 (cons
                                    (cons integer-from-<type2> '(y))
                                    'nil)))
                               'nil))))))))))))
                   (cons
                    (cons
                     'defun-integer
                     (cons
                      shr-<type1>-<type2>
                      (cons
                       ':arg1-type
                       (cons
                        <type1>p
                        (cons
                         ':arg2-type
                         (cons
                          <type2>p
                          (cons
                           ':guard
                           (cons
                            (cons shr-<type1>-<type2>-okp '(x y))
                            (cons
                             ':res-type
                             (cons
                              <ptype1>p
                              (cons
                               ':short
                               (cons
                                (str::cat
                                     "Right shift of a value of "
                                     type1-string " and a value of "
                                     type2-string " [C17:6.5.7].")
                                (cons
                                 ':body
                                 (cons
                                  (cons
                                   shr-<type1>
                                   (cons
                                    'x
                                    (cons
                                     (cons
                                          integer-from-<type2> '(y))
                                     'nil)))
                                  (cons
                                   ':guard-hints
                                   (cons
                                    (cons
                                     (cons
                                      '"Goal"
                                      (cons
                                       ':in-theory
                                       (cons
                                        (cons
                                         'enable
                                         (cons
                                             shr-<type1>-<type2>-okp
                                             'nil))
                                        'nil)))
                                     'nil)
                                    'nil))))))))))))))))
                    (cons
                     (cons
                      'defun-integer
                      (cons
                       lt-<type1>-<type2>
                       (cons
                        ':arg1-type
                        (cons
                         <type1>p
                         (cons
                          ':arg2-type
                          (cons
                           <type2>p
                           (cons
                            ':res-type
                            (cons
                             'sintp
                             (cons
                              ':short
                              (cons
                               (str::cat
                                 "Less-than relation of a value of "
                                 type1-string " and a value of "
                                 type2-string " [C17:6.5.8].")
                               (cons
                                ':body
                                (cons
                                 (if samep
                                  (cons
                                   'if
                                   (cons
                                    (cons
                                     '<
                                     (cons
                                      (cons
                                          integer-from-<type1> '(x))
                                      (cons
                                       (cons
                                          integer-from-<type2> '(y))
                                       'nil)))
                                    '((sint-from-integer 1)
                                      (sint-from-integer 0))))
                                  (cons
                                   lt-<type>-<type>
                                   (cons
                                    (if (eq <type> <type1>)
                                        'x
                                     (cons
                                          <type>-from-<type1> '(x)))
                                    (cons
                                     (if (eq <type> <type2>)
                                         'y
                                      (cons
                                          <type>-from-<type2> '(y)))
                                     'nil))))
                                 'nil))))))))))))
                     (cons
                      (cons
                       'defun-integer
                       (cons
                        gt-<type1>-<type2>
                        (cons
                         ':arg1-type
                         (cons
                          <type1>p
                          (cons
                           ':arg2-type
                           (cons
                            <type2>p
                            (cons
                             ':res-type
                             (cons
                              'sintp
                              (cons
                               ':short
                               (cons
                                (str::cat
                                 "Greater-than relation of a value of "
                                 type1-string " and a value of "
                                 type2-string " [C17:6.5.8].")
                                (cons
                                 ':body
                                 (cons
                                  (if samep
                                   (cons
                                    'if
                                    (cons
                                     (cons
                                      '>
                                      (cons
                                       (cons
                                          integer-from-<type1> '(x))
                                       (cons
                                        (cons
                                          integer-from-<type2> '(y))
                                        'nil)))
                                     '((sint-from-integer 1)
                                       (sint-from-integer 0))))
                                   (cons
                                    gt-<type>-<type>
                                    (cons
                                     (if (eq <type> <type1>)
                                         'x
                                      (cons
                                          <type>-from-<type1> '(x)))
                                     (cons
                                      (if (eq <type> <type2>)
                                          'y
                                       (cons
                                          <type>-from-<type2> '(y)))
                                      'nil))))
                                  'nil))))))))))))
                      (cons
                       (cons
                        'defun-integer
                        (cons
                         le-<type1>-<type2>
                         (cons
                          ':arg1-type
                          (cons
                           <type1>p
                           (cons
                            ':arg2-type
                            (cons
                             <type2>p
                             (cons
                              ':res-type
                              (cons
                               'sintp
                               (cons
                                ':short
                                (cons
                                 (str::cat
                                  "Less-than-or-equal-to relation of a value of "
                                  type1-string " and a value of "
                                  type2-string " [C17:6.5.8].")
                                 (cons
                                  ':body
                                  (cons
                                   (if samep
                                    (cons
                                     'if
                                     (cons
                                      (cons
                                       '<=
                                       (cons
                                        (cons
                                          integer-from-<type1> '(x))
                                        (cons
                                         (cons
                                          integer-from-<type2> '(y))
                                         'nil)))
                                      '((sint-from-integer 1)
                                        (sint-from-integer 0))))
                                    (cons
                                     le-<type>-<type>
                                     (cons
                                      (if (eq <type> <type1>)
                                          'x
                                       (cons
                                          <type>-from-<type1> '(x)))
                                      (cons
                                       (if (eq <type> <type2>)
                                           'y
                                        (cons
                                          <type>-from-<type2> '(y)))
                                       'nil))))
                                   'nil))))))))))))
                       (cons
                        (cons
                         'defun-integer
                         (cons
                          ge-<type1>-<type2>
                          (cons
                           ':arg1-type
                           (cons
                            <type1>p
                            (cons
                             ':arg2-type
                             (cons
                              <type2>p
                              (cons
                               ':res-type
                               (cons
                                'sintp
                                (cons
                                 ':short
                                 (cons
                                  (str::cat
                                   "Greater-than-or-equal-to relation of a value of "
                                   type1-string " and a value of "
                                   type2-string " [C17:6.5.8].")
                                  (cons
                                   ':body
                                   (cons
                                    (if samep
                                     (cons
                                      'if
                                      (cons
                                       (cons
                                        '>=
                                        (cons
                                         (cons
                                          integer-from-<type1> '(x))
                                         (cons
                                          (cons integer-from-<type2>
                                                '(y))
                                          'nil)))
                                       '((sint-from-integer 1)
                                         (sint-from-integer 0))))
                                     (cons
                                      ge-<type>-<type>
                                      (cons
                                       (if (eq <type> <type1>)
                                           'x
                                        (cons
                                          <type>-from-<type1> '(x)))
                                       (cons
                                        (if (eq <type> <type2>)
                                            'y
                                         (cons
                                          <type>-from-<type2> '(y)))
                                        'nil))))
                                    'nil))))))))))))
                        (cons
                         (cons
                          'defun-integer
                          (cons
                           eq-<type1>-<type2>
                           (cons
                            ':arg1-type
                            (cons
                             <type1>p
                             (cons
                              ':arg2-type
                              (cons
                               <type2>p
                               (cons
                                ':res-type
                                (cons
                                 'sintp
                                 (cons
                                  ':short
                                  (cons
                                   (str::cat
                                     "Equality of a value of "
                                     type1-string " and a value of "
                                     type2-string " [C17:6.5.9].")
                                   (cons
                                    ':body
                                    (cons
                                     (if samep
                                      (cons
                                       'if
                                       (cons
                                        (cons
                                         '=
                                         (cons
                                          (cons integer-from-<type1>
                                                '(x))
                                          (cons
                                           (cons
                                                integer-from-<type2>
                                                '(y))
                                           'nil)))
                                        '((sint-from-integer 1)
                                          (sint-from-integer 0))))
                                      (cons
                                       eq-<type>-<type>
                                       (cons
                                        (if (eq <type> <type1>)
                                            'x
                                         (cons
                                          <type>-from-<type1> '(x)))
                                        (cons
                                         (if (eq <type> <type2>)
                                             'y
                                           (cons <type>-from-<type2>
                                                 '(y)))
                                         'nil))))
                                     'nil))))))))))))
                         (cons
                          (cons
                           'defun-integer
                           (cons
                            ne-<type1>-<type2>
                            (cons
                             ':arg1-type
                             (cons
                              <type1>p
                              (cons
                               ':arg2-type
                               (cons
                                <type2>p
                                (cons
                                 ':res-type
                                 (cons
                                  'sintp
                                  (cons
                                   ':short
                                   (cons
                                    (str::cat
                                     "Non-equality of a value of "
                                     type1-string " and a value of "
                                     type2-string " [C17:6.5.9].")
                                    (cons
                                     ':body
                                     (cons
                                      (if samep
                                       (cons
                                        'if
                                        (cons
                                         (cons
                                          '/=
                                          (cons
                                           (cons
                                                integer-from-<type1>
                                                '(x))
                                           (cons
                                            (cons
                                                integer-from-<type2>
                                                '(y))
                                            'nil)))
                                         '((sint-from-integer 1)
                                           (sint-from-integer 0))))
                                       (cons
                                        ne-<type>-<type>
                                        (cons
                                         (if (eq <type> <type1>)
                                             'x
                                           (cons <type>-from-<type1>
                                                 '(x)))
                                         (cons
                                          (if (eq <type> <type2>)
                                              'y
                                           (cons <type>-from-<type2>
                                                 '(y)))
                                          'nil))))
                                      'nil))))))))))))
                          (cons
                           (cons
                            'defun-integer
                            (cons
                             bitand-<type1>-<type2>
                             (cons
                              ':arg1-type
                              (cons
                               <type1>p
                               (cons
                                ':arg2-type
                                (cons
                                 <type2>p
                                 (cons
                                  ':res-type
                                  (cons
                                   <type>p
                                   (cons
                                    ':short
                                    (cons
                                     (str::cat
                                      "Bitwise conjunction of a value of "
                                      type1-string
                                      " and a value of "
                                      type2-string " [C17:6.5.10].")
                                     (cons
                                      ':body
                                      (cons
                                       (if samep
                                        (cons
                                         <type>-from-integer
                                         (cons
                                          (cons
                                           'logand
                                           (cons
                                            (cons
                                                integer-from-<type1>
                                                '(x))
                                            (cons
                                             (cons
                                                integer-from-<type2>
                                                '(y))
                                             'nil)))
                                          'nil))
                                        (cons
                                         bitand-<type>-<type>
                                         (cons
                                          (if (eq <type> <type1>)
                                              'x
                                           (cons <type>-from-<type1>
                                                 '(x)))
                                          (cons
                                           (if (eq <type> <type2>)
                                               'y
                                            (cons
                                                 <type>-from-<type2>
                                                 '(y)))
                                           'nil))))
                                       (and
                                        samep
                                        (cons
                                         ':prepwork
                                         (cons
                                          '((local
                                             (include-book
                                                 "ihs/logops-lemmas"
                                                 :dir :system)))
                                          (cons
                                           ':guard-hints
                                           (cons
                                            (cons
                                             (cons
                                              '"Goal"
                                              (cons
                                               ':in-theory
                                               (cons
                                                (cons
                                                 'enable
                                                 (cons
                                                  <type>-integerp
                                                  (cons
                                                   <type>p
                                                   (cons
                                                    integer-from-<type1>
                                                    'nil))))
                                                'nil)))
                                             'nil)
                                            'nil)))))))))))))))))
                           (cons
                            (cons
                             'defun-integer
                             (cons
                              bitxor-<type1>-<type2>
                              (cons
                               ':arg1-type
                               (cons
                                <type1>p
                                (cons
                                 ':arg2-type
                                 (cons
                                  <type2>p
                                  (cons
                                   ':res-type
                                   (cons
                                    <type>p
                                    (cons
                                     ':short
                                     (cons
                                      (str::cat
                                       "Bitwise exclusive disjunction of a value of "
                                       type1-string
                                       " and a value of "
                                       type2-string
                                       " [C17:6.5.11].")
                                      (cons
                                       ':body
                                       (cons
                                        (if samep
                                         (cons
                                          <type>-from-integer
                                          (cons
                                           (cons
                                            'logxor
                                            (cons
                                             (cons
                                                integer-from-<type1>
                                                '(x))
                                             (cons
                                              (cons
                                                integer-from-<type2>
                                                '(y))
                                              'nil)))
                                           'nil))
                                         (cons
                                          bitxor-<type>-<type>
                                          (cons
                                           (if (eq <type> <type1>)
                                               'x
                                            (cons
                                                 <type>-from-<type1>
                                                 '(x)))
                                           (cons
                                            (if (eq <type> <type2>)
                                                'y
                                             (cons
                                                 <type>-from-<type2>
                                                 '(y)))
                                            'nil))))
                                        (and
                                         samep
                                         (cons
                                          ':prepwork
                                          (cons
                                           '((local
                                              (include-book
                                               "centaur/bitops/ihs-extensions"
                                               :dir :system)))
                                           (cons
                                            ':guard-hints
                                            (cons
                                             (cons
                                              (cons
                                               '"Goal"
                                               (cons
                                                ':in-theory
                                                (cons
                                                 (cons
                                                  'enable
                                                  (cons
                                                   <type>-integerp
                                                   (cons
                                                    <type>p
                                                    (cons
                                                     integer-from-<type1>
                                                     'nil))))
                                                 'nil)))
                                              'nil)
                                             'nil)))))))))))))))))
                            (cons
                             (cons
                              'defun-integer
                              (cons
                               bitior-<type1>-<type2>
                               (cons
                                ':arg1-type
                                (cons
                                 <type1>p
                                 (cons
                                  ':arg2-type
                                  (cons
                                   <type2>p
                                   (cons
                                    ':res-type
                                    (cons
                                     <type>p
                                     (cons
                                      ':short
                                      (cons
                                       (str::cat
                                        "Bitwise inclusive disjunction of a value of "
                                        type1-string
                                        " and a value of "
                                        type2-string
                                        " [C17:6.5.12].")
                                       (cons
                                        ':body
                                        (cons
                                         (if samep
                                          (cons
                                           <type>-from-integer
                                           (cons
                                            (cons
                                             'logior
                                             (cons
                                              (cons
                                                integer-from-<type1>
                                                '(x))
                                              (cons
                                               (cons
                                                integer-from-<type2>
                                                '(y))
                                               'nil)))
                                            'nil))
                                          (cons
                                           bitior-<type>-<type>
                                           (cons
                                            (if (eq <type> <type1>)
                                                'x
                                             (cons
                                                 <type>-from-<type1>
                                                 '(x)))
                                            (cons
                                             (if (eq <type> <type2>)
                                                 'y
                                              (cons
                                                 <type>-from-<type2>
                                                 '(y)))
                                             'nil))))
                                         (and
                                          samep
                                          (cons
                                           ':prepwork
                                           (cons
                                            '((local
                                               (include-book
                                                "centaur/bitops/ihs-extensions"
                                                :dir :system)))
                                            (cons
                                             ':guard-hints
                                             (cons
                                              (cons
                                               (cons
                                                '"Goal"
                                                (cons
                                                 ':in-theory
                                                 (cons
                                                  (cons
                                                   'enable
                                                   (cons
                                                    <type>-integerp
                                                    (cons
                                                     <type>p
                                                     (cons
                                                      integer-from-<type1>
                                                      'nil))))
                                                  'nil)))
                                               'nil)
                                              'nil)))))))))))))))))
                             'nil)))))))))))))))))))))))))))))

Theorem: pseudo-event-formp-of-def-integer-operations-2

(defthm pseudo-event-formp-of-def-integer-operations-2
  (b* ((event (def-integer-operations-2 type1 type2)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)