		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Rev-keys

Signature
(rev-keys x acc) → keys
Arguments: x — Guard (alistp x).; acc — Guard (true-listp acc).
Returns: keys — Type (true-listp keys).

Definitions and Theorems

Function: rev-keys

(defun rev-keys (x acc)
  (declare (xargs :guard (and (alistp x) (true-listp acc))))
  (let ((__function__ 'rev-keys))
    (declare (ignorable __function__))
    (if (atom x)
        (mbe :logic (list-fix acc) :exec acc)
      (rev-keys (cdr x)
                (mbe :logic
                     (if (consp (car x))
                         (cons (caar x) acc)
                       acc)
                     :exec (cons (caar x) acc))))))

Theorem: true-listp-of-rev-keys

(defthm true-listp-of-rev-keys
  (b* ((keys (rev-keys x acc)))
    (true-listp keys))
  :rule-classes :rewrite)

Theorem: rev-keys-is-revappend-of-keys

(defthm rev-keys-is-revappend-of-keys
  (b* nil
    (equal (rev-keys x acc)
           (revappend (alist-keys x)
                      (list-fix acc)))))

Theorem: rev-keys-of-list-fix-acc

(defthm rev-keys-of-list-fix-acc
  (equal (rev-keys x (list-fix acc))
         (rev-keys x acc)))

Theorem: rev-keys-list-equiv-congruence-on-acc

(defthm rev-keys-list-equiv-congruence-on-acc
  (implies (list-equiv acc acc-equiv)
           (equal (rev-keys x acc)
                  (rev-keys x acc-equiv)))
  :rule-classes :congruence)