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

Re: problem with prover



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?

chunnel.pvs