Dear Lu, On Thu, 2010-04-08 at 21:20 -0600, Lu Zhao wrote: > How can I proceed to prove this seemingly very simple expression? I'm > not familiar with word proofs. > > ``(0x3w && (x :bool[32]) + 0x4w = 0x0w) <=> (0x3w && x = 0x0w)`` > > or more general, > > ``(0x3w && (x :bool[32]) + y * 0x4w = 0x0w) <=> (0x3w && x = 0x0w)`` > > Any suggestion is appreciated.
Both goals can also be solved by the Yices SMT solver, which is available as an external oracle via YICES_TAC. See Section 5.9 of the "HOL System Description" for details. Tjark ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
