		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-?*

Atomic if-then-else of 4vecs. Has the property that when branches are equal, the result is equal to the branch, regardless of the test.

Signature
(4vec-?* test then else) → choice
Arguments: test — Guard (4vec-p test).; then — Guard (4vec-p then).; else — Guard (4vec-p else).
Returns: choice — Type (4vec-p choice).

Definitions and Theorems

Function: 4vec-?*

(defun 4vec-?* (test then else)
  (declare (xargs :guard (and (4vec-p test)
                              (4vec-p then)
                              (4vec-p else))))
  (let ((__function__ '4vec-?*))
    (declare (ignorable __function__))
    (3vec-?* (3vec-fix test) then else)))

Theorem: 4vec-p-of-4vec-?*

(defthm 4vec-p-of-4vec-?*
  (b* ((choice (4vec-?* test then else)))
    (4vec-p choice))
  :rule-classes :rewrite)

Theorem: 4vec-?*-of-3vec-fix-test

(defthm 4vec-?*-of-3vec-fix-test
  (equal (4vec-?* (3vec-fix test) then else)
         (4vec-?* test then else)))

Theorem: 4vec-?*-3vec-equiv-congruence-on-test

(defthm 4vec-?*-3vec-equiv-congruence-on-test
  (implies (3vec-equiv test test-equiv)
           (equal (4vec-?* test then else)
                  (4vec-?* test-equiv then else)))
  :rule-classes :congruence)

Theorem: 4vec-?*-of-4vec-fix-then

(defthm 4vec-?*-of-4vec-fix-then
  (equal (4vec-?* test (4vec-fix then) else)
         (4vec-?* test then else)))

Theorem: 4vec-?*-4vec-equiv-congruence-on-then

(defthm 4vec-?*-4vec-equiv-congruence-on-then
  (implies (4vec-equiv then then-equiv)
           (equal (4vec-?* test then else)
                  (4vec-?* test then-equiv else)))
  :rule-classes :congruence)

Theorem: 4vec-?*-of-4vec-fix-else

(defthm 4vec-?*-of-4vec-fix-else
  (equal (4vec-?* test then (4vec-fix else))
         (4vec-?* test then else)))

Theorem: 4vec-?*-4vec-equiv-congruence-on-else

(defthm 4vec-?*-4vec-equiv-congruence-on-else
  (implies (4vec-equiv else else-equiv)
           (equal (4vec-?* test then else)
                  (4vec-?* test then else-equiv)))
  :rule-classes :congruence)