		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Ushort-array-integer-write

Write an element to an array of type unsigned short, using an ACL2 integer index.

Signature
(ushort-array-integer-write array index element) → new-array
Arguments: array — Guard (ushort-arrayp array).; index — Guard (integerp index).; element — Guard (ushortp element).
Returns: new-array — Type (ushort-arrayp new-array).

Definitions and Theorems

Function: ushort-array-integer-write

(defun ushort-array-integer-write (array index element)
  (declare (xargs :guard (and (ushort-arrayp array)
                              (integerp index)
                              (ushortp element))))
  (declare
       (xargs :guard (ushort-array-integer-index-okp array index)))
  (let ((__function__ 'ushort-array-integer-write))
    (declare (ignorable __function__))
    (b* ((array (ushort-array-fix array))
         (index (ifix index))
         (element (ushort-fix element)))
      (if (mbt (ushort-array-integer-index-okp array index))
          (ushort-array-of
               (update-nth index
                           element (ushort-array->elements array)))
        array))))

Theorem: ushort-arrayp-of-ushort-array-integer-write

(defthm ushort-arrayp-of-ushort-array-integer-write
  (b* ((new-array (ushort-array-integer-write array index element)))
    (ushort-arrayp new-array))
  :rule-classes :rewrite)

Theorem: len-of-ushort-array->elements-of-ushort-array-integer-write

(defthm len-of-ushort-array->elements-of-ushort-array-integer-write
 (equal (len (ushort-array->elements
                  (ushort-array-integer-write array index element)))
        (len (ushort-array->elements array))))

Theorem: ushort-array-length-of-ushort-array-integer-write

(defthm ushort-array-length-of-ushort-array-integer-write
  (equal (ushort-array-length
              (ushort-array-integer-write array index element))
         (ushort-array-length array)))

Theorem: ushort-array-integer-write-alt-def

(defthm ushort-array-integer-write-alt-def
  (implies (and (ushort-arrayp array)
                (integerp index)
                (ushortp elem)
                (ushort-array-integer-index-okp array index))
           (equal (ushort-array-integer-write array index elem)
                  (value-array-write index elem array))))

Theorem: ushort-array-integer-write-of-ushort-array-fix-array

(defthm ushort-array-integer-write-of-ushort-array-fix-array
  (equal (ushort-array-integer-write (ushort-array-fix array)
                                     index element)
         (ushort-array-integer-write array index element)))

Theorem: ushort-array-integer-write-ushort-array-equiv-congruence-on-array

(defthm
  ushort-array-integer-write-ushort-array-equiv-congruence-on-array
 (implies
     (ushort-array-equiv array array-equiv)
     (equal (ushort-array-integer-write array index element)
            (ushort-array-integer-write array-equiv index element)))
 :rule-classes :congruence)

Theorem: ushort-array-integer-write-of-ifix-index

(defthm ushort-array-integer-write-of-ifix-index
  (equal (ushort-array-integer-write array (ifix index)
                                     element)
         (ushort-array-integer-write array index element)))

Theorem: ushort-array-integer-write-int-equiv-congruence-on-index

(defthm ushort-array-integer-write-int-equiv-congruence-on-index
 (implies
     (acl2::int-equiv index index-equiv)
     (equal (ushort-array-integer-write array index element)
            (ushort-array-integer-write array index-equiv element)))
 :rule-classes :congruence)

Theorem: ushort-array-integer-write-of-ushort-fix-element

(defthm ushort-array-integer-write-of-ushort-fix-element
  (equal
       (ushort-array-integer-write array index (ushort-fix element))
       (ushort-array-integer-write array index element)))

Theorem: ushort-array-integer-write-ushort-equiv-congruence-on-element

(defthm
      ushort-array-integer-write-ushort-equiv-congruence-on-element
 (implies
     (ushort-equiv element element-equiv)
     (equal (ushort-array-integer-write array index element)
            (ushort-array-integer-write array index element-equiv)))
 :rule-classes :congruence)