[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: Re: problem with prover*From*: rmb@dcs.gla.ac.uk*Date*: Wed, 20 May 1998 09:28:15 +0100

Enclosed is the file chunnel.pvs. I have been trying to prove the lemma move1_lemma. In so doing I get a subgoal which is now given by the lemma the_subgoal (by inspection it can be seen that this is true). I have already explained the problems with trying to prove this: the commands expand, replace etc don't work. E.g (expand "index") returns 'no change'. Your earlier solution was to use apply-extensionality, however at this stage of the proof this is not sensible, because the resulting extension is over the whole of nat. I have reduced the_subgoal by hand, using the prover to prove the bits and pieces given in lemmas length,index1,index2. The first reduction was to the lemma loopy. However i still have the same problems with trying to prove this. The second reduction,loopy0, allows apply-extensionality to produce an extension over below(2) and the prove is then immediate. Is it a bug? Is there a way out?

- Prev by Date:
**Re: PVS file management** - Next by Date:
**info on RH** - Prev by thread:
**Re: problem with prover** - Next by thread:
**question about emacs/pvs** - Index(es):