Evaluation semantics of binary-+.
Function:
(defun eval-binary-+ (x y) (declare (xargs :guard (and (valuep x) (valuep y)))) (let ((__function__ 'eval-binary-+)) (declare (ignorable __function__)) (if (value-case x :number) (if (value-case y :number) (value-number (binary-+ (value-number->get x) (value-number->get y))) (value-fix x)) (if (value-case y :number) (value-fix y) (value-number 0)))))
Theorem:
(defthm valuep-of-eval-binary-+ (b* ((result (eval-binary-+ x y))) (valuep result)) :rule-classes :rewrite)
Theorem:
(defthm eval-binary-+-of-value-fix-x (equal (eval-binary-+ (value-fix x) y) (eval-binary-+ x y)))
Theorem:
(defthm eval-binary-+-value-equiv-congruence-on-x (implies (value-equiv x x-equiv) (equal (eval-binary-+ x y) (eval-binary-+ x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm eval-binary-+-of-value-fix-y (equal (eval-binary-+ x (value-fix y)) (eval-binary-+ x y)))
Theorem:
(defthm eval-binary-+-value-equiv-congruence-on-y (implies (value-equiv y y-equiv) (equal (eval-binary-+ x y) (eval-binary-+ x y-equiv))) :rule-classes :congruence)