(sv::aig-logxor-ss a b) → xab
Function:
(defun sv::aig-logxor-ss (a b) (declare (xargs :guard (and (true-listp a) (true-listp b)))) (let ((__function__ 'sv::aig-logxor-ss)) (declare (ignorable __function__)) (b* (((mv af ar aend) (first/rest/end a)) ((mv bf br bend) (first/rest/end b)) (c (acl2::aig-xor af bf)) ((when (and aend bend)) (sv::aig-sterm c)) (r (sv::aig-logxor-ss ar br))) (sv::aig-scons c r))))
Theorem:
(defthm sv::true-listp-of-aig-logxor-ss (b* ((xab (sv::aig-logxor-ss a b))) (true-listp xab)) :rule-classes :type-prescription)
Theorem:
(defthm sv::aig-logxor-ss-correct (b* ((xab (sv::aig-logxor-ss a b))) (and (equal (sv::aig-list->s xab env) (logxor (sv::aig-list->s a env) (sv::aig-list->s b env))))))