		Search-engine friendly clone of the ACL2 documentation.

Proof-utilities

Pos

Position of element e in a list x

Signature
(pos e x) → *
Arguments: x — Guard (true-listp x).

We use this function to get the byte located at a memory address; thus, in our use case, e is the address, x is the region of memory represented as a true-list, and the return value is the byte at address e (if e is a valid address in x). We use this function exclusively on the output obtained from functions like rb and program-at.

Definitions and Theorems

Function: pos

(defun pos (e x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'pos))
    (declare (ignorable __function__))
    (pos-1 e x 0)))

Theorem: member-p-pos-non-nil

(defthm member-p-pos-non-nil
  (implies (member-p e x)
           (and (integerp (pos e x))
                (<= 0 (pos e x))))
  :rule-classes :type-prescription)

Theorem: member-p-pos-value

(defthm member-p-pos-value
  (implies (member-p e x)
           (< (pos e x) (len x)))
  :rule-classes :linear)

Theorem: not-member-p-pos-nil

(defthm not-member-p-pos-nil
  (implies (equal (member-p e x) nil)
           (equal (pos e x) nil)))

Theorem: nth-pos-of-list-first

(defthm nth-pos-of-list-first
  (implies (and (syntaxp (not (and (consp xs)
                                   (eq (car xs) 'addr-range))))
                (equal index (car xs))
                (consp xs))
           (equal (pos index xs) 0)))