Hi Lu,
If I do the following (MoscowML based HOL),
- app load ["wordsLib","pred_setLib"];
- g `DISJOINT {a | a >= 0x1000w /\ a < 0x2000w}
{a | a >= 0x0w /\ a < 0x1000w}`;
- time e
(RW_TAC (srw_ss()) [pred_setTheory.DISJOINT_DEF,
pred_setTheory.EXTENS
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:
DI
*
1st Call for Papers
4th INTERNATIONAL CONFERENCE ON LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS
(LATA 2010)
Trier, Germany, May 24-28, 2010
http://grammars.grlmc.com/LATA2010/
*
Dear Colleagues,
Please find enclosed a Call for Lectures for the next academic year
at the Department of Computer Science of the University of L'Aquila.
I apologise if you receive multiple copies of this message.
Thank you very much.
Best regards,
Monica Nesi
Dipartimento di Informatica
