		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist-separate-upper-lower-aux

Signature
(a4veclist-separate-upper-lower-aux x uppers lowers) → (mv ups lows)
Arguments: x — Guard (a4veclist-p x).; uppers — Guard (true-listp uppers).; lowers — Guard (true-listp lowers).
Returns: ups — Type (true-listp ups).; lows — Type (true-listp lows).

Definitions and Theorems

Function: a4veclist-separate-upper-lower-aux

(defun a4veclist-separate-upper-lower-aux (x uppers lowers)
 (declare (xargs :guard (and (a4veclist-p x)
                             (true-listp uppers)
                             (true-listp lowers))))
 (let ((__function__ 'a4veclist-separate-upper-lower-aux))
   (declare (ignorable __function__))
   (if (atom x)
       (mbe :logic (mv (true-list-fix uppers)
                       (true-list-fix lowers))
            :exec (mv uppers lowers))
     (b* (((a4vec x1) (car x))
          (up-len (len x1.upper))
          (low-len (len x1.lower))
          ((mv up low)
           (cond ((eql up-len low-len)
                  (mv x1.upper x1.lower))
                 ((< up-len low-len)
                  (mv (append x1.upper
                              (repeat (- low-len up-len)
                                      (car (last x1.upper))))
                      x1.lower))
                 (t (mv x1.upper
                        (append x1.lower
                                (repeat (- up-len low-len)
                                        (car (last x1.lower)))))))))
       (a4veclist-separate-upper-lower-aux (cdr x)
                                           (append up uppers)
                                           (append low lowers))))))

Theorem: true-listp-of-a4veclist-separate-upper-lower-aux.ups

(defthm true-listp-of-a4veclist-separate-upper-lower-aux.ups
  (b* (((mv ?ups ?lows)
        (a4veclist-separate-upper-lower-aux x uppers lowers)))
    (true-listp ups))
  :rule-classes :type-prescription)

Theorem: true-listp-of-a4veclist-separate-upper-lower-aux.lows

(defthm true-listp-of-a4veclist-separate-upper-lower-aux.lows
  (b* (((mv ?ups ?lows)
        (a4veclist-separate-upper-lower-aux x uppers lowers)))
    (true-listp lows))
  :rule-classes :type-prescription)