Re: [PVS-Help] Non empty finite set induction

[Jerome <jerome@xxxxxxxxxxxxxx>]

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))
    |-------
  [1]   member(k!1, singleton(e!1))
  [2]   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

jerome