Checks whether
Function:
(defun branches-same-under-mask-p (mask then else) (declare (xargs :guard (and (4vmask-p mask) (svex-p then) (svex-p else)))) (let ((__function__ 'branches-same-under-mask-p)) (declare (ignorable __function__)) (b* ((mask (4vmask-fix mask)) ((s4vec thenval) (svex-s4xeval then)) (then-bool (sparseint-biteqv thenval.upper thenval.lower)) ((when (sparseint-test-bitandc2 mask then-bool)) nil) ((s4vec elseval) (svex-s4xeval else)) (else-bool (sparseint-biteqv elseval.upper elseval.lower)) ((when (sparseint-test-bitandc2 mask else-bool)) nil)) (sparseint-equal (sparseint-bitand mask thenval.upper) (sparseint-bitand mask elseval.upper)))))
Theorem:
(defthm branches-same-under-mask-p-of-4vmask-fix-mask (equal (branches-same-under-mask-p (4vmask-fix mask) then else) (branches-same-under-mask-p mask then else)))
Theorem:
(defthm branches-same-under-mask-p-4vmask-equiv-congruence-on-mask (implies (4vmask-equiv mask mask-equiv) (equal (branches-same-under-mask-p mask then else) (branches-same-under-mask-p mask-equiv then else))) :rule-classes :congruence)
Theorem:
(defthm branches-same-under-mask-p-of-svex-fix-then (equal (branches-same-under-mask-p mask (svex-fix then) else) (branches-same-under-mask-p mask then else)))
Theorem:
(defthm branches-same-under-mask-p-svex-equiv-congruence-on-then (implies (svex-equiv then then-equiv) (equal (branches-same-under-mask-p mask then else) (branches-same-under-mask-p mask then-equiv else))) :rule-classes :congruence)
Theorem:
(defthm branches-same-under-mask-p-of-svex-fix-else (equal (branches-same-under-mask-p mask then (svex-fix else)) (branches-same-under-mask-p mask then else)))
Theorem:
(defthm branches-same-under-mask-p-svex-equiv-congruence-on-else (implies (svex-equiv else else-equiv) (equal (branches-same-under-mask-p mask then else) (branches-same-under-mask-p mask then else-equiv))) :rule-classes :congruence)