Hi Anthony and Magnus, Thank you very much for the solution.
I have a question on srw_ss(). Before sending the email for help, I used SIMP_TAC (std_ss++WORD_ARITH_EQ_ss) [] but it didn't work. Why does srw_ss() work and std_ss not? In what situations should I use srw_ss()? Lu > 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
