		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))))