		Search-engine friendly clone of the ACL2 documentation.

A4vec-ite

A4vec-ite-fn

Basic if-then-else for symbolic 4vecs.

Signature
(a4vec-ite-fn test then else) → res
Arguments: test — Test AIG (not a 4vec!).; then — Guard (a4vec-p then).; else — Guard (a4vec-p else).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a4vec-ite-fn

(defun a4vec-ite-fn (test then else)
 (declare (xargs :guard (and (a4vec-p then) (a4vec-p else))))
 (let ((__function__ 'a4vec-ite-fn))
  (declare (ignorable __function__))
  (cond
       ((eq test t) (a4vec-fix then))
       ((eq test nil) (a4vec-fix else))
       (t (b* (((a4vec then)) ((a4vec else)))
            (a4vec (aig-ite-bss-fn test then.upper else.upper)
                   (aig-ite-bss-fn test then.lower else.lower)))))))

Theorem: a4vec-p-of-a4vec-ite-fn

(defthm a4vec-p-of-a4vec-ite-fn
  (b* ((res (a4vec-ite-fn test then else)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-ite-fn-correct

(defthm a4vec-ite-fn-correct
  (equal (a4vec-eval (a4vec-ite-fn test then else)
                     env)
         (if (aig-eval test env)
             (a4vec-eval then env)
           (a4vec-eval else env))))

Theorem: a4vec-ite-fn-of-const-tests

(defthm a4vec-ite-fn-of-const-tests
  (and (equal (a4vec-ite-fn t then else)
              (a4vec-fix then))
       (equal (a4vec-ite-fn nil then else)
              (a4vec-fix else))))

Theorem: a4vec-ite-fn-of-a4vec-fix-then

(defthm a4vec-ite-fn-of-a4vec-fix-then
  (equal (a4vec-ite-fn test (a4vec-fix then)
                       else)
         (a4vec-ite-fn test then else)))

Theorem: a4vec-ite-fn-a4vec-equiv-congruence-on-then

(defthm a4vec-ite-fn-a4vec-equiv-congruence-on-then
  (implies (a4vec-equiv then then-equiv)
           (equal (a4vec-ite-fn test then else)
                  (a4vec-ite-fn test then-equiv else)))
  :rule-classes :congruence)

Theorem: a4vec-ite-fn-of-a4vec-fix-else

(defthm a4vec-ite-fn-of-a4vec-fix-else
  (equal (a4vec-ite-fn test then (a4vec-fix else))
         (a4vec-ite-fn test then else)))

Theorem: a4vec-ite-fn-a4vec-equiv-congruence-on-else

(defthm a4vec-ite-fn-a4vec-equiv-congruence-on-else
  (implies (a4vec-equiv else else-equiv)
           (equal (a4vec-ite-fn test then else)
                  (a4vec-ite-fn test then else-equiv)))
  :rule-classes :congruence)