		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

4veclist-separate-upper-lower

Signature
(4veclist-separate-upper-lower x) → (mv uppers lowers)
Arguments: x — Guard (4veclist-p x).
Returns: uppers — Type (integer-listp uppers).; lowers — Type (integer-listp lowers).

Definitions and Theorems

Function: 4veclist-separate-upper-lower

(defun 4veclist-separate-upper-lower (x)
  (declare (xargs :guard (4veclist-p x)))
  (let ((__function__ '4veclist-separate-upper-lower))
    (declare (ignorable __function__))
    (if (atom x)
        (mv nil nil)
      (b* (((mv rest-up rest-low)
            (4veclist-separate-upper-lower (cdr x)))
           ((4vec x1) (car x)))
        (mv (cons x1.upper rest-up)
            (cons x1.lower rest-low))))))

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

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

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

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

Theorem: 4veclist-separate-upper-lower-rec-log-elim

(defthm 4veclist-separate-upper-lower-rec-log-elim
 (equal
   (4veclist-separate-upper-lower-rec-log n x rest-upper rest-lower)
   (b* (((mv uppers lowers)
         (4veclist-separate-upper-lower (take n x))))
     (mv (append uppers rest-upper)
         (append lowers rest-lower)))))

Theorem: 4veclist-separate-upper-lower-fgl

(defthm 4veclist-separate-upper-lower-fgl
  (equal (4veclist-separate-upper-lower x)
         (4veclist-separate-upper-lower-rec-log (len x)
                                                x nil nil)))