(fraig-output-map-initial-equiv-start/count x prev-count) → (mv offset count)
Function:
(defun fraig-output-map-initial-equiv-start/count (x prev-count) (declare (xargs :guard (and (fraig-output-map-p x) (natp prev-count)))) (let ((__function__ 'fraig-output-map-initial-equiv-start/count)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv 0 0)) ((fraig-output-map-entry x1) (car x))) (if (fraig-output-type-case x1.type :initial-equiv-classes) (mv (lnfix prev-count) (logtail 1 x1.count)) (fraig-output-map-initial-equiv-start/count (cdr x) (+ x1.count (lnfix prev-count)))))))
Theorem:
(defthm natp-of-fraig-output-map-initial-equiv-start/count.offset (b* (((mv ?offset common-lisp::?count) (fraig-output-map-initial-equiv-start/count x prev-count))) (natp offset)) :rule-classes :type-prescription)
Theorem:
(defthm natp-of-fraig-output-map-initial-equiv-start/count.count (b* (((mv ?offset common-lisp::?count) (fraig-output-map-initial-equiv-start/count x prev-count))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm fraig-output-map-initial-equiv-start/count-of-fraig-output-map-fix-x (equal (fraig-output-map-initial-equiv-start/count (fraig-output-map-fix x) prev-count) (fraig-output-map-initial-equiv-start/count x prev-count)))
Theorem:
(defthm fraig-output-map-initial-equiv-start/count-fraig-output-map-equiv-congruence-on-x (implies (fraig-output-map-equiv x x-equiv) (equal (fraig-output-map-initial-equiv-start/count x prev-count) (fraig-output-map-initial-equiv-start/count x-equiv prev-count))) :rule-classes :congruence)
Theorem:
(defthm fraig-output-map-initial-equiv-start/count-of-nfix-prev-count (equal (fraig-output-map-initial-equiv-start/count x (nfix prev-count)) (fraig-output-map-initial-equiv-start/count x prev-count)))
Theorem:
(defthm fraig-output-map-initial-equiv-start/count-nat-equiv-congruence-on-prev-count (implies (nat-equiv prev-count prev-count-equiv) (equal (fraig-output-map-initial-equiv-start/count x prev-count) (fraig-output-map-initial-equiv-start/count x prev-count-equiv))) :rule-classes :congruence)