Open certik opened 4 years ago
If you allow x = 0 or y = 0, you can get factors like 0^-1. It looks like it should still be correct if arithmetic with UnsignedInfinity and Undefined is defined consistently, but my test code can't check this (yet).
I see, I forgot about that. Yes, I would not allow 1/0 at all. So it looks like the assumptions should be modified to something like this:
Assumptions(Or(
And(
Element(x, SetMinus(CC, Set(0))),
Element(y, SetMinus(CC, Set(0))),
Element(a, CC)
),
And(
Element(x, CC),
Element(y, CC),
Element(a, OpenInterval(0, oo))
),
))
Maybe one can also generalize to Re(a) > 0
or something like that.
It's this formula: http://fungrim.org/entry/2090c3/, it seems it's valid even if
x
and/ory
are 0.