Hi,
I'd like to prove two sets disjoint. Currently, I use
DISJOINT_DEF,INTER_DEF,EXTENSION to rewrite the goal first, then
Cases_on each bound, and finally use WORD_DECIDE_TAC. This approach
works, but it takes a long time.
For example, it takes over 40s to prove the following theorem:
DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
{a | a >= 0x0w /\ a < 0x1000w}
I can't image how long it takes if each set has multiple segments. Is
there any efficient way to prove two sets are disjoint?
Thanks a lot.
Lu
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
