		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A3vec-?

Symbolic version of 3vec-?.

Signature
(a3vec-? x y y3p z z3p) → res
Arguments: x — Guard (a4vec-p x).; y — Guard (a4vec-p y).; z — Guard (a4vec-p z).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a3vec-?

(defun a3vec-? (x y y3p z z3p)
 (declare (xargs :guard (and (a4vec-p x)
                             (a4vec-p y)
                             (a4vec-p z))))
 (let ((__function__ 'a3vec-?))
  (declare (ignorable __function__))
  (b*
   (((a4vec a) x)
    ((a4vec b) y)
    ((a4vec c) z)
    (a=1 (aig-not (aig-iszero-s a.lower)))
    (a=0 (aig-iszero-s a.upper))
    (a=x (aig-nor a=1 a=0))
    (boolcase (aig-logior-ss (aig-ite-bss-fn a=1 b.upper nil)
                             (aig-ite-bss-fn a=0 c.upper nil)))
    (upper
        (aig-logior-ss
             boolcase
             (aig-ite-bss
                  a=x
                  (aig-logior-ss (if z3p c.upper
                                   (aig-logior-ss c.upper c.lower))
                                 (if y3p b.upper
                                   (aig-logior-ss b.upper b.lower)))
                  nil)))
    (boolcase (aig-logior-ss (aig-ite-bss-fn a=1 b.lower nil)
                             (aig-ite-bss-fn a=0 c.lower nil)))
    (lower
        (aig-logior-ss
             boolcase
             (aig-ite-bss
                  a=x
                  (aig-logand-ss (if z3p c.lower
                                   (aig-logand-ss c.upper c.lower))
                                 (if y3p b.lower
                                   (aig-logand-ss b.upper b.lower)))
                  nil))))
   (a4vec upper lower))))

Theorem: a4vec-p-of-a3vec-?

(defthm a4vec-p-of-a3vec-?
  (b* ((res (a3vec-? x y y3p z z3p)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a3vec-?-correct

(defthm a3vec-?-correct
  (implies
       (and (case-split (implies y3p (3vec-p (a4vec-eval y env))))
            (case-split (implies z3p (3vec-p (a4vec-eval z env))))
            (3vec-p (a4vec-eval x env)))
       (equal (a4vec-eval (a3vec-? x y y3p z z3p) env)
              (3vec-? (a4vec-eval x env)
                      (a4vec-eval y env)
                      (a4vec-eval z env)))))

Theorem: a3vec-?-of-a4vec-fix-x

(defthm a3vec-?-of-a4vec-fix-x
  (equal (a3vec-? (a4vec-fix x) y y3p z z3p)
         (a3vec-? x y y3p z z3p)))

Theorem: a3vec-?-a4vec-equiv-congruence-on-x

(defthm a3vec-?-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a3vec-? x y y3p z z3p)
                  (a3vec-? x-equiv y y3p z z3p)))
  :rule-classes :congruence)

Theorem: a3vec-?-of-a4vec-fix-y

(defthm a3vec-?-of-a4vec-fix-y
  (equal (a3vec-? x (a4vec-fix y) y3p z z3p)
         (a3vec-? x y y3p z z3p)))

Theorem: a3vec-?-a4vec-equiv-congruence-on-y

(defthm a3vec-?-a4vec-equiv-congruence-on-y
  (implies (a4vec-equiv y y-equiv)
           (equal (a3vec-? x y y3p z z3p)
                  (a3vec-? x y-equiv y3p z z3p)))
  :rule-classes :congruence)

Theorem: a3vec-?-of-a4vec-fix-z

(defthm a3vec-?-of-a4vec-fix-z
  (equal (a3vec-? x y y3p (a4vec-fix z) z3p)
         (a3vec-? x y y3p z z3p)))

Theorem: a3vec-?-a4vec-equiv-congruence-on-z

(defthm a3vec-?-a4vec-equiv-congruence-on-z
  (implies (a4vec-equiv z z-equiv)
           (equal (a3vec-? x y y3p z z3p)
                  (a3vec-? x y y3p z-equiv z3p)))
  :rule-classes :congruence)