Division
(int-div operand-left operand-right) → result
Function:
(defun int-div (operand-left operand-right) (declare (xargs :guard (and (int-valuep operand-left) (int-valuep operand-right)))) (declare (xargs :guard (not (equal (int-value->int operand-right) 0)))) (b* ((x (int-value->int operand-left)) (y (int-value->int operand-right))) (int-value (logext 32 (truncate x y)))))
Theorem:
(defthm int-valuep-of-int-div (b* ((result (int-div operand-left operand-right))) (int-valuep result)) :rule-classes :rewrite)
Theorem:
(defthm int-div-of-int-value-fix-operand-left (equal (int-div (int-value-fix operand-left) operand-right) (int-div operand-left operand-right)))
Theorem:
(defthm int-div-int-value-equiv-congruence-on-operand-left (implies (int-value-equiv operand-left operand-left-equiv) (equal (int-div operand-left operand-right) (int-div operand-left-equiv operand-right))) :rule-classes :congruence)
Theorem:
(defthm int-div-of-int-value-fix-operand-right (equal (int-div operand-left (int-value-fix operand-right)) (int-div operand-left operand-right)))
Theorem:
(defthm int-div-int-value-equiv-congruence-on-operand-right (implies (int-value-equiv operand-right operand-right-equiv) (equal (int-div operand-left operand-right) (int-div operand-left operand-right-equiv))) :rule-classes :congruence)