Hi, 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. Thanks. Lu ------------------------------------------------------------------------------ Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
