		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

A4veclist-separate-upper-lower

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

Definitions and Theorems

Function: a4veclist-separate-upper-lower

(defun a4veclist-separate-upper-lower (x)
  (declare (xargs :guard (a4veclist-p x)))
  (let ((__function__ 'a4veclist-separate-upper-lower))
    (declare (ignorable __function__))
    (a4veclist-separate-upper-lower-aux x nil nil)))

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

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

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

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