		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

4veclist-separate-upper-lower-rec-log

Signature
(4veclist-separate-upper-lower-rec-log n x rest-upper rest-lower) → (mv uppers lowers)
Arguments: n — Guard (natp n).; x — Guard (4veclist-p x).; rest-upper — Guard (integer-listp rest-upper).; rest-lower — Guard (integer-listp rest-lower).
Returns: uppers — Type (integer-listp uppers), given (integer-listp rest-upper).; lowers — Type (integer-listp lowers), given (integer-listp rest-lower).

Definitions and Theorems

Function: 4veclist-separate-upper-lower-rec-log

(defun 4veclist-separate-upper-lower-rec-log
       (n x rest-upper rest-lower)
 (declare (xargs :guard (and (natp n)
                             (4veclist-p x)
                             (integer-listp rest-upper)
                             (integer-listp rest-lower))))
 (declare (xargs :guard (<= n (len x))))
 (let ((__function__ '4veclist-separate-upper-lower-rec-log))
  (declare (ignorable __function__))
  (if (zp n)
      (mv rest-upper rest-lower)
   (b*
    (((4vec x1) (car x))
     (n (1- n))
     (x (cdr x))
     (halfn (ash n -1))
     (restn (- n halfn))
     ((mv rest-upper rest-lower)
      (4veclist-separate-upper-lower-rec-log restn (nthcdr halfn x)
                                             rest-upper rest-lower))
     ((mv rest-upper rest-lower)
      (4veclist-separate-upper-lower-rec-log
           halfn x rest-upper rest-lower)))
    (mv (cons x1.upper rest-upper)
        (cons x1.lower rest-lower))))))

Theorem: integer-listp-of-4veclist-separate-upper-lower-rec-log.uppers

(defthm
      integer-listp-of-4veclist-separate-upper-lower-rec-log.uppers
  (implies (integer-listp rest-upper)
           (b* (((mv ?uppers ?lowers)
                 (4veclist-separate-upper-lower-rec-log
                      n x rest-upper rest-lower)))
             (integer-listp uppers)))
  :rule-classes :rewrite)

Theorem: integer-listp-of-4veclist-separate-upper-lower-rec-log.lowers

(defthm
      integer-listp-of-4veclist-separate-upper-lower-rec-log.lowers
  (implies (integer-listp rest-lower)
           (b* (((mv ?uppers ?lowers)
                 (4veclist-separate-upper-lower-rec-log
                      n x rest-upper rest-lower)))
             (integer-listp lowers)))
  :rule-classes :rewrite)