		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-symwildeq

Signature
(s4vec-symwildeq a b) → res
Arguments: a — Guard (s4vec-p a).; b — Guard (s4vec-p b).
Returns: res — Type (s4vec-p res).

Definitions and Theorems

Function: s4vec-symwildeq

(defun s4vec-symwildeq (a b)
 (declare (xargs :guard (and (s4vec-p a) (s4vec-p b))))
 (let ((__function__ 's4vec-symwildeq))
  (declare (ignorable __function__))
  (b*
   ((eq (s3vec-bitnot (s4vec-bitxor a b)))
    ((s4vec b))
    ((s4vec a))
    (zxmask (sparseint-bitor (sparseint-bitandc1 b.upper b.lower)
                             (sparseint-bitandc1 a.upper a.lower))))
   (s3vec-reduction-and (s3vec-bitor eq (s2vec zxmask))))))

Theorem: s4vec-p-of-s4vec-symwildeq

(defthm s4vec-p-of-s4vec-symwildeq
  (b* ((res (s4vec-symwildeq a b)))
    (s4vec-p res))
  :rule-classes :rewrite)

Theorem: s4vec-symwildeq-correct

(defthm s4vec-symwildeq-correct
  (b* ((?res (s4vec-symwildeq a b)))
    (equal (s4vec->4vec res)
           (4vec-symwildeq (s4vec->4vec a)
                           (s4vec->4vec b)))))

Theorem: s4vec-symwildeq-of-s4vec-fix-a

(defthm s4vec-symwildeq-of-s4vec-fix-a
  (equal (s4vec-symwildeq (s4vec-fix a) b)
         (s4vec-symwildeq a b)))

Theorem: s4vec-symwildeq-s4vec-equiv-congruence-on-a

(defthm s4vec-symwildeq-s4vec-equiv-congruence-on-a
  (implies (s4vec-equiv a a-equiv)
           (equal (s4vec-symwildeq a b)
                  (s4vec-symwildeq a-equiv b)))
  :rule-classes :congruence)

Theorem: s4vec-symwildeq-of-s4vec-fix-b

(defthm s4vec-symwildeq-of-s4vec-fix-b
  (equal (s4vec-symwildeq a (s4vec-fix b))
         (s4vec-symwildeq a b)))

Theorem: s4vec-symwildeq-s4vec-equiv-congruence-on-b

(defthm s4vec-symwildeq-s4vec-equiv-congruence-on-b
  (implies (s4vec-equiv b b-equiv)
           (equal (s4vec-symwildeq a b)
                  (s4vec-symwildeq a b-equiv)))
  :rule-classes :congruence)