Hi all.
I have some problem with proving in HOL4.
I have some subgoal:
-- 1 <= i - 1
------------------------------------
0. ...
1. 1 <= i
2. ...
3. ...
4. ...
5. ...
: goalstack
So it seems to be trivial but I can't find the way to prove it in HOL. Could
anybody help me with this please? What tactic should I use? Or may be I
should inform HOL in some way to use assumption #1?
Thank you in advance.
--
Sincerely yours,
Vladimir Yu. Timashov
ICQ: 334366950
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
