		Search-engine friendly clone of the ACL2 documentation.

4v-<=

4v-list-<=

Extension of 4v-<= to four-valued lists.

We say X <= Y for four-valued lists when:

Y is at least as long as X, and
Xi <= Yi for all i up to |X|.

Definitions and Theorems

Function: 4v-list-<=

(defun 4v-list-<= (x y)
  (declare (xargs :guard t))
  (if (atom x)
      t
    (and (consp y)
         (4v-<= (car x) (car y))
         (4v-list-<= (cdr x) (cdr y)))))

Theorem: 4v-list-<=-nth

(defthm 4v-list-<=-nth
  (implies (4v-list-<= a b)
           (4v-<= (nth n a) (nth n b))))