(aignet-count-ubdd-branches-wrap count0 count1 ubdd limit) → count
Function:
(defun aignet-count-ubdd-branches-wrap (count0 count1 ubdd limit) (declare (xargs :guard (and (natp count0) (natp count1) (acl2::ubddp ubdd) (natp limit)))) (let ((__function__ 'aignet-count-ubdd-branches-wrap)) (declare (ignorable __function__)) (let ((est (* (lnfix count0) (lnfix count1)))) (if (<= est (lnfix limit)) est (aignet-count-ubdd-branches ubdd limit)))))
Theorem:
(defthm natp-of-aignet-count-ubdd-branches-wrap (b* ((count (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm aignet-count-ubdd-branches-wrap-bound (<= (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit) (nfix limit)) :rule-classes :linear)
Theorem:
(defthm aignet-count-ubdd-branches-wrap-of-nfix-count0 (equal (aignet-count-ubdd-branches-wrap (nfix count0) count1 ubdd limit) (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit)))
Theorem:
(defthm aignet-count-ubdd-branches-wrap-nat-equiv-congruence-on-count0 (implies (nat-equiv count0 count0-equiv) (equal (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit) (aignet-count-ubdd-branches-wrap count0-equiv count1 ubdd limit))) :rule-classes :congruence)
Theorem:
(defthm aignet-count-ubdd-branches-wrap-of-nfix-count1 (equal (aignet-count-ubdd-branches-wrap count0 (nfix count1) ubdd limit) (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit)))
Theorem:
(defthm aignet-count-ubdd-branches-wrap-nat-equiv-congruence-on-count1 (implies (nat-equiv count1 count1-equiv) (equal (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit) (aignet-count-ubdd-branches-wrap count0 count1-equiv ubdd limit))) :rule-classes :congruence)
Theorem:
(defthm aignet-count-ubdd-branches-wrap-of-nfix-limit (equal (aignet-count-ubdd-branches-wrap count0 count1 ubdd (nfix limit)) (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit)))
Theorem:
(defthm aignet-count-ubdd-branches-wrap-nat-equiv-congruence-on-limit (implies (nat-equiv limit limit-equiv) (equal (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit) (aignet-count-ubdd-branches-wrap count0 count1 ubdd limit-equiv))) :rule-classes :congruence)