		Search-engine friendly clone of the ACL2 documentation.

Count-avx-pfx-cases

Signature
(count-avx-pfx-cases lst alst vex?) → count-alst
Arguments: lst — Guard (true-listp lst).; alst — Guard (alistp alst).; vex? — Guard (booleanp vex?).
Returns: count-alst — Type (alistp count-alst), given (and (alistp alst) (true-listp lst)).

Definitions and Theorems

Function: count-avx-pfx-cases

(defun count-avx-pfx-cases (lst alst vex?)
  (declare (xargs :guard (and (true-listp lst)
                              (alistp alst)
                              (booleanp vex?))))
  (let ((__function__ 'count-avx-pfx-cases))
    (declare (ignorable __function__))
    (if (endp lst)
        alst
      (b* ((e (car lst)) (rest (cdr lst)))
        (cond ((member e *vvvv-pfx*)
               (b* ((vvvv (nfix (cdr (assoc-equal :vvvv alst))))
                    (alst (put-assoc :vvvv (1+ vvvv) alst)))
                 (count-avx-pfx-cases rest alst vex?)))
              ((member e
                       (if vex? *l-pfx* (cons :|512| *l-pfx*)))
               (b* ((l (nfix (cdr (assoc-equal :l alst))))
                    (alst (put-assoc :l (1+ l) alst)))
                 (count-avx-pfx-cases rest alst vex?)))
              ((member e *pp-pfx*)
               (b* ((pp (nfix (cdr (assoc-equal :pp alst))))
                    (alst (put-assoc :pp (1+ pp) alst)))
                 (count-avx-pfx-cases rest alst vex?)))
              ((member e *mm-pfx*)
               (b* ((mm (nfix (cdr (assoc-equal :mm alst))))
                    (alst (put-assoc :mm (1+ mm) alst)))
                 (count-avx-pfx-cases rest alst vex?)))
              ((member e *w-pfx*)
               (b* ((w (nfix (cdr (assoc-equal :w alst))))
                    (alst (put-assoc :w (1+ w) alst)))
                 (count-avx-pfx-cases rest alst vex?))))))))

Theorem: alistp-of-count-avx-pfx-cases

(defthm alistp-of-count-avx-pfx-cases
  (implies (and (alistp alst) (true-listp lst))
           (b* ((count-alst (count-avx-pfx-cases lst alst vex?)))
             (alistp count-alst)))
  :rule-classes :rewrite)