Read an element from an array of type
(ushort-array-integer-read array index) → element
Function:
(defun ushort-array-integer-read (array index) (declare (xargs :guard (and (ushort-arrayp array) (integerp index)))) (declare (xargs :guard (ushort-array-integer-index-okp array index))) (let ((__function__ 'ushort-array-integer-read)) (declare (ignorable __function__)) (ushort-fix (nth index (ushort-array->elements array)))))
Theorem:
(defthm ushortp-of-ushort-array-integer-read (b* ((element (ushort-array-integer-read array index))) (ushortp element)) :rule-classes :rewrite)
Theorem:
(defthm ushort-array-integer-read-of-ushort-array-fix-array (equal (ushort-array-integer-read (ushort-array-fix array) index) (ushort-array-integer-read array index)))
Theorem:
(defthm ushort-array-integer-read-ushort-array-equiv-congruence-on-array (implies (ushort-array-equiv array array-equiv) (equal (ushort-array-integer-read array index) (ushort-array-integer-read array-equiv index))) :rule-classes :congruence)
Theorem:
(defthm ushort-array-integer-read-of-ifix-index (equal (ushort-array-integer-read array (ifix index)) (ushort-array-integer-read array index)))
Theorem:
(defthm ushort-array-integer-read-int-equiv-congruence-on-index (implies (acl2::int-equiv index index-equiv) (equal (ushort-array-integer-read array index) (ushort-array-integer-read array index-equiv))) :rule-classes :congruence)
Theorem:
(defthm ushort-array-integer-read-alt-def (implies (and (ushort-arrayp array) (integerp index) (ushort-array-integer-index-okp array index)) (equal (ushort-array-integer-read array index) (value-array-read index array))))