		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-wildeq-aux

Signature
(a4vec-wildeq-aux a.upper a.lower b.upper b.lower) → (mv wildeq-p-upper wildeq-p-lower)
Arguments: a.upper — aig list.
Guard (true-listp a.upper).; a.lower — aig list.
Guard (true-listp a.lower).; b.upper — aig list.
Guard (true-listp b.upper).; b.lower — aig list.
Guard (true-listp b.lower).
Returns: wildeq-p-upper — aig.; wildeq-p-lower — aig.

Definitions and Theorems

Function: a4vec-wildeq-aux

(defun a4vec-wildeq-aux (a.upper a.lower b.upper b.lower)
  (declare (xargs :guard (and (true-listp a.upper)
                              (true-listp a.lower)
                              (true-listp b.upper)
                              (true-listp b.lower))))
  (let ((__function__ 'a4vec-wildeq-aux))
    (declare (ignorable __function__))
    (b* (((mv buf bur buend)
          (gl::first/rest/end b.upper))
         ((mv blf blr blend)
          (gl::first/rest/end b.lower))
         ((mv auf aur auend)
          (gl::first/rest/end a.upper))
         ((mv alf alr alend)
          (gl::first/rest/end a.lower))
         ((mv upper1 lower1)
          (a4vec-wildeq-bit auf alf buf blf))
         ((when (mbe :logic (and4 buend blend auend alend)
                     :exec (and buend blend auend alend)))
          (mv upper1 lower1)))
      (mbe :logic
           (b* (((mv upper-rest lower-rest)
                 (a4vec-wildeq-aux aur alr bur blr)))
             (mv (aig-and upper1 upper-rest)
                 (aig-and lower1 lower-rest)))
           :exec
           (b* (((when (and (eq upper1 nil) (eq lower1 nil)))
                 (mv nil nil))
                ((mv upper-rest lower-rest)
                 (a4vec-wildeq-aux aur alr bur blr)))
             (mv (aig-and upper1 upper-rest)
                 (aig-and lower1 lower-rest)))))))

Theorem: a4vec-wildeq-aux-correct

(defthm a4vec-wildeq-aux-correct
  (b* (((mv ans.upper ans.lower)
        (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)))
    (equal (a4vec-eval (a4vec (list ans.upper)
                              (list ans.lower))
                       env)
           (4vec-wildeq (4vec (aig-list->s a.upper env)
                              (aig-list->s a.lower env))
                        (4vec (aig-list->s b.upper env)
                              (aig-list->s b.lower env))))))

Theorem: a4vec-wildeq-aux-of-list-fix-a.upper

(defthm a4vec-wildeq-aux-of-list-fix-a.upper
  (equal (a4vec-wildeq-aux (list-fix a.upper)
                           a.lower b.upper b.lower)
         (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)))

Theorem: a4vec-wildeq-aux-list-equiv-congruence-on-a.upper

(defthm a4vec-wildeq-aux-list-equiv-congruence-on-a.upper
 (implies
   (list-equiv a.upper a.upper-equiv)
   (equal (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)
          (a4vec-wildeq-aux a.upper-equiv a.lower b.upper b.lower)))
 :rule-classes :congruence)

Theorem: a4vec-wildeq-aux-of-list-fix-a.lower

(defthm a4vec-wildeq-aux-of-list-fix-a.lower
  (equal (a4vec-wildeq-aux a.upper (list-fix a.lower)
                           b.upper b.lower)
         (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)))

Theorem: a4vec-wildeq-aux-list-equiv-congruence-on-a.lower

(defthm a4vec-wildeq-aux-list-equiv-congruence-on-a.lower
 (implies
   (list-equiv a.lower a.lower-equiv)
   (equal (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)
          (a4vec-wildeq-aux a.upper a.lower-equiv b.upper b.lower)))
 :rule-classes :congruence)

Theorem: a4vec-wildeq-aux-of-list-fix-b.upper

(defthm a4vec-wildeq-aux-of-list-fix-b.upper
  (equal (a4vec-wildeq-aux a.upper a.lower (list-fix b.upper)
                           b.lower)
         (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)))

Theorem: a4vec-wildeq-aux-list-equiv-congruence-on-b.upper

(defthm a4vec-wildeq-aux-list-equiv-congruence-on-b.upper
 (implies
   (list-equiv b.upper b.upper-equiv)
   (equal (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)
          (a4vec-wildeq-aux a.upper a.lower b.upper-equiv b.lower)))
 :rule-classes :congruence)

Theorem: a4vec-wildeq-aux-of-list-fix-b.lower

(defthm a4vec-wildeq-aux-of-list-fix-b.lower
  (equal (a4vec-wildeq-aux a.upper
                           a.lower b.upper (list-fix b.lower))
         (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)))

Theorem: a4vec-wildeq-aux-list-equiv-congruence-on-b.lower

(defthm a4vec-wildeq-aux-list-equiv-congruence-on-b.lower
 (implies
   (list-equiv b.lower b.lower-equiv)
   (equal (a4vec-wildeq-aux a.upper a.lower b.upper b.lower)
          (a4vec-wildeq-aux a.upper a.lower b.upper b.lower-equiv)))
 :rule-classes :congruence)