| Author |
Comment/Response |
David
|
 08/25/10 04:22am
Hi
Consider the following query:
Reduce[
ForAll[{A, B}, 0 <= A <= B <= 1 && 3/2 < A + B <= 2,
Abs[A1 - A] >= Abs[B1 - B] && 0 <= A1 <= B1 <= 1
], {A1, B1}, Reals
]
on which M7 yields:
(0 <= A1 < 1/2 && 1/2 (1 + 2 A1) <= B1 <= 1) || (A1 == 1/2 &&
B1 == 1) || (A1 == 1 && B1 == 1)
Now, if I only change the Abs[A1 - A] >= Abs[B1 - B] to Abs[A1 - A] > Abs[B1 - B]:
Reduce[
ForAll[{A, B}, 0 <= A <= B <= 1 && 3/2 < A + B <= 2,
Abs[A1 - A] > Abs[B1 - B] && 0 <= A1 <= B1 <= 1
], {A1, B1}, Reals
]
M7 yields:
(0 <= A1 < 1/2 && 1/2 (1 + 2 A1) <= B1 <= 1) || (A1 == 1/2 && B1 == 1)
So. My guess is should I put Abs[A1 - A] == Abs[B1 - B] I ought to get (A1 == 1 && B1 == 1).
But M7 on the following input
Reduce[
ForAll[{A, B}, 0 <= A <= B <= 1 && 3/2 < A + B <= 2,
Abs[A1 - A] == Abs[B1 - B] && 0 <= A1 <= B1 <= 1
], {A1, B1}, Reals
]
Returns False.
Am I missing smth or is there a bug?
Thanks for replies.
Best, David
(I've also attached .nb sources.)
Attachment: zanimivost-bug.nb, URL: , |
|
