		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-implies-lists

(4vs-implies-lists x y) pairwise impliess together the sexprs from the lists x and y, forming a new sexpr list.

Definitions and Theorems

Function: 4vs-implies-lists

(defun 4vs-implies-lists (x y)
  (declare (xargs :guard (equal (len x) (len y))))
  (if (atom x)
      nil
    (cons (4vs-implies (car x) (car y))
          (4vs-implies-lists (cdr x) (cdr y)))))