>> I would also like to know if there is any way of defining the
>> reflexive-transitive closure of a relation in a better way (i.e., so
>> that HOL knows what it is and there is no need to prove, for example,
>> that WiresRTC(WiresRTC(a)) = WiresRTC(a)).
>>
RTC is defined in relationTheory, and you can find out a little about
it in the Description, in the section on Basic Theories. You can
also find useful definitions and theorems in an interactive session
by invoking
find "rtc";
Konrad.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
