[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 5:21 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> 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

That isn't straightforward, I'm afraid.  Both [1] and [2] amount to
"k!1 = e!1", but it could be that k!1 /= e!1 and choose(add(k!1,
singleton(e!1)) just happens to be e!1.
Jerry James