Hello,
I again need your help in some beginner questions.
I have a theorem proved:
*- lemma5_8;
> val it =
|- (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) /\
((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==> (access
t2 (k + 1) = access t1 (k + 1))) /\
((!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==> (access
t2 k = access t1 k)) /\
access t1 k <= access t1 (k + 1) ==>
access t2 k <= access t2 (k + 1) : thm*
I need to prove a theorem. After some intermediate transformations I get the
following subgoal:
* Current goal:
access t2 k <= access t2 (k + 1)
------------------------------------
0. !k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)
1. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==> (access t2
(k + 1) = access t1 (k + 1))
2. (!k. k < i - 1 \/ k > i ==> (access t2 k = access t1 k)) ==> (access t2
k = access t1 k)
3. access t1 k <= access t1 (k + 1)*
You can see that even names of variables and order of assumptions are the
same for lemma and subgoal. But I was not able to prove this. For example:
e(PROVE_TAC[lemma5_8]);
fails with "Too deep" exception with 287320 inferences on the 30-th step.
Am I correct that "assumptions" and "goal" is in fact an implication of
conjunctions and goal and my theorems are equal?
So could you please advice how I should prove the theorem using lemma?
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
