		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)))