[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Non empty finite set induction
On Thu, May 15, 2008 at 03:03:44PM -0600, Jerry James wrote:
>Rewriting with singleton_as_add makes the proof of the branch you are
>working on much easier.
Thanks, Jerry. That, along with a few other rewrites, did the trick.
Another set-based subgoal I have is the following:
[-1] member(choose(add(k!1, singleton(e!1))), singleton(e!1))
 member(k!1, singleton(e!1))
 singleton?(add(k!1, singleton(e!1)))
Again, seems straightforward, but figuring out which set_lemma's to
use, and in what order, isn't so easy. Any ideas? Thanks