Function:
(defun fraig-ctrex-has-relevant-disagreement (n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (declare (xargs :stobjs (ctrex-eval ctrex-relevant packed-vals packed-relevants))) (declare (xargs :guard (and (natp n) (natp ctrex-num)))) (declare (xargs :guard (and (< ctrex-num (* 32 (s32v-ncols packed-vals))) (< ctrex-num (* 32 (s32v-ncols packed-relevants))) (<= n (bits-length ctrex-eval)) (<= n (bits-length ctrex-relevant)) (<= n (s32v-nrows packed-vals)) (<= n (s32v-nrows packed-relevants))))) (let ((__function__ 'fraig-ctrex-has-relevant-disagreement)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (n (1- n)) (ctrex-rel (get-bit n ctrex-relevant)) ((when (eql 0 ctrex-rel)) (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)) (packed-rel (s32v-get-bit n ctrex-num packed-relevants)) ((when (eql 0 packed-rel)) (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)) (ctrex-val (get-bit n ctrex-eval)) (packed-val (s32v-get-bit n ctrex-num packed-vals))) (or (not (eql ctrex-val packed-val)) (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)))))
Theorem:
(defthm fraig-ctrex-has-relevant-disagreement-of-nfix-n (equal (fraig-ctrex-has-relevant-disagreement (nfix n) ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)))
Theorem:
(defthm fraig-ctrex-has-relevant-disagreement-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-has-relevant-disagreement n-equiv ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants))) :rule-classes :congruence)
Theorem:
(defthm fraig-ctrex-has-relevant-disagreement-of-nfix-ctrex-num (equal (fraig-ctrex-has-relevant-disagreement n (nfix ctrex-num) ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants)))
Theorem:
(defthm fraig-ctrex-has-relevant-disagreement-nat-equiv-congruence-on-ctrex-num (implies (nat-equiv ctrex-num ctrex-num-equiv) (equal (fraig-ctrex-has-relevant-disagreement n ctrex-num ctrex-eval ctrex-relevant packed-vals packed-relevants) (fraig-ctrex-has-relevant-disagreement n ctrex-num-equiv ctrex-eval ctrex-relevant packed-vals packed-relevants))) :rule-classes :congruence)