		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-=-ss

Signature
(sv::aig-=-ss a b) → a=b
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).

Definitions and Theorems

Function: aig-=-ss

(defun sv::aig-=-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'sv::aig-=-ss))
    (declare (ignorable __function__))
    (b* (((mv head1 tail1 end1)
          (first/rest/end a))
         ((mv head2 tail2 end2)
          (first/rest/end b))
         ((when (and end1 end2))
          (acl2::aig-iff head1 head2))
         (first-eq (acl2::aig-iff head1 head2)))
      (acl2::aig-and first-eq (sv::aig-=-ss tail1 tail2)))))

Theorem: aig-=-ss-correct

(defthm sv::aig-=-ss-correct
  (b* ((a=b (sv::aig-=-ss a b)))
    (and (equal (acl2::aig-eval a=b env)
                (equal (sv::aig-list->s a env)
                       (sv::aig-list->s b env))))))