One option is

simpLib.SIMP_PROVE (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) []
  ``(p:bool[32]) + 0x4w <> p + 0x8w``;

Anthony.

On 12 Dec 2009, at 00:21, Lu Zhao wrote:

> Hi,
> 
> I have an inequality proof:
> 
> ``(p:bool[32]) + 0x4w <> p + 0x8w``
> 
> How should I proceed to prove it?
> 
> Lu
> 
> 
> ------------------------------------------------------------------------------
> Return on Information:
> Google Enterprise Search pays you back
> Get the facts.
> http://p.sf.net/sfu/google-dev2dev
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info


------------------------------------------------------------------------------
Return on Information:
Google Enterprise Search pays you back
Get the facts.
http://p.sf.net/sfu/google-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to