		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Ullong-array-write

Write an element to an array of type unsigned long long, using a c integer index.

Signature
(ullong-array-write array index element) → new-array
Arguments: array — Guard (ullong-arrayp array).; index — Guard (cintegerp index).; element — Guard (ullongp element).
Returns: new-array — Type (ullong-arrayp new-array).

Definitions and Theorems

Function: ullong-array-write

(defun ullong-array-write (array index element)
 (declare (xargs :guard (and (ullong-arrayp array)
                             (cintegerp index)
                             (ullongp element))))
 (declare (xargs :guard (ullong-array-index-okp array index)))
 (let ((__function__ 'ullong-array-write))
   (declare (ignorable __function__))
   (if (mbt (ullong-array-index-okp array index))
       (ullong-array-of (update-nth (integer-from-cinteger index)
                                    (ullong-fix element)
                                    (ullong-array->elements array)))
     (ullong-array-fix array))))

Theorem: ullong-arrayp-of-ullong-array-write

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

Theorem: len-of-ullong-array->elements-of-ullong-array-write

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

Theorem: ullong-array-length-of-ullong-array-write

(defthm ullong-array-length-of-ullong-array-write
 (equal
      (ullong-array-length (ullong-array-write array index element))
      (ullong-array-length array)))

Theorem: ullong-array-write-to-integer-write

(defthm ullong-array-write-to-integer-write
 (equal
     (ullong-array-write array index val)
     (ullong-array-integer-write array (integer-from-cinteger index)
                                 val)))

Theorem: ullong-array-write-alt-def

(defthm ullong-array-write-alt-def
  (implies (and (ullong-arrayp array)
                (cintegerp index)
                (ullongp elem)
                (ullong-array-index-okp array index))
           (equal (ullong-array-write array index elem)
                  (value-array-write (integer-from-cinteger index)
                                     elem array))))

Theorem: ullong-array-write-of-ullong-array-fix-array

(defthm ullong-array-write-of-ullong-array-fix-array
  (equal (ullong-array-write (ullong-array-fix array)
                             index element)
         (ullong-array-write array index element)))

Theorem: ullong-array-write-ullong-array-equiv-congruence-on-array

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

Theorem: ullong-array-write-of-cinteger-fix-index

(defthm ullong-array-write-of-cinteger-fix-index
  (equal (ullong-array-write array (cinteger-fix index)
                             element)
         (ullong-array-write array index element)))

Theorem: ullong-array-write-cinteger-equiv-congruence-on-index

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

Theorem: ullong-array-write-of-ullong-fix-element

(defthm ullong-array-write-of-ullong-fix-element
  (equal (ullong-array-write array index (ullong-fix element))
         (ullong-array-write array index element)))

Theorem: ullong-array-write-ullong-equiv-congruence-on-element

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