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

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

On Wed, May 14, 2008 at 10:18 PM, Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> I've worked it out on paper, but unfortunately can't carry it over to
> PVS. Most of my trouble comes from trying to reason about set
> operations.
> The idea is to induct on K: the base case being where K is singleton;
> the inductive step where K has an additional (arbitrary) element. My
> proof so far is as follows:

Rewriting with singleton_as_add makes the proof of the branch you are
working on much easier.
Jerry James