(fraig-output-map-total-count x) → count
Function:
(defun fraig-output-map-total-count (x) (declare (xargs :guard (fraig-output-map-p x))) (let ((__function__ 'fraig-output-map-total-count)) (declare (ignorable __function__)) (b* (((when (atom x)) 0) ((fraig-output-map-entry x1) (car x))) (+ x1.count (fraig-output-map-total-count (cdr x))))))
Theorem:
(defthm natp-of-fraig-output-map-total-count (b* ((count (fraig-output-map-total-count x))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm fraig-output-map-total-count-of-fraig-output-map-fix-x (equal (fraig-output-map-total-count (fraig-output-map-fix x)) (fraig-output-map-total-count x)))
Theorem:
(defthm fraig-output-map-total-count-fraig-output-map-equiv-congruence-on-x (implies (fraig-output-map-equiv x x-equiv) (equal (fraig-output-map-total-count x) (fraig-output-map-total-count x-equiv))) :rule-classes :congruence)