		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-array-member-ops

Generate the operations for an array member of the structures defined by defstruct.

Signature
(defstruct-gen-array-member-ops struct-tag struct-tag-p struct-tag-fix name type size?) → (mv event length checker reader reader-element writer writer-element reader-return-thm reader-element-return-thm writer-return-thm writer-element-return-thm)
Arguments: struct-tag — Guard (symbolp struct-tag).; struct-tag-p — Guard (symbolp struct-tag-p).; struct-tag-fix — Guard (symbolp struct-tag-fix).; name — Guard (identp name).; type — Guard (typep type).; size? — Guard (pos-optionp size?).
Returns: event — Type (pseudo-event-formp event).; length — Type (symbolp length).; checker — Type (symbolp checker).; reader — Type (symbolp reader).; reader-element — Type (symbolp reader-element).; writer — Type (symbolp writer).; writer-element — Type (symbolp writer-element).; reader-return-thm — Type (symbolp reader-return-thm).; reader-element-return-thm — Type (symbolp reader-element-return-thm).; writer-return-thm — Type (symbolp writer-return-thm).; writer-element-return-thm — Type (symbolp writer-element-return-thm).

This is only for integer arrays. The type parameter of this ACL2 function is the type of the elements of the array.

There are one reader and one writer for the whole array member, one reader and one writer for elements of the array member, and one reader and one writer for the list of elements of the array. We also generate a checker for the index. For a flexible array member, we also generate a length function.

Definitions and Theorems

Function: defstruct-gen-array-member-ops

