# Is it possible to resolve this proposition?

Executing this code (see MSE for its background)

ForAll[{a, b, c}, Implies[ForAll[x, -1 <= x <= 1, RealAbs[a*x^2 + b*x + c] <= 1],
ForAll[x, -1 <= x <= 1, RealAbs[c*x^2 + b*x + a] <= 2]]]
Resolve[%, Reals]


, I obtain

Beep:The kernel Local has quit (exited) during the course of an evaluation.

Can somebody with a powerful comp kindly execute it and report us the result? It would be very kind of her/him.

• FindInstance[! Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, {x, a, b, c}] returns {}, which would imply that there are no results for which this implication wouldn't hold, or am I mistaken? – kirma Aug 26 '18 at 10:24
• Also: Resolve[ForAll[{a, b, c}, Implies[Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals], Resolve[ForAll[x, -1 <= x <= 1, -2 <= c x^2 + b x + a <= 2], Reals]]], Reals] evaluates to True. – kirma Aug 26 '18 at 10:31
• @kirma: Thank you. Can you transform your second comment to an answer, elaborating it in details? – user64494 Aug 26 '18 at 10:54
• These are some of the things I'm worried about... but With[{eq = Resolve[ForAll[x, -1 <= x <= 1, -1 <= a x^2 + b x + c <= 1], Reals]}, FindInstance[! Implies[eq, -2 <= c x^2 + b x + a <= 2] && -1 <= x <= 1, {x, a, b, c}]] should, at least, resolve this problem. Frankly I thought the first Resolve would evaluate early enough not to cause trouble here - or does it? – kirma Aug 26 '18 at 17:26
• x is there in order FindInstance to look for a solution (over a, b, c and also x) which would prove the implication wrong on that range for the last part of Implies under FindInstance. No solution to that was found, which should prove that implication is right. – kirma Aug 26 '18 at 18:14

Resolve[ForAll[{a, b, c},

In addition to replacing RealAbs (which might complicate Resolve unnecessarily) with corresponding range checks, I Resolve parts of Implies early. These result somewhat complicated intermediate results, but apparently they're easier for top-level Resolve to handle than multiple ForAlls inside each other.
Resolving ForAlls and Exists tends to be a bit of black art at times. I think I didn't really change the semantics in this case...