		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-multirefs-top

Signature
(svexlist-multirefs-top x) → multirefs
Arguments: x — Guard (svexlist-p x).
Returns: multirefs — Type (svex-key-alist-p multirefs).

Definitions and Theorems

Function: svexlist-multirefs-top

(defun svexlist-multirefs-top (x)
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-multirefs-top))
    (declare (ignorable __function__))
    (b* (((mv seen multirefs)
          (svexlist-multirefs x nil nil)))
      (fast-alist-free seen)
      multirefs)))

Theorem: svex-key-alist-p-of-svexlist-multirefs-top

(defthm svex-key-alist-p-of-svexlist-multirefs-top
  (b* ((multirefs (svexlist-multirefs-top x)))
    (svex-key-alist-p multirefs))
  :rule-classes :rewrite)

Theorem: svexlist-multirefs-top-of-svexlist-fix-x

(defthm svexlist-multirefs-top-of-svexlist-fix-x
  (equal (svexlist-multirefs-top (svexlist-fix x))
         (svexlist-multirefs-top x)))

Theorem: svexlist-multirefs-top-svexlist-equiv-congruence-on-x

(defthm svexlist-multirefs-top-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-multirefs-top x)
                  (svexlist-multirefs-top x-equiv)))
  :rule-classes :congruence)