(defun defstruct-gen-array-member-ops
       (struct-tag struct-tag-p
                   struct-tag-fix name type size?)
 (declare (xargs :guard (and (symbolp struct-tag)
                             (symbolp struct-tag-p)
                             (symbolp struct-tag-fix)
                             (identp name)
                             (typep type)
                             (pos-optionp size?))))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'defstruct-gen-array-member-ops))
  (declare (ignorable __function__))
  (b*
   ((fixtype (integer-type-to-fixtype type))
    (fixtype-arrayp (pack fixtype '-arrayp))
    (fixtype-array-fix (pack fixtype '-array-fix))
    (fixtype-array-fix-when-fixtype-arrayp
         (pack fixtype-array-fix '-when-
               fixtype-arrayp))
    (fixtype-arrayp-of-fixtype-array-fix (pack fixtype-arrayp '-of-
                                               fixtype-array-fix))
    (fixtype-arrayp-of-fixtype-array (pack fixtype '-arrayp-of-
                                           fixtype '-array))
    (fixtype-array-of (pack fixtype '-array-of))
    (fixtype-arrayp-of-fixtype-array-of (pack fixtype '-arrayp-of-
                                              fixtype-array-of))
    (fixtype-array-length (pack fixtype '-array-length))
    (fixtype-array-length-of-fixtype-array-fix-array
         (pack fixtype-array-length '-of-
               fixtype-array-fix '-array))
    (fixtype-array-write (pack fixtype '-array-write))
    (fixtype-array-length-of-fixtype-array-write
         (pack fixtype-array-length '-of-
               fixtype-array-write))
    (fixtype-array-index-okp (pack fixtype '-array-index-okp))
    (fixtype-array-read (pack fixtype '-array-read))
    (fixtype-array-read-of-cinteger-fix-index
         (pack fixtype-array-read
               '-of-cinteger-fix-index))
    (fixtype-array-write-of-cinteger-fix-index
         (pack fixtype-array-write
               '-of-cinteger-fix-index))
    (fixtype-array-write-of-fixtype-fix-element
         (pack fixtype-array-write '-of-
               fixtype '-fix-element))
    (fixtypep (pack fixtype 'p))
    (fixtype-listp (pack fixtype '-listp))
    (fixtype-list-fix (pack fixtype '-list-fix))
    (consp-of-fixtype-list-fix (pack 'consp-of- fixtype-list-fix))
    (len-of-fixtype-list-fix (pack 'len-of- fixtype-list-fix))
    (type-of-value-when-fixtype-arrayp (pack 'type-of-value-when-
                                             fixtype-arrayp))
    (fixtype-array->elements (pack fixtype '-array->elements))
    (fixtype-array->elements-of-fixtype-array
         (pack fixtype '-array->elements-of-
               fixtype '-array))
    (fixtype-listp-of-fixtype-array->elements
         (pack fixtype-listp '-of-
               fixtype-array->elements))
    (value-array->length-when-fixtype-arrayp
         (pack 'value-array->length-when-
               fixtype '-arrayp))
    (not-flexible-array-member-p-when-fixtype-arrayp
         (pack 'not-flexible-array-member-p-when-
               fixtype-arrayp))
    (valuep-when-fixtype-arrayp (pack 'valuep-when- fixtype-arrayp))
    (true-listp-when-fixtype-listp
         (pack 'true-listp-when-
               fixtype-listp '-compound-recognizer))
    (fixtype-array-of-of-fixtype-list-fix-elements
         (pack fixtype '-array-of-of-
               fixtype '-list-fix-elements))
    (posp-of-fixtype-array-length
         (pack 'posp-of- fixtype-array-length))
    (natp-of-fixtype-array-length
         (pack 'natp-of- fixtype-array-length))
    (fixtypep-of-fixtype-array-read (pack fixtypep '-of-
                                          fixtype-array-read))
    (fixtype-arrayp-of-fixtype-array-write
         (pack fixtype-arrayp '-of-
               fixtype-array-write))
    (member-length (packn-pos (list struct-tag '-
                                    (ident->name name)
                                    '-length)
                              struct-tag))
    (read-member (packn-pos (list struct-tag '-read-
                                  (ident->name name))
                            struct-tag))
    (write-member (packn-pos (list struct-tag '-write-
                                   (ident->name name))
                             struct-tag))
    (member-index-okp (packn-pos (list struct-tag '-
                                       (ident->name name)
                                       '-index-okp)
                                 struct-tag))
    (read-member-element (packn-pos (list struct-tag '-read-
                                          (ident->name name)
                                          '-element)
                                    struct-tag))
    (write-member-element (packn-pos (list struct-tag '-write-
                                           (ident->name name)
                                           '-element)
                                     struct-tag))
    (read-member-list (packn-pos (list struct-tag '-read-
                                       (ident->name name)
                                       '-list)
                                 struct-tag))
    (write-member-list (packn-pos (list struct-tag '-write-
                                        (ident->name name)
                                        '-list)
                                  struct-tag))
    (len-of-read-member-list
         (packn-pos (list 'len-of- read-member-list)
                    read-member-list))
    (consp-of-read-member-list
         (packn-pos (list 'consp-of- read-member-list)
                    read-member-list))
    (write-member-list-extra-guard
     (if size? (cons 'equal
                     (cons '(len values) (cons size? 'nil)))
      (cons
           'equal
           (cons '(len values)
                 (cons (cons 'len
                             (cons (cons read-member-list '(struct))
                                   'nil))
                       'nil)))))
    (struct-tag-equiv-implies-equal-struct-tag-fix-1
         (packn-pos (list struct-tag '-equiv-implies-equal-
                          struct-tag '-fix-1)
                    struct-tag))
    (struct-tag-fix-under-struct-tag-equiv
         (packn-pos (list struct-tag-fix '-under-
                          struct-tag '-equiv)
                    struct-tag))
    (struct-tag-fix-when-struct-tag-p
         (packn-pos (list struct-tag-fix '-when-
                          struct-tag-p)
                    struct-tag-p))
    (struct-tag-p-of-struct-tag-fix
         (packn-pos (list struct-tag-p '-of- struct-tag-fix)
                    struct-tag-p))
    (member-length-of-struct-tag-fix-struct
         (packn-pos (list member-length '-of-
                          struct-tag-fix '-struct)
                    struct-tag))
    (read-member-of-struct-tag-fix-struct
         (packn-pos (list read-member '-of-
                          struct-tag-fix '-struct)
                    struct-tag))
    (write-member-of-struct-tag-fix-struct
         (packn-pos (list write-member '-of-
                          struct-tag-fix '-struct)
                    struct-tag))
    (struct-tag-p-of-write-member
         (packn-pos (list struct-tag-p '-of- write-member)
                    struct-tag))
    (member-length-theory
     (cons
      'consp-when-ucharp
      (cons
       'consp-when-ushortp
       (cons
        'consp-when-uintp
        (cons
         'consp-when-ulongp
         (cons
          'consp-when-ullongp
          (cons
           'consp-when-scharp
           (cons
            'consp-when-sshortp
            (cons
             'consp-when-sintp
             (cons
              'consp-when-slongp
              (cons
               'consp-when-sllongp
               (cons
                'consp-when-valuep
                (cons
                 'consp-when-uchar-arrayp
                 (cons
                  'consp-when-ushort-arrayp
                  (cons
                   'consp-when-uint-arrayp
                   (cons
                    'consp-when-ulong-arrayp
                    (cons
                     'consp-when-ullong-arrayp
                     (cons
                      'consp-when-schar-arrayp
                      (cons
                       'consp-when-sshort-arrayp
                       (cons
                        'consp-when-sint-arrayp
                        (cons
                         'consp-when-slong-arrayp
                         (cons
                          'consp-when-sllong-arrayp
                          (cons
                           'consp-when-valuep
                           (cons
                            'value-struct-read
                            (cons
                             'value-optionp-when-valuep
                             (cons
                              'valuep-when-value-optionp
                              (cons
                               'eq
                               (cons
                                'not
                                (cons
                                 struct-tag-p
                                 (cons
                                  '(:e equal)
                                  (cons
                                   '(:e ident)
                                   (cons
                                    '(:e identp)
                                    (cons
                                     struct-tag-fix-when-struct-tag-p
                                     (cons
                                      (cons
                                       ':t
                                       (cons
                                        posp-of-fixtype-array-length
                                        'nil))
                                      '((:t
                                         value-struct->flexiblep))))))))))))))))))))))))))))))))))))
    (read-member-returns-theory
     (cons
      struct-tag-p
      (cons
           struct-tag-fix
           (cons read-member
                 '(value-struct-read (:e ident)
                                     (:e member-value)
                                     (:e repeat)
                                     (:e schar-from-integer)
                                     (:e uchar-from-integer)
                                     (:e sshort-from-integer)
                                     (:e ushort-from-integer)
                                     (:e sint-from-integer)
                                     (:e uint-from-integer)
                                     (:e slong-from-integer)
                                     (:e ulong-from-integer)
                                     (:e sllong-from-integer)
                                     (:e ullong-from-integer)
                                     (:e type-schar)
                                     (:e type-uchar)
                                     (:e type-sshort)
                                     (:e type-ushort)
                                     (:e type-sint)
                                     (:e type-uint)
                                     (:e type-slong)
                                     (:e type-ulong)
                                     (:e type-sllong)
                                     (:e type-ullong)
                                     (:e schar-arrayp)
                                     (:e uchar-arrayp)
                                     (:e sshort-arrayp)
                                     (:e ushort-arrayp)
                                     (:e sint-arrayp)
                                     (:e uint-arrayp)
                                     (:e slong-arrayp)
                                     (:e ulong-arrayp)
                                     (:e sllong-arrayp)
                                     (:e ullong-arrayp)
                                     (:e value-array)
                                     (:e value-struct)
                                     (:e value-struct->members)
                                     (:e value-struct-read-aux))))))
    (write-member-returns-theory
     (append
      (and (not size?)
           (list member-length 'value-struct-read))
      (cons
       struct-tag-p
       (cons
        struct-tag-fix
        (cons
         write-member
         (cons
          'value-array->length-when-schar-arrayp
          (cons
           'value-array->length-when-uchar-arrayp
           (cons
            'value-array->length-when-sshort-arrayp
            (cons
             'value-array->length-when-ushort-arrayp
             (cons
              'value-array->length-when-sint-arrayp
              (cons
               'value-array->length-when-uint-arrayp
               (cons
                'value-array->length-when-slong-arrayp
                (cons
                 'value-array->length-when-ulong-arrayp
                 (cons
                  'value-array->length-when-sllong-arrayp
                  (cons
                   'value-array->length-when-ullong-arrayp
                   (cons
                    'value-struct-write
                    (cons
                     '(:e acl2::bool-fix)
                     (cons
                      '(:e ident)
                      (cons
                       '(:e ident-equiv)
                       (cons
                        '(:e ident-fix)
                        (cons
                         (cons ':t (cons struct-tag-p 'nil))
                         '((:t value-struct)
                           (:t value-struct-write-aux)
                           member-value-list->name-list-of-struct-write-aux
                           member-value-list-fix-when-member-value-listp
                           member-value-listp-of-value-struct-write-aux
                           not-errorp-when-member-value-listp
                           remove-flexible-array-member-when-absent
                           return-type-of-value-struct
                           value-fix-when-valuep
                           value-optionp-when-valuep
                           valuep-when-value-optionp
                           value-struct->flexiblep-of-value-struct
                           value-struct->members-of-value-struct
                           value-struct->tag-of-value-struct
                           value-struct-read-aux-of-value-struct-write-aux
                           not-flexible-array-member-p-when-schar-arrayp
                           not-flexible-array-member-p-when-uchar-arrayp
                           not-flexible-array-member-p-when-sshort-arrayp
                           not-flexible-array-member-p-when-ushort-arrayp
                           not-flexible-array-member-p-when-sint-arrayp
                           not-flexible-array-member-p-when-uint-arrayp
                           not-flexible-array-member-p-when-slong-arrayp
                           not-flexible-array-member-p-when-ulong-arrayp
                           not-flexible-array-member-p-when-sllong-arrayp
                           not-flexible-array-member-p-when-ullong-arrayp
                           type-of-value-when-schar-arrayp
                           type-of-value-when-uchar-arrayp
                           type-of-value-when-sshort-arrayp
                           type-of-value-when-ushort-arrayp
                           type-of-value-when-sint-arrayp
                           type-of-value-when-uint-arrayp
                           type-of-value-when-slong-arrayp
                           type-of-value-when-ulong-arrayp
                           type-of-value-when-sllong-arrayp
                           type-of-value-when-ullong-arrayp
                           valuep-when-schar-arrayp
                           valuep-when-uchar-arrayp
                           valuep-when-sshort-arrayp
                           valuep-when-ushort-arrayp
                           valuep-when-sint-arrayp
                           valuep-when-uint-arrayp
                           valuep-when-slong-arrayp
                           valuep-when-ulong-arrayp
                           valuep-when-sllong-arrayp
                           valuep-when-ullong-arrayp
                           (:e member-value)
                           (:e member-value-list->name-list)
                           (:e repeat)
                           (:e schar-from-integer)
                           (:e uchar-from-integer)
                           (:e sshort-from-integer)
                           (:e ushort-from-integer)
                           (:e sint-from-integer)
                           (:e uint-from-integer)
                           (:e slong-from-integer)
                           (:e ulong-from-integer)
                           (:e sllong-from-integer)
                           (:e ullong-from-integer)
                           (:e scharp)
                           (:e ucharp)
                           (:e sshortp)
                           (:e ushortp)
                           (:e sintp)
                           (:e uintp)
                           (:e slongp)
                           (:e ulongp)
                           (:e sllongp)
                           (:e ullongp)
                           (:e type-schar)
                           (:e type-uchar)
                           (:e type-sshort)
                           (:e type-ushort)
                           (:e type-sint)
                           (:e type-uint)
                           (:e type-slong)
                           (:e type-ulong)
                           (:e type-sllong)
                           (:e type-ullong)
                           (:e type-array)
                           (:e schar-array-length)
                           (:e uchar-array-length)
                           (:e sshort-array-length)
                           (:e ushort-array-length)
                           (:e sint-array-length)
                           (:e uint-array-length)
                           (:e slong-array-length)
                           (:e ulong-array-length)
                           (:e sllong-array-length)
                           (:e ullong-array-length)
                           (:e schar-arrayp)
                           (:e uchar-arrayp)
                           (:e sshort-arrayp)
                           (:e ushort-arrayp)
                           (:e sint-arrayp)
                           (:e uint-arrayp)
                           (:e slong-arrayp)
                           (:e ulong-arrayp)
                           (:e sllong-arrayp)
                           (:e ullong-arrayp)
                           (:e value-array)
                           (:e value-struct)
                           (:e value-kind)
                           (:e value-struct->flexiblep)
                           (:e value-struct->members)
                           (:e value-struct->tag)
                           (:e value-struct-read-aux)
                           (:e valuep)
                           schar-array-length-of-schar-array-fix-array
                           uchar-array-length-of-uchar-array-fix-array
                           sshort-array-length-of-sshort-array-fix-array
                           ushort-array-length-of-ushort-array-fix-array
                           sint-array-length-of-sint-array-fix-array
                           uint-array-length-of-uint-array-fix-array
                           slong-array-length-of-slong-array-fix-array
                           ulong-array-length-of-ulong-array-fix-array
                           sllong-array-length-of-sllong-array-fix-array
                           ullong-array-length-of-ullong-array-fix-array
                           schar-arrayp-of-schar-array-fix
                           uchar-arrayp-of-uchar-array-fix
                           sshort-arrayp-of-sshort-array-fix
                           ushort-arrayp-of-ushort-array-fix
                           sint-arrayp-of-sint-array-fix
                           uint-arrayp-of-uint-array-fix
                           slong-arrayp-of-slong-array-fix
                           ulong-arrayp-of-ulong-array-fix
                           sllong-arrayp-of-sllong-array-fix
                           ullong-arrayp-of-ullong-array-fix))))))))))))))))))))))
    (len-of-read-member-list-theory
     (cons
      struct-tag-p
      (cons
       struct-tag-fix
       (cons
          read-member-list
          (cons fixtype-array-length
                '(value-struct-read value-struct-read-aux (:e cons)
                                    (:e ident)
                                    (:e len)
                                    (:e member-value)
                                    (:e repeat)
                                    (:e type-schar)
                                    (:e type-uchar)
                                    (:e type-sshort)
                                    (:e type-ushort)
                                    (:e type-sint)
                                    (:e type-uint)
                                    (:e type-slong)
                                    (:e type-ulong)
                                    (:e type-sllong)
                                    (:e type-ullong)
                                    (:e schar-from-integer)
                                    (:e uchar-from-integer)
                                    (:e sshort-from-integer)
                                    (:e ushort-from-integer)
                                    (:e sint-from-integer)
                                    (:e uint-from-integer)
                                    (:e slong-from-integer)
                                    (:e ulong-from-integer)
                                    (:e sllong-from-integer)
                                    (:e ullong-from-integer)
                                    (:e schar-array->elements)
                                    (:e uchar-array->elements)
                                    (:e sshort-array->elements)
                                    (:e ushort-array->elements)
                                    (:e sint-array->elements)
                                    (:e uint-array->elements)
                                    (:e slong-array->elements)
                                    (:e ulong-array->elements)
                                    (:e sllong-array->elements)
                                    (:e ullong-array->elements)
                                    (:e value-array)
                                    (:e value-struct)
                                    (:e value-struct->members)
                                    (:e value-struct-read-aux)))))))
    (write-member-list-theory
     (cons
      struct-tag-p
      (cons
       struct-tag-fix
       (cons
        write-member-list
        (cons
         'value-struct-write
         (cons
          fixtype-array-length
          (cons
           fixtype-array-of
           (cons
            value-array->length-when-fixtype-arrayp
            (cons
             consp-of-fixtype-list-fix
             (cons
              len-of-fixtype-list-fix
              (cons
               'member-value-list->name-list-of-struct-write-aux
               (cons
                'member-value-list-fix-when-member-value-listp
                (cons
                 'member-value-listp-of-value-struct-write-aux
                 (cons
                  'not-errorp-when-member-value-listp
                  (cons
                   not-flexible-array-member-p-when-fixtype-arrayp
                   (cons
                    'remove-flexible-array-member-when-absent
                    (cons
                     'return-type-of-value-struct
                     (cons
                      type-of-value-when-fixtype-arrayp
                      (cons
                       fixtype-array->elements-of-fixtype-array
                       (cons
                        fixtype-arrayp-of-fixtype-array
                        (cons
                         'value-fix-when-valuep
                         (cons
                          'value-struct->flexiblep-of-value-struct
                          (cons
                           'value-struct->members-of-value-struct
                           (cons
                            'value-struct->tag-of-value-struct
                            (cons
                             'value-struct-read-aux-of-value-struct-write-aux
                             (cons
                              valuep-when-fixtype-arrayp
                              (cons
                               (cons
                                ':e
                                (cons fixtype-array->elements 'nil))
                               (cons
                                '(:e acl2::bool-fix)
                                (cons
                                 '(:e ident)
                                 (cons
                                  '(:e ident-fix)
                                  (cons
                                   '(:e ident-equiv)
                                   (cons
                                    '(:e member-value)
                                    (cons
                                     '(:e
                                       member-value-list->name-list)
                                     (cons
                                      '(:e repeat)
                                      (cons
                                       '(:e len)
                                       (cons
                                        '(:e type-array)
                                        (cons
                                         '(:e value-struct)
                                         (cons
                                          '(:e value-struct->tag)
                                          (cons
                                           '(:e
                                              value-struct->members)
                                           (cons
                                            '(:e
                                              value-struct->flexiblep)
                                            (cons
                                             '(:e value-array)
                                             (cons
                                              '(:e
                                                value-struct-read-aux)
                                              (cons
                                               '(:e type-schar)
                                               (cons
                                                '(:e type-uchar)
                                                (cons
                                                 '(:e type-sshort)
                                                 (cons
                                                  '(:e type-ushort)
                                                  (cons
                                                   '(:e type-sint)
                                                   (cons
                                                    '(:e type-uint)
                                                    (cons
                                                     '(:e
                                                         type-slong)
                                                     (cons
                                                      '(:e
                                                         type-ulong)
                                                      (cons
                                                       '(:e
                                                         type-sllong)
                                                       (cons
                                                        '(:e
                                                          type-ullong)
                                                        (cons
                                                         '(:e
                                                           schar-from-integer)
                                                         (cons
                                                          '(:e
                                                            uchar-from-integer)
                                                          (cons
                                                           '(:e
                                                             sshort-from-integer)
                                                           (cons
                                                            '(:e
                                                              ushort-from-integer)
                                                            (cons
                                                             '(:e
                                                               sint-from-integer)
                                                             (cons
                                                              '(:e
                                                                uint-from-integer)
                                                              (cons
                                                               '(:e
                                                                 slong-from-integer)
                                                               (cons
                                                                '(:e
                                                                  ulong-from-integer)
                                                                (cons
                                                                 '(:e
                                                                   sllong-from-integer)
                                                                 (cons
                                                                  '(:e
                                                                    ullong-from-integer)
                                                                  (cons
                                                                   '(:e
                                                                     scharp)
                                                                   (cons
                                                                    '(:e
                                                                     
 ucharp)
                                                                    (cons
                                                                     '(:e
                                                                     
  sshortp)
                                                                     (cons
                                                                     
 '(:e
                                                                     
   ushortp)
                                                                     
 (cons
                                                                     
  '(:e
                                                                     
    sintp)
                                                                     
  (cons
                                                                     
   '(:e
                                                                     
     uintp)
                                                                     
   (cons
                                                                     
    '(:e
                                                                     
      slongp)
                                                                     
    (cons
                                                                     
     '(:e
                                                                     
       ulongp)
                                                                     
     (cons
                                                                     
      '(:e
                                                                     
        sllongp)
                                                                     
      (cons
                                                                     
       '(:e
                                                                     
         ullongp)
                                                                     
       (cons
                                                                     
        '(:e
                                                                     
          schar-arrayp)
                                                                     
        (cons
                                                                     
         '(:e
                                                                     
           uchar-arrayp)
                                                                     
         (cons
                                                                     
          '(:e
                                                                     
            sshort-arrayp)
                                                                     
          (cons
                                                                     
           '(:e
                                                                     
             ushort-arrayp)
                                                                     
           (cons
                                                                     
            '(:e
                                                                     
              sint-arrayp)
                                                                     
            (cons
                                                                     
             '(:e
                                                                     
               uint-arrayp)
                                                                     
             (cons
                                                                     
              '(:e
                                                                     
                slong-arrayp)
                                                                     
              (cons
                                                                     
               '(:e
                                                                     
                 ulong-arrayp)
                                                                     
               (cons
                                                                     
                '(:e
                                                                     
                  sllong-arrayp)
                                                                     
                (cons
                                                                     
                 '(:e
                                                                     
                   ullong-arrayp)
                                                                     
                 (cons
                                                                     
                  '(:e
                                                                     
                    schar-array-length)
                                                                     
                  (cons
                                                                     
                   '(:e
                                                                     
                     uchar-array-length)
                                                                     
                   (cons
                                                                     
                    '(:e
                                                                     
                      sshort-array-length)
                                                                     
                    (cons
                                                                     
                     '(:e
                                                                     
                       ushort-array-length)
                                                                     
                     (cons
                                                                     
                      '(:e
                                                                     
                        sint-array-length)
                                                                     
                      (cons
                                                                     
                       '(:e
                                                                     
                         uint-array-length)
                                                                     
                       (cons
                                                                     
                        '(:e
                                                                     
                          slong-array-length)
                                                                     
                        (cons
                                                                     
                         '(:e
                                                                     
                           ulong-array-length)
                                                                     
                         (cons
                                                                     
                          '(:e
                                                                     
                            sllong-array-length)
                                                                     
                          (cons
                                                                     
                           '(:e
                                                                     
                             ullong-array-length)
                                                                     
                           (cons
                                                                     
                            '(:t
                                                                     
                              value-struct-write-aux)
                                                                     
                            (if
                                                                     
                             size?
                                                                     
                             '(acl2::posp-compound-recognizer
                                                                     
                               (:e
                                                                     
                                type-of-value)
                                                                     
                               defstruct-consp-len-lemma)
                                                                     
                             (cons
                                                                     
                              read-member-list
                                                                     
                              (cons
                                                                     
                               'value-struct-read
                                                                     
                               (cons
                                                                     
                                (cons
                                                                     
                                 ':e
                                                                     
                                 (cons
                                                                     
                                  fixtype-array->elements
                                                                     
                                  'nil))
                                                                     
                                '((:e
                                                                     
                                   len)
                                                                     
                                  returns-lemma))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    (events
     (append
      (and
       (not size?)
       (cons
        (cons
         'define
         (cons
          member-length
          (cons
           (cons (cons 'struct (cons struct-tag-p 'nil))
                 'nil)
           (cons
            ':returns
            (cons
             (cons
              'len
              (cons
               'natp
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                       (cons
                           member-length
                           (cons natp-of-fixtype-array-length 'nil))
                       'nil))
                     'nil)))
                  'nil)
                 'nil))))
             (cons
              (cons
               'b*
               (cons
                (cons
                 (cons
                  'array
                  (cons
                   (cons 'value-struct-read
                         (cons (cons 'ident
                                     (cons (ident->name name) 'nil))
                               (cons (cons struct-tag-fix '(struct))
                                     'nil)))
                   'nil))
                 'nil)
                (cons (cons fixtype-array-length '(array))
                      'nil)))
              (cons
               ':guard-simplify
               (cons
                ':limited
                (cons
                 ':guard-hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                       ':in-theory
                       (cons (cons 'quote
                                   (cons member-length-theory 'nil))
                             'nil)))
                   'nil)
                  (cons
                   '///
                   (cons
                    (cons
                     'fty::deffixequiv
                     (cons
                      member-length
                      (cons
                       ':hints
                       (cons
                        (cons
                         (cons
                          '"Goal"
                          (cons
                           ':in-theory
                           (cons
                            (cons
                             'quote
                             (cons
                              (cons
                               member-length
                               (cons
                                struct-tag-fix-when-struct-tag-p
                                (cons struct-tag-p-of-struct-tag-fix
                                      'nil)))
                              'nil))
                            'nil)))
                         'nil)
                        'nil))))
                    'nil))))))))))))
        'nil))
      (cons
       (cons
        'define
        (cons
         read-member
         (cons
          (cons (cons 'struct (cons struct-tag-p 'nil))
                'nil)
          (cons
           ':returns
           (cons
            (cons
             'val
             (cons
              fixtype-arrayp
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                       (cons 'quote
                             (cons read-member-returns-theory 'nil))
                       'nil)))
                 'nil)
                'nil))))
            (cons
             (cons 'value-struct-read
                   (cons (cons 'ident
                               (cons (ident->name name) 'nil))
                         (cons (cons struct-tag-fix '(struct))
                               'nil)))
             (cons
              ':guard-simplify
              (cons
               ':limited
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                       (cons
                           struct-tag-p
                           (cons struct-tag-fix '(identp-of-ident)))
                       'nil))
                     'nil)))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     read-member
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons
                             (cons
                              read-member
                              (cons
                               struct-tag-equiv-implies-equal-struct-tag-fix-1
                               (cons
                                struct-tag-fix-under-struct-tag-equiv
                                'nil)))
                             'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil))))))))))))
       (cons
        (cons
         'define
         (cons
          write-member
          (cons
           (cons (cons 'val (cons fixtype-arrayp 'nil))
                 (cons (cons 'struct (cons struct-tag-p 'nil))
                       'nil))
           (cons
            ':guard
            (cons
             (cons
               'equal
               (cons (cons fixtype-array-length '(val))
                     (cons (or size? (cons member-length '(struct)))
                           'nil)))
             (cons
              ':returns
              (cons
               (cons
                'new-struct
                (cons
                 struct-tag-p
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                            'quote
                            (cons write-member-returns-theory 'nil))
                       'nil)))
                    'nil)
                   'nil))))
               (cons
                (cons
                 'if
                 (cons
                  (cons
                   'mbt
                   (cons
                    (cons
                     'equal
                     (cons
                      (cons fixtype-array-length '(val))
                      (cons
                       (or
                         size?
                         (cons member-length
                               (cons (cons struct-tag-fix '(struct))
                                     'nil)))
                       'nil)))
                    'nil))
                  (cons
                   (cons
                    'value-struct-write
                    (cons
                         (cons 'ident
                               (cons (ident->name name) 'nil))
                         (cons (cons fixtype-array-fix '(val))
                               (cons (cons struct-tag-fix '(struct))
                                     'nil))))
                   (cons (cons struct-tag-fix '(struct))
                         'nil))))
                (cons
                 ':guard-simplify
                 (cons
                  ':limited
                  (cons
                   ':guard-hints
                   (cons
                    (cons
                     (cons
                      '"Goal"
                      (cons
                       ':in-theory
                       (cons
                        (cons
                         'quote
                         (cons
                          (cons
                           struct-tag-p
                           (cons
                            struct-tag-fix
                            (cons
                             valuep-when-fixtype-arrayp
                             (cons
                               fixtype-array-fix-when-fixtype-arrayp
                               '(identp-of-ident)))))
                          'nil))
                        'nil)))
                     'nil)
                    (cons
                     '///
                     (cons
                      (cons
                       'fty::deffixequiv
                       (cons
                        write-member
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'quote
                               (cons
                                (cons
                                 '(:e ident)
                                 (cons
                                  write-member
                                  (cons
                                   struct-tag-fix-when-struct-tag-p
                                   (cons
                                    struct-tag-p-of-struct-tag-fix
                                    (cons
                                     fixtype-array-fix-when-fixtype-arrayp
                                     (cons
                                      fixtype-arrayp-of-fixtype-array-fix
                                      (cons
                                       fixtype-array-length-of-fixtype-array-fix-array
                                       'nil)))))))
                                'nil))
                              'nil)))
                           'nil)
                          'nil))))
                      'nil))))))))))))))
        (cons
         (cons
          'define
          (cons
           member-index-okp
           (cons
            (cons '(index cintegerp)
                  (and (not size?)
                       (cons (cons 'struct (cons struct-tag-p 'nil))
                             'nil)))
            (cons
             ':returns
             (cons
              (cons
               'yes/no
               (cons
                'booleanp
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                      (cons 'quote
                            (cons (cons member-index-okp
                                        '(booleanp-compound-recognizer
                                              (:t integer-range-p)))
                                  'nil))
                      'nil)))
                   'nil)
                  'nil))))
              (cons
               (cons
                'integer-range-p
                (cons
                     '0
                     (cons (or size? (cons member-length '(struct)))
                           '((integer-from-cinteger index)))))
               (cons
                ':guard-simplify
                (cons
                 ':limited
                 (cons
                  ':guard-hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (and
                      (not size?)
                      (cons
                       ':use
                       (cons
                           (packn-pos (list 'natp-of- member-length)
                                      member-length)
                           '(:in-theory '(natp))))))
                    'nil)
                   (cons
                    '///
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       member-index-okp
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons
                               (cons
                                member-index-okp
                                (cons
                                 'integer-from-cinteger-of-cinteger-fix-cint
                                 (and
                                  (not size?)
                                  (list
                                   member-length-of-struct-tag-fix-struct))))
                               'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     'nil))))))))))))
         (cons
          (cons
           'define
           (cons
            read-member-element
            (cons
             (cons '(index cintegerp)
                   (cons (cons 'struct (cons struct-tag-p 'nil))
                         'nil))
             (cons
              ':guard
              (cons
               (cons member-index-okp
                     (cons 'index
                           (and (not size?) (list 'struct))))
               (cons
                ':returns
                (cons
                 (cons
                  'val
                  (cons
                   fixtypep
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons
                        ':in-theory
                        (cons
                         (cons
                          'quote
                          (cons
                           (cons
                            read-member-element
                            (cons
                               fixtypep-of-fixtype-array-read 'nil))
                           'nil))
                         'nil)))
                      'nil)
                     'nil))))
                 (cons
                  (cons fixtype-array-read
                        (cons (cons read-member '(struct))
                              '(index)))
                  (cons
                   ':guard-simplify
                   (cons
                    ':limited
                    (cons
                     ':guard-hints
                     (cons
                      (cons
                       (cons
                        '"Goal"
                        (cons
                         ':in-theory
                         (cons
                          (cons
                           'quote
                           (cons
                            (cons
                             struct-tag-p
                             (cons
                              struct-tag-fix-when-struct-tag-p
                              (cons
                               member-index-okp
                               (cons
                                read-member
                                (cons
                                 fixtype-array-index-okp
                                 (cons
                                  'value-struct-read
                                  (cons
                                   'integer-range-p
                                   (cons
                                    '(:e ident)
                                    (and
                                       (not size?)
                                       (list member-length))))))))))
                            'nil))
                          'nil)))
                       'nil)
                      (cons
                       '///
                       (cons
                        (cons
                         'fty::deffixequiv
                         (cons
                          read-member-element
                          (cons
                           ':hints
                           (cons
                            (cons
                             (cons
                              '"Goal"
                              (cons
                               ':in-theory
                               (cons
                                (cons
                                 'quote
                                 (cons
                                  (cons
                                   read-member-element
                                   (cons
                                    read-member-of-struct-tag-fix-struct
                                    (cons
                                     fixtype-array-read-of-cinteger-fix-index
                                     'nil)))
                                  'nil))
                                'nil)))
                             'nil)
                            'nil))))
                        'nil))))))))))))))
          (cons
           (cons
            'define
            (cons
             write-member-element
             (cons
              (cons
                 '(index cintegerp)
                 (cons (cons 'val (cons fixtypep 'nil))
                       (cons (cons 'struct (cons struct-tag-p 'nil))
                             'nil)))
              (cons
               ':guard
               (cons
                (cons member-index-okp
                      (cons 'index
                            (and (not size?) (list 'struct))))
                (cons
                 ':returns
                 (cons
                  (cons
                   'new-struct
                   (cons
                    struct-tag-p
                    (cons
                     ':hints
                     (cons
                      (cons
                       (cons
                        '"Goal"
                        (cons
                         ':in-theory
                         (cons
                          (cons
                           'quote
                           (cons
                            (cons
                             write-member-element
                             (cons
                                 struct-tag-p-of-write-member 'nil))
                            'nil))
                          'nil)))
                       'nil)
                      'nil))))
                  (cons
                   (cons
                      write-member
                      (cons (cons fixtype-array-write
                                  (cons (cons read-member '(struct))
                                        '(index val)))
                            '(struct)))
                   (cons
                    ':guard-simplify
                    (cons
                     ':limited
                     (cons
                      ':guard-hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons
                             (cons
                              struct-tag-p
                              (cons
                               read-member
                               (cons
                                member-index-okp
                                (cons
                                 struct-tag-fix-when-struct-tag-p
                                 (cons
                                  fixtype-array-index-okp
                                  (cons
                                   fixtype-arrayp-of-fixtype-array-write
                                   (cons
                                    fixtype-array-length-of-fixtype-array-write
                                    (cons
                                     'value-struct-read
                                     (cons
                                      '(:e ident)
                                      (and
                                       (not size?)
                                       (list
                                            member-length)))))))))))
                             'nil))
                           'nil)))
                        'nil)
                       (cons
                        '///
                        (cons
                         (cons
                          'fty::deffixequiv
                          (cons
                           write-member-element
                           (cons
                            ':hints
                            (cons
                             (cons
                              (cons
                               '"Goal"
                               (cons
                                ':in-theory
                                (cons
                                 (cons
                                  'quote
                                  (cons
                                   (cons
                                    write-member-element
                                    (cons
                                     fixtype-array-write-of-cinteger-fix-index
                                     (cons
                                      fixtype-array-write-of-fixtype-fix-element
                                      (cons
                                       read-member-of-struct-tag-fix-struct
                                       (cons
                                        write-member-of-struct-tag-fix-struct
                                        'nil)))))
                                   'nil))
                                 'nil)))
                              'nil)
                             'nil))))
                         'nil))))))))))))))
           (cons
            (cons
             'define
             (cons
              read-member-list
              (cons
               (cons (cons 'struct (cons struct-tag-p 'nil))
                     'nil)
               (cons
                ':returns
                (cons
                 (cons
                  'values
                  (cons
                   fixtype-listp
                   (cons
                    ':hints
                    (cons
                     (cons
                      (cons
                       '"Goal"
                       (cons
                        ':in-theory
                        (cons
                         (cons
                          'quote
                          (cons
                           (cons
                            read-member-list
                            (cons
                             fixtype-listp-of-fixtype-array->elements
                             'nil))
                           'nil))
                         'nil)))
                      'nil)
                     'nil))))
                 (cons
                  (cons
                   fixtype-array->elements
                   (cons
                    (cons
                         'value-struct-read
                         (cons (cons 'ident
                                     (cons (ident->name name) 'nil))
                               (cons (cons struct-tag-fix '(struct))
                                     'nil)))
                    'nil))
                  (cons
                   ':guard-simplify
                   (cons
                    ':limited
                    (cons
                     ':guard-hints
                     (cons
                      (cons
                       (cons
                        '"Goal"
                        (cons
                         ':in-theory
                         (cons
                          (cons
                           'quote
                           (cons
                            (cons
                             struct-tag-p
                             (cons
                                  struct-tag-fix
                                  '(value-struct-read (:e ident)
                                                      (:e identp))))
                            'nil))
                          'nil)))
                       'nil)
                      (cons
                       '///
                       (cons
                        (if size?
                         (cons
                          'defret
                          (cons
                           len-of-read-member-list
                           (cons
                            (cons
                             'equal
                             (cons '(len values) (cons size? 'nil)))
                            (cons
                             ':hints
                             (cons
                              (cons
                               (cons
                                '"Goal"
                                (cons
                                 ':in-theory
                                 (cons
                                  (cons
                                   'quote
                                   (cons
                                      len-of-read-member-list-theory
                                      'nil))
                                  'nil)))
                               'nil)
                              'nil)))))
                         (cons
                          'defret
                          (cons
                           consp-of-read-member-list
                           (cons
                            '(consp values)
                            (cons
                             ':rule-classes
                             (cons
                              ':type-prescription
                              (cons
                               ':hints
                               (cons
                                (cons
                                 (cons
                                  '"Goal"
                                  (cons
                                   ':in-theory
                                   (cons
                                    (cons
                                     'quote
                                     (cons
                                      (cons
                                       read-member-list
                                       (cons
                                        (cons
                                         ':t
                                         (cons
                                             fixtype-array->elements
                                             'nil))
                                        'nil))
                                      'nil))
                                    'nil)))
                                 'nil)
                                'nil))))))))
                        (cons
                         (cons
                          'fty::deffixequiv
                          (cons
                           read-member-list
                           (cons
                            ':hints
                            (cons
                             (cons
                              (cons
                               '"Goal"
                               (cons
                                ':in-theory
                                (cons
                                 (cons
                                  'quote
                                  (cons
                                   (cons
                                    read-member-list
                                    (cons
                                     struct-tag-fix-under-struct-tag-equiv
                                     (cons
                                      struct-tag-equiv-implies-equal-struct-tag-fix-1
                                      'nil)))
                                   'nil))
                                 'nil)))
                              'nil)
                             'nil))))
                         'nil)))))))))))))
            (cons
             (cons
              'define
              (cons
               write-member-list
               (cons
                (cons (cons 'values (cons fixtype-listp 'nil))
                      (cons (cons 'struct (cons struct-tag-p 'nil))
                            'nil))
                (cons
                 ':guard
                 (cons
                  write-member-list-extra-guard
                  (cons
                   ':returns
                   (cons
                    (cons
                     'new-struct
                     (cons
                      struct-tag-p
                      (cons
                       ':hyp
                       (cons
                        write-member-list-extra-guard
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"Goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'quote
                               (cons write-member-list-theory 'nil))
                              'nil)))
                           'nil)
                          'nil))))))
                    (cons
                     (cons
                      'value-struct-write
                      (cons
                         (cons 'ident
                               (cons (ident->name name) 'nil))
                         (cons (cons fixtype-array-of '(values))
                               (cons (cons struct-tag-fix '(struct))
                                     'nil))))
                     (cons
                      ':guard-simplify
                      (cons
                       ':limited
                       (cons
                        ':guard-hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons
                               (cons
                                struct-tag-p
                                (cons
                                 struct-tag-fix
                                 (cons
                                  valuep-when-fixtype-arrayp
                                  (cons
                                   true-listp-when-fixtype-listp
                                   (cons
                                    fixtype-arrayp-of-fixtype-array-of
                                    (append
                                     (if size? '(defstruct-consp-len-lemma
                                                     (:e posp))
                                      (cons
                                       '(:e len)
                                       (cons
                                        'defstruct-len-consp-lemma
                                        (cons
                                         consp-of-read-member-list
                                         (cons
                                          (cons
                                           ':t
                                           (cons
                                             read-member-list 'nil))
                                          'nil)))))
                                     '(identp-of-ident)))))))
                               'nil))
                             'nil)))
                          'nil)
                         (cons
                          ':prepwork
                          (cons
                           (cons
                            (cons
                             'defrulel
                             (cons
                              'returns-lemma
                              (cons
                               (cons
                                'implies
                                (cons
                                 (cons
                                  'equal
                                  (cons
                                   '(len values)
                                   (cons
                                    (cons
                                     'len
                                     (cons
                                      (cons
                                       fixtype-array->elements '(x))
                                      'nil))
                                    'nil)))
                                 '((consp values))))
                               (cons
                                ':in-theory
                                (cons
                                 (cons
                                  'quote
                                  (cons
                                   (cons
                                    'len
                                    (cons
                                     'defstruct-len-consp-lemma
                                     (cons
                                      (cons
                                       ':t
                                       (cons fixtype-array->elements
                                             'nil))
                                      'nil)))
                                   'nil))
                                 'nil)))))
                            'nil)
                           (cons
                            '///
                            (cons
                             (cons
                              'fty::deffixequiv
                              (cons
                               write-member-list
                               (cons
                                ':hints
                                (cons
                                 (cons
                                  (cons
                                   '"Goal"
                                   (cons
                                    ':in-theory
                                    (cons
                                     (cons
                                      'quote
                                      (cons
                                       (cons
                                        write-member-list
                                        (cons
                                         fixtype-array-of-of-fixtype-list-fix-elements
                                         (cons
                                          struct-tag-equiv-implies-equal-struct-tag-fix-1
                                          (cons
                                           struct-tag-fix-under-struct-tag-equiv
                                           'nil))))
                                       'nil))
                                     'nil)))
                                  'nil)
                                 'nil))))
                             'nil))))))))))))))))
             'nil)))))))))
    (event (cons 'encapsulate (cons 'nil events))))
   (mv event (and (not size?) member-length)
       member-index-okp
       read-member read-member-element
       write-member write-member-element
       (packn-pos (list fixtype-arrayp '-of- read-member)
                  read-member)
       (packn-pos (list fixtypep '-of-
                        read-member-element)
                  read-member-element)
       (packn-pos (list struct-tag-p '-of- write-member)
                  write-member)
       (packn-pos (list struct-tag-p '-of-
                        write-member-element)
                  write-member-element)))))

Theorem: pseudo-event-formp-of-defstruct-gen-array-member-ops.event

(defthm pseudo-event-formp-of-defstruct-gen-array-member-ops.event
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.length

(defthm symbolp-of-defstruct-gen-array-member-ops.length
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp length))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.checker

(defthm symbolp-of-defstruct-gen-array-member-ops.checker
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp checker))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.reader

(defthm symbolp-of-defstruct-gen-array-member-ops.reader
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp reader))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.reader-element

(defthm symbolp-of-defstruct-gen-array-member-ops.reader-element
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp reader-element))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.writer

(defthm symbolp-of-defstruct-gen-array-member-ops.writer
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp writer))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.writer-element

(defthm symbolp-of-defstruct-gen-array-member-ops.writer-element
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp writer-element))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.reader-return-thm

(defthm symbolp-of-defstruct-gen-array-member-ops.reader-return-thm
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp reader-return-thm))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.reader-element-return-thm

(defthm
 symbolp-of-defstruct-gen-array-member-ops.reader-element-return-thm
 (b* (((mv acl2::?event common-lisp::?length
           ?checker ?reader ?reader-element ?writer
           ?writer-element ?reader-return-thm
           ?reader-element-return-thm
           ?writer-return-thm
           ?writer-element-return-thm)
       (defstruct-gen-array-member-ops
            struct-tag struct-tag-p
            struct-tag-fix name type size?)))
   (symbolp reader-element-return-thm))
 :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.writer-return-thm

(defthm symbolp-of-defstruct-gen-array-member-ops.writer-return-thm
  (b* (((mv acl2::?event common-lisp::?length
            ?checker ?reader ?reader-element ?writer
            ?writer-element ?reader-return-thm
            ?reader-element-return-thm
            ?writer-return-thm
            ?writer-element-return-thm)
        (defstruct-gen-array-member-ops
             struct-tag struct-tag-p
             struct-tag-fix name type size?)))
    (symbolp writer-return-thm))
  :rule-classes :rewrite)

Theorem: symbolp-of-defstruct-gen-array-member-ops.writer-element-return-thm

(defthm
 symbolp-of-defstruct-gen-array-member-ops.writer-element-return-thm
 (b* (((mv acl2::?event common-lisp::?length
           ?checker ?reader ?reader-element ?writer
           ?writer-element ?reader-return-thm
           ?reader-element-return-thm
           ?writer-return-thm
           ?writer-element-return-thm)
       (defstruct-gen-array-member-ops
            struct-tag struct-tag-p
            struct-tag-fix name type size?)))
   (symbolp writer-element-return-thm))
 :rule-classes :rewrite)

Theorem: defstruct-len-consp-lemma

(defthm defstruct-len-consp-lemma
  (implies (consp x)
           (not (equal (len x) 0))))