		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-override

Symbolic version of 4vec-override.

Signature
(a4vec-override stronger weaker) → res
Arguments: stronger — Guard (a4vec-p stronger).; weaker — Guard (a4vec-p weaker).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a4vec-override

(defun a4vec-override (stronger weaker)
 (declare (xargs :guard (and (a4vec-p stronger)
                             (a4vec-p weaker))))
 (let ((__function__ 'a4vec-override))
  (declare (ignorable __function__))
  (b* (((a4vec stronger)) ((a4vec weaker)))
   (a4vec (aig-logior-ss (aig-logand-ss stronger.lower weaker.upper)
                         stronger.upper)
          (aig-logand-ss (aig-logior-ss stronger.upper weaker.lower)
                         stronger.lower)))))

Theorem: a4vec-p-of-a4vec-override

(defthm a4vec-p-of-a4vec-override
  (b* ((res (a4vec-override stronger weaker)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-override-correct

(defthm a4vec-override-correct
  (equal (a4vec-eval (a4vec-override x y) env)
         (4vec-override (a4vec-eval x env)
                        (a4vec-eval y env))))

Theorem: a4vec-override-of-a4vec-fix-stronger

(defthm a4vec-override-of-a4vec-fix-stronger
  (equal (a4vec-override (a4vec-fix stronger)
                         weaker)
         (a4vec-override stronger weaker)))

Theorem: a4vec-override-a4vec-equiv-congruence-on-stronger

(defthm a4vec-override-a4vec-equiv-congruence-on-stronger
  (implies (a4vec-equiv stronger stronger-equiv)
           (equal (a4vec-override stronger weaker)
                  (a4vec-override stronger-equiv weaker)))
  :rule-classes :congruence)

Theorem: a4vec-override-of-a4vec-fix-weaker

(defthm a4vec-override-of-a4vec-fix-weaker
  (equal (a4vec-override stronger (a4vec-fix weaker))
         (a4vec-override stronger weaker)))

Theorem: a4vec-override-a4vec-equiv-congruence-on-weaker

(defthm a4vec-override-a4vec-equiv-congruence-on-weaker
  (implies (a4vec-equiv weaker weaker-equiv)
           (equal (a4vec-override stronger weaker)
                  (a4vec-override stronger weaker-equiv)))
  :rule-classes :congruence)