		Search-engine friendly clone of the ACL2 documentation.

Set-bi-induct

Induct over the structure of two sets simultaneously.

Signature
(set-bi-induct x y) → *

Definitions and Theorems

Function: set-bi-induct

(defun set-bi-induct (x y)
  (declare (xargs :guard t))
  (or (emptyp x)
      (emptyp y)
      (let ((left (set-bi-induct (left x) (left y)))
            (right (set-bi-induct (right x) (right y))))
        (declare (ignore left right))
        t)))