		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-rev-blocks

Signature
(a4vec-rev-blocks w b x) → res
Arguments: w — Guard (a4vec-p w).; b — Guard (a4vec-p b).; x — Guard (a4vec-p x).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: a4vec-rev-blocks

(defun a4vec-rev-blocks (w b x)
  (declare (xargs :guard (and (a4vec-p w)
                              (a4vec-p b)
                              (a4vec-p x))))
  (let ((__function__ 'a4vec-rev-blocks))
    (declare (ignorable __function__))
    (b* (((a4vec w) w)
         ((a4vec b) b)
         ((a4vec x) x))
      (a4vec-ite
           (aig-and (a2vec-p w)
                    (aig-not (aig-sign-s w.upper))
                    (a2vec-p b)
                    (aig-not (aig-sign-s b.upper))
                    (aig-not (aig-=-ss b.upper nil)))
           (a4vec (aig-rev-blocks-sss 0 0 w.upper b.upper x.upper)
                  (aig-rev-blocks-sss 0 0 w.upper b.upper x.lower))
           (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-rev-blocks

(defthm a4vec-p-of-a4vec-rev-blocks
  (b* ((res (a4vec-rev-blocks w b x)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-rev-blocks-correct

(defthm a4vec-rev-blocks-correct
  (equal (a4vec-eval (a4vec-rev-blocks w b x)
                     env)
         (4vec-rev-blocks (a4vec-eval w env)
                          (a4vec-eval b env)
                          (a4vec-eval x env))))

Theorem: a4vec-rev-blocks-of-a4vec-fix-w

(defthm a4vec-rev-blocks-of-a4vec-fix-w
  (equal (a4vec-rev-blocks (a4vec-fix w) b x)
         (a4vec-rev-blocks w b x)))

Theorem: a4vec-rev-blocks-a4vec-equiv-congruence-on-w

(defthm a4vec-rev-blocks-a4vec-equiv-congruence-on-w
  (implies (a4vec-equiv w w-equiv)
           (equal (a4vec-rev-blocks w b x)
                  (a4vec-rev-blocks w-equiv b x)))
  :rule-classes :congruence)

Theorem: a4vec-rev-blocks-of-a4vec-fix-b

(defthm a4vec-rev-blocks-of-a4vec-fix-b
  (equal (a4vec-rev-blocks w (a4vec-fix b) x)
         (a4vec-rev-blocks w b x)))

Theorem: a4vec-rev-blocks-a4vec-equiv-congruence-on-b

(defthm a4vec-rev-blocks-a4vec-equiv-congruence-on-b
  (implies (a4vec-equiv b b-equiv)
           (equal (a4vec-rev-blocks w b x)
                  (a4vec-rev-blocks w b-equiv x)))
  :rule-classes :congruence)

Theorem: a4vec-rev-blocks-of-a4vec-fix-x

(defthm a4vec-rev-blocks-of-a4vec-fix-x
  (equal (a4vec-rev-blocks w b (a4vec-fix x))
         (a4vec-rev-blocks w b x)))

Theorem: a4vec-rev-blocks-a4vec-equiv-congruence-on-x

(defthm a4vec-rev-blocks-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a4vec-rev-blocks w b x)
                  (a4vec-rev-blocks w b x-equiv)))
  :rule-classes :congruence)

Subtopics

Aig-rev-blocks-nss
Aig-rev-blocks-nns