		Search-engine friendly clone of the ACL2 documentation.

Validator-states

Address+pos-pairs-with-address

Retrieve, from a set of pairs of addresses and positive integers, the pairs with a given address.

Signature
(address+pos-pairs-with-address addr pairs) → pairs-with-addr
Arguments: addr — Guard (addressp addr).; pairs — Guard (address+pos-setp pairs).
Returns: pairs-with-addr — Type (address+pos-setp pairs-with-addr).

Definitions and Theorems

Function: address+pos-pairs-with-address

(defun address+pos-pairs-with-address (addr pairs)
 (declare (xargs :guard (and (addressp addr)
                             (address+pos-setp pairs))))
 (let ((__function__ 'address+pos-pairs-with-address))
   (declare (ignorable __function__))
   (b* (((when (emptyp pairs)) nil)
        (pair (head pairs)))
     (if (equal (address-fix addr)
                (address+pos->address pair))
         (insert (address+pos-fix pair)
                 (address+pos-pairs-with-address addr (tail pairs)))
       (address+pos-pairs-with-address addr (tail pairs))))))

Theorem: address+pos-setp-of-address+pos-pairs-with-address

(defthm address+pos-setp-of-address+pos-pairs-with-address
 (b* ((pairs-with-addr (address+pos-pairs-with-address addr pairs)))
   (address+pos-setp pairs-with-addr))
 :rule-classes :rewrite)

Theorem: address+pos-pairs-with-address-of-address-fix-addr

(defthm address+pos-pairs-with-address-of-address-fix-addr
  (equal (address+pos-pairs-with-address (address-fix addr)
                                         pairs)
         (address+pos-pairs-with-address addr pairs)))

Theorem: address+pos-pairs-with-address-address-equiv-congruence-on-addr

(defthm
    address+pos-pairs-with-address-address-equiv-congruence-on-addr
 (implies (address-equiv addr addr-equiv)
          (equal (address+pos-pairs-with-address addr pairs)
                 (address+pos-pairs-with-address addr-equiv pairs)))
 :rule-classes :congruence)

Theorem: address+pos-pairs-with-address-of-nil

(defthm address+pos-pairs-with-address-of-nil
  (equal (address+pos-pairs-with-address addr nil)
         nil))

Theorem: in-of-address+pos-pairs-with-address

(defthm in-of-address+pos-pairs-with-address
  (implies (address+pos-setp pairs)
           (equal (in pair
                      (address+pos-pairs-with-address addr pairs))
                  (and (in pair pairs)
                       (equal (address+pos->address pair)
                              (address-fix addr))))))

Theorem: address+pos-pairs-with-address-of-insert

(defthm address+pos-pairs-with-address-of-insert
 (implies
    (and (address+pos-p pair)
         (address+pos-setp pairs))
    (equal (address+pos-pairs-with-address addr (insert pair pairs))
           (if (equal (address+pos->address pair)
                      (address-fix addr))
               (insert pair
                       (address+pos-pairs-with-address addr pairs))
             (address+pos-pairs-with-address addr pairs)))))

Theorem: address+pos-pairs-with-address-of-delete

(defthm address+pos-pairs-with-address-of-delete
 (implies
    (address+pos-setp pairs)
    (equal (address+pos-pairs-with-address addr (delete pair pairs))
           (delete pair
                   (address+pos-pairs-with-address addr pairs)))))

Theorem: author+round-pair-in-pairs-with-author

(defthm author+round-pair-in-pairs-with-author
  (implies (and (address+pos-setp pairs)
                (in (address+pos author round) pairs))
           (in (address+pos author round)
               (address+pos-pairs-with-address author pairs))))

Theorem: no-author+round-pair-if-no-pairs-with-author

(defthm no-author+round-pair-if-no-pairs-with-author
  (implies (and (address+pos-setp pairs)
                (equal (address+pos-pairs-with-address author pairs)
                       nil))
           (not (in (address+pos author round) pairs))))