Function:
(defun positive-cofactor (n truth numvars) (declare (xargs :guard (and (natp n) (integerp truth) (natp numvars)))) (declare (xargs :guard (< n numvars))) (let ((__function__ 'positive-cofactor)) (declare (ignorable __function__)) (b* ((mask (logand (var n numvars) (truth-norm truth numvars)))) (logior mask (ash mask (- (ash 1 (lnfix n))))))))
Theorem:
(defthm integerp-of-positive-cofactor (b* ((cofactor (positive-cofactor n truth numvars))) (integerp cofactor)) :rule-classes :type-prescription)
Theorem:
(defthm positive-cofactor-correct (b* ((?cofactor (positive-cofactor n truth numvars))) (implies (< (nfix n) (nfix numvars)) (equal (truth-eval cofactor env numvars) (truth-eval truth (env-update n t env) numvars)))))
Theorem:
(defthm positive-cofactor-size-basic (b* ((?cofactor (positive-cofactor n truth numvars))) (implies (and (< (nfix n) numvars) (natp numvars)) (unsigned-byte-p (ash 1 numvars) cofactor))))
Theorem:
(defthm positive-cofactor-size (b* ((?cofactor (positive-cofactor n truth numvars))) (implies (and (natp m) (<= (ash 1 numvars) m) (< (nfix n) numvars) (natp numvars)) (unsigned-byte-p m cofactor))))
Theorem:
(defthm positive-cofactor-of-truth-norm (equal (positive-cofactor n (truth-norm truth numvars) numvars) (positive-cofactor n truth numvars)))
Theorem:
(defthm truth-norm-of-positive-cofactor (implies (< (nfix n) (nfix numvars)) (equal (truth-norm (positive-cofactor n truth numvars) numvars) (positive-cofactor n truth numvars))))
Theorem:
(defthm positive-cofactor-of-nfix-n (equal (positive-cofactor (nfix n) truth numvars) (positive-cofactor n truth numvars)))
Theorem:
(defthm positive-cofactor-nat-equiv-congruence-on-n (implies (nat-equiv n n-equiv) (equal (positive-cofactor n truth numvars) (positive-cofactor n-equiv truth numvars))) :rule-classes :congruence)
Theorem:
(defthm positive-cofactor-of-ifix-truth (equal (positive-cofactor n (ifix truth) numvars) (positive-cofactor n truth numvars)))
Theorem:
(defthm positive-cofactor-int-equiv-congruence-on-truth (implies (int-equiv truth truth-equiv) (equal (positive-cofactor n truth numvars) (positive-cofactor n truth-equiv numvars))) :rule-classes :congruence)
Theorem:
(defthm positive-cofactor-of-nfix-numvars (equal (positive-cofactor n truth (nfix numvars)) (positive-cofactor n truth numvars)))
Theorem:
(defthm positive-cofactor-nat-equiv-congruence-on-numvars (implies (nat-equiv numvars numvars-equiv) (equal (positive-cofactor n truth numvars) (positive-cofactor n truth numvars-equiv))) :rule-classes :congruence)