nikodemus/screamer — pull request #15 by hacdevilliers (2013-02-25 11:32:23+00:00)
Title: Fix for +-rule-down

Argument presented in the source code was
;; note: We can't assert that X and Y are integers when Z is an integer since
;; Z may be an integer when X and Y are Gaussian integers. But we can
;; make such an assertion if either X or Y is real. If the Screamer
;; type system could distinguish Gaussian integers from other complex
;; numbers we could make such an assertion whenever either X or Y was
;; not a Gaussian integer.
The argument above must surely be incorrect. If Z is an integer, and Y is a real
say 2.5 then X will surely not be an integer. The argument *does* work if eithe
r X or Y are integers. So changed things so that Z being an integer and X OR Y being an INTEGER means that X AND Y are both integers. (Note the assertion is only for X, but this is correct given that the assertion for Y happens in another call to this rule.