(fraig-output-map-has-initial-equivs x) → *
Function:
(defun fraig-output-map-has-initial-equivs (x) (declare (xargs :guard (fraig-output-map-p x))) (let ((__function__ 'fraig-output-map-has-initial-equivs)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((fraig-output-map-entry x1) (car x))) (or (fraig-output-type-case x1.type :initial-equiv-classes) (fraig-output-map-has-initial-equivs (cdr x))))))
Theorem:
(defthm fraig-output-map-has-initial-equivs-of-fraig-output-map-fix-x (equal (fraig-output-map-has-initial-equivs (fraig-output-map-fix x)) (fraig-output-map-has-initial-equivs x)))
Theorem:
(defthm fraig-output-map-has-initial-equivs-fraig-output-map-equiv-congruence-on-x (implies (fraig-output-map-equiv x x-equiv) (equal (fraig-output-map-has-initial-equivs x) (fraig-output-map-has-initial-equivs x-equiv))) :rule-classes :congruence)