Simplification with custom axioms
- To: mathgroup at smc.vnet.net
 - Subject: [mg116204] Simplification with custom axioms
 - From: Vavilen <nvr.disappear at gmail.com>
 - Date: Sat, 5 Feb 2011 05:44:16 -0500 (EST)
 
Hi all,
I wonder if it's possible to get Mathematica to understand specified
properties of functions when simplifying.
For example, by default it does not know that BitAnd[x, y] <= x:
In = FullSimplify[BitAnd[x, 10] <= 10]
Out = BitAnd[10, x] <= 10
(expected result is True)
I tried using ForAll, but without success:
In = Assuming[
  ForAll[{x, y}, 0 <= BitAnd[x, y] <= x && 0 <= BitAnd[x, y] <= y],
  FullSimplify[BitAnd[10, x] <= 10]]
Out = BitAnd[10, x] <= 10
Any ideas?