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