(fraig-create-output-map output-ranges types) → output-map
Function:
(defun fraig-create-output-map (output-ranges types) (declare (xargs :guard (and (aignet-output-range-map-p output-ranges) (fraig-output-type-map-p types)))) (let ((__function__ 'fraig-create-output-map)) (declare (ignorable __function__)) (if (atom output-ranges) nil (if (mbt (consp (car output-ranges))) (cons (make-fraig-output-map-entry :type (or (cdr (assoc-eq (mbe :logic (acl2::symbol-fix (caar output-ranges)) :exec (caar output-ranges)) (fraig-output-type-map-fix types))) (fraig-output-type-simplify)) :count (cdar output-ranges)) (fraig-create-output-map (cdr output-ranges) types)) (fraig-create-output-map (cdr output-ranges) types)))))
Theorem:
(defthm fraig-output-map-p-of-fraig-create-output-map (b* ((output-map (fraig-create-output-map output-ranges types))) (fraig-output-map-p output-map)) :rule-classes :rewrite)
Theorem:
(defthm count-of-fraig-create-output-map (b* ((?output-map (fraig-create-output-map output-ranges types))) (equal (fraig-output-map-total-count output-map) (aignet-output-range-map-length output-ranges))))
Theorem:
(defthm fraig-create-output-map-of-aignet-output-range-map-fix-output-ranges (equal (fraig-create-output-map (aignet-output-range-map-fix output-ranges) types) (fraig-create-output-map output-ranges types)))
Theorem:
(defthm fraig-create-output-map-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-create-output-map output-ranges types) (fraig-create-output-map output-ranges-equiv types))) :rule-classes :congruence)
Theorem:
(defthm fraig-create-output-map-of-fraig-output-type-map-fix-types (equal (fraig-create-output-map output-ranges (fraig-output-type-map-fix types)) (fraig-create-output-map output-ranges types)))
Theorem:
(defthm fraig-create-output-map-fraig-output-type-map-equiv-congruence-on-types (implies (fraig-output-type-map-equiv types types-equiv) (equal (fraig-create-output-map output-ranges types) (fraig-create-output-map output-ranges types-equiv))) :rule-classes :congruence)