		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-<

Integer less-than for 4vecs.

Signature
(4vec-< x y) → less
Arguments: x — Guard (4vec-p x).; y — Guard (4vec-p y).
Returns: less — Type (4vec-p less).

We return, following the boolean-convention,

All Xes when if either input has any X or Z bits, or else
True (all 1s) when x < y, or else
False (all 0s) otherwise.

This is a fairly conservative definition in the style of the Verilog semantics: if either input has X or Z bits, the result is all X bits. We return all Xes even in cases where the comparison would ``obviously'' go a certain way. For instance, if you compare 4'b 0100 < 4'b 011X, we return all Xes even though a less conservative semantics might say that the comparison will be true.

Definitions and Theorems

Function: 4vec-<

(defun 4vec-< (x y)
  (declare (xargs :guard (and (4vec-p x) (4vec-p y))))
  (let ((__function__ '4vec-<))
    (declare (ignorable __function__))
    (if (and (2vec-p x) (2vec-p y))
        (2vec (bool->vec (< (the integer (2vec->val x))
                            (the integer (2vec->val y)))))
      (4vec-x))))

Theorem: 4vec-p-of-4vec-<

(defthm 4vec-p-of-4vec-<
  (b* ((less (4vec-< x y))) (4vec-p less))
  :rule-classes :rewrite)

Theorem: 4vec-<-of-2vecx-fix-x

(defthm 4vec-<-of-2vecx-fix-x
  (equal (4vec-< (2vecx-fix x) y)
         (4vec-< x y)))

Theorem: 4vec-<-2vecx-equiv-congruence-on-x

(defthm 4vec-<-2vecx-equiv-congruence-on-x
  (implies (2vecx-equiv x x-equiv)
           (equal (4vec-< x y) (4vec-< x-equiv y)))
  :rule-classes :congruence)

Theorem: 4vec-<-of-2vecx-fix-y

(defthm 4vec-<-of-2vecx-fix-y
  (equal (4vec-< x (2vecx-fix y))
         (4vec-< x y)))

Theorem: 4vec-<-2vecx-equiv-congruence-on-y

(defthm 4vec-<-2vecx-equiv-congruence-on-y
  (implies (2vecx-equiv y y-equiv)
           (equal (4vec-< x y) (4vec-< x y-equiv)))
  :rule-classes :congruence)