Hello.
I need advice in how to prove following subgoal. Seems that it is obvious
for human put I can't prove it in HOL.
Here f is some function of two arguments.
> val it =
f t2 (i - 2) = f t1 (i - 2)
------------------------------------
...
1. 0 <= i - 1
....
4. i < N
...
7. !k.
0 <= k /\ k < N /\ ~(k = i - 1) /\ ~(k = i) ==>
(f t2 k = f t1 k)
: goalstack
I have one doubt regarding this: if variable "i" will be equal to 1 ( it is
ok by first assumption), second arguments in goal will be equal to -1. But
it is not ok for 7-th assumption. Can this be the cause of my fail to prove
this theorem?
In any case I also not possible to prove the following goal with the same
assumptions.
i = 1 \/ f t2 (i - 2) = f t1 (i - 2)
So please advice. Any help will be greatly appreciated.
Thank you.
--
Sincerely yours,
Vladimir Yu. Timashov
ICQ: 334366950
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
