Function:
(defun fraig-ctrex-find-agreeable (ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (declare (xargs :stobjs (ctrex-eval ctrex-relevant packed-vals packed-relevants))) (declare (xargs :guard (natp ctrex-num))) (declare (xargs :guard (and (<= ctrex-num (* 32 (s32v-ncols packed-vals))) (<= ctrex-num (* 32 (s32v-ncols packed-relevants))) (<= (s32v-nrows packed-relevants) (bits-length ctrex-eval)) (<= (s32v-nrows packed-relevants) (bits-length ctrex-relevant)) (<= (s32v-nrows packed-relevants) (s32v-nrows packed-vals))))) (let ((__function__ 'fraig-ctrex-find-agreeable)) (declare (ignorable __function__)) (b* (((when (zp ctrex-num)) nil) (ctrex-num (1- ctrex-num)) ((unless (fraig-ctrex-has-relevant-disagreement (s32v-nrows packed-relevants) ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)) ctrex-num)) (fraig-ctrex-find-agreeable ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants))))
Theorem:
(defthm return-type-of-fraig-ctrex-find-agreeable (b* ((good-ctrex-num (fraig-ctrex-find-agreeable ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants))) (or (natp good-ctrex-num) (not good-ctrex-num))) :rule-classes :type-prescription)
Theorem:
(defthm fraig-ctrex-find-agreeable-bound (b* ((?good-ctrex-num (fraig-ctrex-find-agreeable ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants))) (implies good-ctrex-num (< good-ctrex-num (nfix ctrex-num)))) :rule-classes :linear)
Theorem:
(defthm fraig-ctrex-find-agreeable-of-nfix-ctrex-num (equal (fraig-ctrex-find-agreeable (nfix ctrex-num) ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-find-agreeable ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)))
Theorem:
(defthm fraig-ctrex-find-agreeable-nat-equiv-congruence-on-ctrex-num (implies (nat-equiv ctrex-num ctrex-num-equiv) (equal (fraig-ctrex-find-agreeable ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-find-agreeable ctrex-num-equiv ctrex-eval ctrex-relevant packed-vals packed-relevants))) :rule-classes :congruence)